%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP117+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:51:16 AM UTC 2026
% Result : Theorem 0.15s 11.00s
% Output : Proof 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 1
% Syntax : Number of formulae : 1080 ( 665 unt; 0 def)
% Number of atoms : 3057 ( 0 equ)
% Maximal formula atoms : 106 ( 2 avg)
% Number of connectives : 3295 (1318 ~;1297 |; 676 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 61 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 1 prp; 0-6 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 990 ( 420 sgn 408 !; 150 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
~ ~ ( ( ? [X1] :
( ? [X2,X3,X4,X5,X6] :
( in(X1,X6,X2)
& down(X1,X6,X4)
& barrel(X1,X6)
& present(X1,X6)
& agent(X1,X6,X5)
& event(X1,X6)
& old(X1,X5)
& dirty(X1,X5)
& white(X1,X5)
& chevy(X1,X5)
& lonely(X1,X4)
& street(X1,X4)
& placename(X1,X3)
& hollywood_placename(X1,X3)
& city(X1,X2)
& of(X1,X3,X2) )
& actual_world(X1) )
=> ? [U] :
( ? [V,W,X,Y,Z] :
( in(U,Z,V)
& down(U,Z,Y)
& barrel(U,Z)
& present(U,Z)
& agent(U,Z,X)
& event(U,Z)
& lonely(U,Y)
& street(U,Y)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& placename(U,W)
& hollywood_placename(U,W)
& city(U,V)
& of(U,W,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W,X,Y,Z] :
( in(U,Z,V)
& down(U,Z,Y)
& barrel(U,Z)
& present(U,Z)
& agent(U,Z,X)
& event(U,Z)
& lonely(U,Y)
& street(U,Y)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& placename(U,W)
& hollywood_placename(U,W)
& city(U,V)
& of(U,W,V) )
& actual_world(U) )
=> ? [X1] :
( ? [X2,X3,X4,X5,X6] :
( in(X1,X6,X2)
& down(X1,X6,X4)
& barrel(X1,X6)
& present(X1,X6)
& agent(X1,X6,X5)
& event(X1,X6)
& old(X1,X5)
& dirty(X1,X5)
& white(X1,X5)
& chevy(X1,X5)
& lonely(X1,X4)
& street(X1,X4)
& placename(X1,X3)
& hollywood_placename(X1,X3)
& city(X1,X2)
& of(X1,X3,X2) )
& actual_world(X1) ) ) ),
file('theBenchmark.p',co1) ).
fof(f_1_1,negated_conjecture,
~ ( ( ? [X1] :
( ? [X2,X3,X4,X5,X6] :
( in(X1,X6,X2)
& down(X1,X6,X4)
& barrel(X1,X6)
& present(X1,X6)
& agent(X1,X6,X5)
& event(X1,X6)
& old(X1,X5)
& dirty(X1,X5)
& white(X1,X5)
& chevy(X1,X5)
& lonely(X1,X4)
& street(X1,X4)
& placename(X1,X3)
& hollywood_placename(X1,X3)
& city(X1,X2)
& of(X1,X3,X2) )
& actual_world(X1) )
=> ? [U] :
( ? [V,W,X,Y,Z] :
( in(U,Z,V)
& down(U,Z,Y)
& barrel(U,Z)
& present(U,Z)
& agent(U,Z,X)
& event(U,Z)
& lonely(U,Y)
& street(U,Y)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& placename(U,W)
& hollywood_placename(U,W)
& city(U,V)
& of(U,W,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W,X,Y,Z] :
( in(U,Z,V)
& down(U,Z,Y)
& barrel(U,Z)
& present(U,Z)
& agent(U,Z,X)
& event(U,Z)
& lonely(U,Y)
& street(U,Y)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& placename(U,W)
& hollywood_placename(U,W)
& city(U,V)
& of(U,W,V) )
& actual_world(U) )
=> ? [X1] :
( ? [X2,X3,X4,X5,X6] :
( in(X1,X6,X2)
& down(X1,X6,X4)
& barrel(X1,X6)
& present(X1,X6)
& agent(X1,X6,X5)
& event(X1,X6)
& old(X1,X5)
& dirty(X1,X5)
& white(X1,X5)
& chevy(X1,X5)
& lonely(X1,X4)
& street(X1,X4)
& placename(X1,X3)
& hollywood_placename(X1,X3)
& city(X1,X2)
& of(X1,X3,X2) )
& actual_world(X1) ) ) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_1_2,negated_conjecture,
( ( ! [U] :
( ! [V,W,X,Y,Z] :
( ~ in(U,Z,V)
| ~ down(U,Z,Y)
| ~ barrel(U,Z)
| ~ present(U,Z)
| ~ agent(U,Z,X)
| ~ event(U,Z)
| ~ lonely(U,Y)
| ~ street(U,Y)
| ~ old(U,X)
| ~ dirty(U,X)
| ~ white(U,X)
| ~ chevy(U,X)
| ~ placename(U,W)
| ~ hollywood_placename(U,W)
| ~ city(U,V)
| ~ of(U,W,V) )
| ~ actual_world(U) )
& ? [X1] :
( ? [X2,X3,X4,X5,X6] :
( in(X1,X6,X2)
& down(X1,X6,X4)
& barrel(X1,X6)
& present(X1,X6)
& agent(X1,X6,X5)
& event(X1,X6)
& old(X1,X5)
& dirty(X1,X5)
& white(X1,X5)
& chevy(X1,X5)
& lonely(X1,X4)
& street(X1,X4)
& placename(X1,X3)
& hollywood_placename(X1,X3)
& city(X1,X2)
& of(X1,X3,X2) )
& actual_world(X1) ) )
| ( ! [X1] :
( ! [X2,X3,X4,X5,X6] :
( ~ in(X1,X6,X2)
| ~ down(X1,X6,X4)
| ~ barrel(X1,X6)
| ~ present(X1,X6)
| ~ agent(X1,X6,X5)
| ~ event(X1,X6)
| ~ old(X1,X5)
| ~ dirty(X1,X5)
| ~ white(X1,X5)
| ~ chevy(X1,X5)
| ~ lonely(X1,X4)
| ~ street(X1,X4)
| ~ placename(X1,X3)
| ~ hollywood_placename(X1,X3)
| ~ city(X1,X2)
| ~ of(X1,X3,X2) )
| ~ actual_world(X1) )
& ? [U] :
( ? [V,W,X,Y,Z] :
( in(U,Z,V)
& down(U,Z,Y)
& barrel(U,Z)
& present(U,Z)
& agent(U,Z,X)
& event(U,Z)
& lonely(U,Y)
& street(U,Y)
& old(U,X)
& dirty(U,X)
& white(U,X)
& chevy(U,X)
& placename(U,W)
& hollywood_placename(U,W)
& city(U,V)
& of(U,W,V) )
& actual_world(U) ) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
( ( ! [U_23] :
( ! [U_22,U_21,U_20,U_19,U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18)
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19)
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20)
| ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ city(U_23,U_22)
| ~ of(U_23,U_21,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16,U_15,U_14,U_13,U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12)
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13)
& lonely(U_17,U_14)
& street(U_17,U_14)
& placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& city(U_17,U_16)
& of(U_17,U_15,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10,U_9,U_8,U_7,U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6)
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7)
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8)
| ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ city(U_11,U_10)
| ~ of(U_11,U_9,U_10) )
| ~ actual_world(U_11) )
& ? [U_5] :
( ? [U_4,U_3,U_2,U_1,U_0] :
( in(U_5,U_0,U_4)
& down(U_5,U_0,U_1)
& barrel(U_5,U_0)
& present(U_5,U_0)
& agent(U_5,U_0,U_2)
& event(U_5,U_0)
& lonely(U_5,U_1)
& street(U_5,U_1)
& old(U_5,U_2)
& dirty(U_5,U_2)
& white(U_5,U_2)
& chevy(U_5,U_2)
& placename(U_5,U_3)
& hollywood_placename(U_5,U_3)
& city(U_5,U_4)
& of(U_5,U_3,U_4) )
& actual_world(U_5) ) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16] :
( ? [U_15] :
( placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& of(U_17,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12) )
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13) )
& lonely(U_17,U_14)
& street(U_17,U_14) )
& city(U_17,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& ? [U_5] :
( ? [U_4] :
( ? [U_3] :
( placename(U_5,U_3)
& hollywood_placename(U_5,U_3)
& of(U_5,U_3,U_4) )
& ? [U_2] :
( ? [U_1] :
( ? [U_0] :
( in(U_5,U_0,U_4)
& down(U_5,U_0,U_1)
& barrel(U_5,U_0)
& present(U_5,U_0)
& agent(U_5,U_0,U_2)
& event(U_5,U_0) )
& lonely(U_5,U_1)
& street(U_5,U_1) )
& old(U_5,U_2)
& dirty(U_5,U_2)
& white(U_5,U_2)
& chevy(U_5,U_2) )
& city(U_5,U_4) )
& actual_world(U_5) ) ) ),
inference(miniscope,[status(thm)],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16] :
( ? [U_15] :
( placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& of(U_17,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12) )
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13) )
& lonely(U_17,U_14)
& street(U_17,U_14) )
& city(U_17,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& ? [U_4] :
( ? [U_3] :
( placename(sK1,U_3)
& hollywood_placename(sK1,U_3)
& of(sK1,U_3,U_4) )
& ? [U_2] :
( ? [U_1] :
( ? [U_0] :
( in(sK1,U_0,U_4)
& down(sK1,U_0,U_1)
& barrel(sK1,U_0)
& present(sK1,U_0)
& agent(sK1,U_0,U_2)
& event(sK1,U_0) )
& lonely(sK1,U_1)
& street(sK1,U_1) )
& old(sK1,U_2)
& dirty(sK1,U_2)
& white(sK1,U_2)
& chevy(sK1,U_2) )
& city(sK1,U_4) )
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_5,sK1)],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16] :
( ? [U_15] :
( placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& of(U_17,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12) )
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13) )
& lonely(U_17,U_14)
& street(U_17,U_14) )
& city(U_17,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& ? [U_3] :
( placename(sK1,U_3)
& hollywood_placename(sK1,U_3)
& of(sK1,U_3,sK2) )
& ? [U_2] :
( ? [U_1] :
( ? [U_0] :
( in(sK1,U_0,sK2)
& down(sK1,U_0,U_1)
& barrel(sK1,U_0)
& present(sK1,U_0)
& agent(sK1,U_0,U_2)
& event(sK1,U_0) )
& lonely(sK1,U_1)
& street(sK1,U_1) )
& old(sK1,U_2)
& dirty(sK1,U_2)
& white(sK1,U_2)
& chevy(sK1,U_2) )
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_4,sK2)],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16] :
( ? [U_15] :
( placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& of(U_17,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12) )
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13) )
& lonely(U_17,U_14)
& street(U_17,U_14) )
& city(U_17,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& ? [U_3] :
( placename(sK1,U_3)
& hollywood_placename(sK1,U_3)
& of(sK1,U_3,sK2) )
& ? [U_1] :
( ? [U_0] :
( in(sK1,U_0,sK2)
& down(sK1,U_0,U_1)
& barrel(sK1,U_0)
& present(sK1,U_0)
& agent(sK1,U_0,sK3)
& event(sK1,U_0) )
& lonely(sK1,U_1)
& street(sK1,U_1) )
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_2,sK3)],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16] :
( ? [U_15] :
( placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& of(U_17,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12) )
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13) )
& lonely(U_17,U_14)
& street(U_17,U_14) )
& city(U_17,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& ? [U_3] :
( placename(sK1,U_3)
& hollywood_placename(sK1,U_3)
& of(sK1,U_3,sK2) )
& ? [U_0] :
( in(sK1,U_0,sK2)
& down(sK1,U_0,sK4)
& barrel(sK1,U_0)
& present(sK1,U_0)
& agent(sK1,U_0,sK3)
& event(sK1,U_0) )
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_1,sK4)],[f_1_7]) ).
fof(f_1_9,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16] :
( ? [U_15] :
( placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& of(U_17,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12) )
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13) )
& lonely(U_17,U_14)
& street(U_17,U_14) )
& city(U_17,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& ? [U_3] :
( placename(sK1,U_3)
& hollywood_placename(sK1,U_3)
& of(sK1,U_3,sK2) )
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_0,sK5)],[f_1_8]) ).
fof(f_1_10,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_17] :
( ? [U_16] :
( ? [U_15] :
( placename(U_17,U_15)
& hollywood_placename(U_17,U_15)
& of(U_17,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(U_17,U_12,U_16)
& down(U_17,U_12,U_14)
& barrel(U_17,U_12)
& present(U_17,U_12)
& agent(U_17,U_12,U_13)
& event(U_17,U_12) )
& old(U_17,U_13)
& dirty(U_17,U_13)
& white(U_17,U_13)
& chevy(U_17,U_13) )
& lonely(U_17,U_14)
& street(U_17,U_14) )
& city(U_17,U_16) )
& actual_world(U_17) ) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& placename(sK1,sK6)
& hollywood_placename(sK1,sK6)
& of(sK1,sK6,sK2)
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_3,sK6)],[f_1_9]) ).
fof(f_1_11,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_16] :
( ? [U_15] :
( placename(sK7,U_15)
& hollywood_placename(sK7,U_15)
& of(sK7,U_15,U_16) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(sK7,U_12,U_16)
& down(sK7,U_12,U_14)
& barrel(sK7,U_12)
& present(sK7,U_12)
& agent(sK7,U_12,U_13)
& event(sK7,U_12) )
& old(sK7,U_13)
& dirty(sK7,U_13)
& white(sK7,U_13)
& chevy(sK7,U_13) )
& lonely(sK7,U_14)
& street(sK7,U_14) )
& city(sK7,U_16) )
& actual_world(sK7) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& placename(sK1,sK6)
& hollywood_placename(sK1,sK6)
& of(sK1,sK6,sK2)
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_17,sK7)],[f_1_10]) ).
fof(f_1_12,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_15] :
( placename(sK7,U_15)
& hollywood_placename(sK7,U_15)
& of(sK7,U_15,sK8) )
& ? [U_14] :
( ? [U_13] :
( ? [U_12] :
( in(sK7,U_12,sK8)
& down(sK7,U_12,U_14)
& barrel(sK7,U_12)
& present(sK7,U_12)
& agent(sK7,U_12,U_13)
& event(sK7,U_12) )
& old(sK7,U_13)
& dirty(sK7,U_13)
& white(sK7,U_13)
& chevy(sK7,U_13) )
& lonely(sK7,U_14)
& street(sK7,U_14) )
& city(sK7,sK8)
& actual_world(sK7) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& placename(sK1,sK6)
& hollywood_placename(sK1,sK6)
& of(sK1,sK6,sK2)
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_16,sK8)],[f_1_11]) ).
fof(f_1_13,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_15] :
( placename(sK7,U_15)
& hollywood_placename(sK7,U_15)
& of(sK7,U_15,sK8) )
& ? [U_13] :
( ? [U_12] :
( in(sK7,U_12,sK8)
& down(sK7,U_12,sK9)
& barrel(sK7,U_12)
& present(sK7,U_12)
& agent(sK7,U_12,U_13)
& event(sK7,U_12) )
& old(sK7,U_13)
& dirty(sK7,U_13)
& white(sK7,U_13)
& chevy(sK7,U_13) )
& lonely(sK7,sK9)
& street(sK7,sK9)
& city(sK7,sK8)
& actual_world(sK7) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& placename(sK1,sK6)
& hollywood_placename(sK1,sK6)
& of(sK1,sK6,sK2)
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_14,sK9)],[f_1_12]) ).
fof(f_1_14,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_15] :
( placename(sK7,U_15)
& hollywood_placename(sK7,U_15)
& of(sK7,U_15,sK8) )
& ? [U_12] :
( in(sK7,U_12,sK8)
& down(sK7,U_12,sK9)
& barrel(sK7,U_12)
& present(sK7,U_12)
& agent(sK7,U_12,sK10)
& event(sK7,U_12) )
& old(sK7,sK10)
& dirty(sK7,sK10)
& white(sK7,sK10)
& chevy(sK7,sK10)
& lonely(sK7,sK9)
& street(sK7,sK9)
& city(sK7,sK8)
& actual_world(sK7) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& placename(sK1,sK6)
& hollywood_placename(sK1,sK6)
& of(sK1,sK6,sK2)
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_13,sK10)],[f_1_13]) ).
fof(f_1_15,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& ? [U_15] :
( placename(sK7,U_15)
& hollywood_placename(sK7,U_15)
& of(sK7,U_15,sK8) )
& in(sK7,sK11,sK8)
& down(sK7,sK11,sK9)
& barrel(sK7,sK11)
& present(sK7,sK11)
& agent(sK7,sK11,sK10)
& event(sK7,sK11)
& old(sK7,sK10)
& dirty(sK7,sK10)
& white(sK7,sK10)
& chevy(sK7,sK10)
& lonely(sK7,sK9)
& street(sK7,sK9)
& city(sK7,sK8)
& actual_world(sK7) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& placename(sK1,sK6)
& hollywood_placename(sK1,sK6)
& of(sK1,sK6,sK2)
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_12,sK11)],[f_1_14]) ).
fof(f_1_16,negated_conjecture,
( ( ! [U_23] :
( ! [U_22] :
( ! [U_21] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22) )
| ! [U_20] :
( ! [U_19] :
( ! [U_18] :
( ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18) )
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19) )
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20) )
| ~ city(U_23,U_22) )
| ~ actual_world(U_23) )
& placename(sK7,sK12)
& hollywood_placename(sK7,sK12)
& of(sK7,sK12,sK8)
& in(sK7,sK11,sK8)
& down(sK7,sK11,sK9)
& barrel(sK7,sK11)
& present(sK7,sK11)
& agent(sK7,sK11,sK10)
& event(sK7,sK11)
& old(sK7,sK10)
& dirty(sK7,sK10)
& white(sK7,sK10)
& chevy(sK7,sK10)
& lonely(sK7,sK9)
& street(sK7,sK9)
& city(sK7,sK8)
& actual_world(sK7) )
| ( ! [U_11] :
( ! [U_10] :
( ! [U_9] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10) )
| ! [U_8] :
( ! [U_7] :
( ! [U_6] :
( ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6) )
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7) )
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8) )
| ~ city(U_11,U_10) )
| ~ actual_world(U_11) )
& placename(sK1,sK6)
& hollywood_placename(sK1,sK6)
& of(sK1,sK6,sK2)
& in(sK1,sK5,sK2)
& down(sK1,sK5,sK4)
& barrel(sK1,sK5)
& present(sK1,sK5)
& agent(sK1,sK5,sK3)
& event(sK1,sK5)
& lonely(sK1,sK4)
& street(sK1,sK4)
& old(sK1,sK3)
& dirty(sK1,sK3)
& white(sK1,sK3)
& chevy(sK1,sK3)
& city(sK1,sK2)
& actual_world(sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_15,sK12)],[f_1_15]) ).
fof(f_1_17,negated_conjecture,
( ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22)
| ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18)
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19)
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20)
| ~ city(U_23,U_22)
| ~ actual_world(U_23)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( placename(sK7,sK12)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( hollywood_placename(sK7,sK12)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( of(sK7,sK12,sK8)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( in(sK7,sK11,sK8)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( down(sK7,sK11,sK9)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( barrel(sK7,sK11)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( present(sK7,sK11)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( agent(sK7,sK11,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( event(sK7,sK11)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( old(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( dirty(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( white(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( chevy(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( lonely(sK7,sK9)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( street(sK7,sK9)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( city(sK7,sK8)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_20,U_21,U_22,U_23,U_18,U_19] :
( actual_world(sK7)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10)
| ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6)
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7)
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8)
| ~ city(U_11,U_10)
| ~ actual_world(U_11)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( placename(sK1,sK6)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( hollywood_placename(sK1,sK6)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( of(sK1,sK6,sK2)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( in(sK1,sK5,sK2)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( down(sK1,sK5,sK4)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( barrel(sK1,sK5)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( present(sK1,sK5)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( agent(sK1,sK5,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( event(sK1,sK5)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( lonely(sK1,sK4)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( street(sK1,sK4)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( old(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( dirty(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( white(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( chevy(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( city(sK1,sK2)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_11] :
( actual_world(sK1)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) )
& ! [U_7,U_8,U_9,U_6,U_10,U_20,U_21,U_22,U_23,U_18,U_19,U_11] :
( sP1(U_20,U_21,U_22,U_23,U_18,U_19)
| sP0(U_7,U_8,U_9,U_6,U_10,U_11) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_1_16]) ).
cnf(f_1_18,negated_conjecture,
( sP1(U_20,U_21,U_22,U_23,U_18,U_19)
| sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_19,negated_conjecture,
( actual_world(sK1)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_20,negated_conjecture,
( city(sK1,sK2)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_21,negated_conjecture,
( chevy(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_22,negated_conjecture,
( white(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_23,negated_conjecture,
( dirty(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_24,negated_conjecture,
( old(sK1,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_25,negated_conjecture,
( street(sK1,sK4)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_26,negated_conjecture,
( lonely(sK1,sK4)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_27,negated_conjecture,
( event(sK1,sK5)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_28,negated_conjecture,
( agent(sK1,sK5,sK3)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_29,negated_conjecture,
( present(sK1,sK5)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_30,negated_conjecture,
( barrel(sK1,sK5)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_31,negated_conjecture,
( down(sK1,sK5,sK4)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_32,negated_conjecture,
( in(sK1,sK5,sK2)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_33,negated_conjecture,
( of(sK1,sK6,sK2)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_34,negated_conjecture,
( hollywood_placename(sK1,sK6)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_35,negated_conjecture,
( placename(sK1,sK6)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_36,negated_conjecture,
( ~ placename(U_11,U_9)
| ~ hollywood_placename(U_11,U_9)
| ~ of(U_11,U_9,U_10)
| ~ in(U_11,U_6,U_10)
| ~ down(U_11,U_6,U_8)
| ~ barrel(U_11,U_6)
| ~ present(U_11,U_6)
| ~ agent(U_11,U_6,U_7)
| ~ event(U_11,U_6)
| ~ old(U_11,U_7)
| ~ dirty(U_11,U_7)
| ~ white(U_11,U_7)
| ~ chevy(U_11,U_7)
| ~ lonely(U_11,U_8)
| ~ street(U_11,U_8)
| ~ city(U_11,U_10)
| ~ actual_world(U_11)
| ~ sP0(U_7,U_8,U_9,U_6,U_10,U_11) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_37,negated_conjecture,
( actual_world(sK7)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_38,negated_conjecture,
( city(sK7,sK8)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_39,negated_conjecture,
( street(sK7,sK9)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_40,negated_conjecture,
( lonely(sK7,sK9)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_41,negated_conjecture,
( chevy(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_42,negated_conjecture,
( white(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_43,negated_conjecture,
( dirty(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_44,negated_conjecture,
( old(sK7,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_45,negated_conjecture,
( event(sK7,sK11)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_46,negated_conjecture,
( agent(sK7,sK11,sK10)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_47,negated_conjecture,
( present(sK7,sK11)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_48,negated_conjecture,
( barrel(sK7,sK11)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_49,negated_conjecture,
( down(sK7,sK11,sK9)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_50,negated_conjecture,
( in(sK7,sK11,sK8)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_51,negated_conjecture,
( of(sK7,sK12,sK8)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_52,negated_conjecture,
( hollywood_placename(sK7,sK12)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_53,negated_conjecture,
( placename(sK7,sK12)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(f_1_54,negated_conjecture,
( ~ placename(U_23,U_21)
| ~ hollywood_placename(U_23,U_21)
| ~ of(U_23,U_21,U_22)
| ~ in(U_23,U_18,U_22)
| ~ down(U_23,U_18,U_19)
| ~ barrel(U_23,U_18)
| ~ present(U_23,U_18)
| ~ agent(U_23,U_18,U_20)
| ~ event(U_23,U_18)
| ~ lonely(U_23,U_19)
| ~ street(U_23,U_19)
| ~ old(U_23,U_20)
| ~ dirty(U_23,U_20)
| ~ white(U_23,U_20)
| ~ chevy(U_23,U_20)
| ~ city(U_23,U_22)
| ~ actual_world(U_23)
| ~ sP1(U_20,U_21,U_22,U_23,U_18,U_19) ),
inference(clausify,[status(thm)],[f_1_17]) ).
cnf(t1,plain,
( ~ actual_world(sK7)
| ~ city(sK7,sK8)
| ~ street(sK7,sK9)
| ~ lonely(sK7,sK9)
| ~ chevy(sK7,sK10)
| ~ white(sK7,sK10)
| ~ dirty(sK7,sK10)
| ~ old(sK7,sK10)
| ~ event(sK7,sK11)
| ~ agent(sK7,sK11,sK10)
| ~ present(sK7,sK11)
| ~ barrel(sK7,sK11)
| ~ down(sK7,sK11,sK9)
| ~ in(sK7,sK11,sK8)
| ~ of(sK7,sK12,sK8)
| ~ hollywood_placename(sK7,sK12)
| ~ placename(sK7,sK12)
| ~ sP0(sK10,sK9,sK12,sK11,sK8,sK7) ),
inference(start,[status(thm),parent(0:0)],[f_1_36]) ).
cnf(t2,plain,
( sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| sP0(sK10,sK9,sK12,sK11,sK8,sK7) ),
inference(extension,[status(thm),parent(t1:1)],[f_1_18]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ actual_world(sK7)
| ~ city(sK7,sK8)
| ~ chevy(sK7,sK10)
| ~ white(sK7,sK10)
| ~ dirty(sK7,sK10)
| ~ old(sK7,sK10)
| ~ street(sK7,sK9)
| ~ lonely(sK7,sK9)
| ~ event(sK7,sK11)
| ~ agent(sK7,sK11,sK10)
| ~ present(sK7,sK11)
| ~ barrel(sK7,sK11)
| ~ down(sK7,sK11,sK9)
| ~ in(sK7,sK11,sK8)
| ~ of(sK7,sK12,sK8)
| ~ hollywood_placename(sK7,sK12)
| ~ placename(sK7,sK12)
| ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9) ),
inference(extension,[status(thm),parent(t2:2)],[f_1_54]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| placename(sK7,sK12) ),
inference(extension,[status(thm),parent(t4:2)],[f_1_53]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
$false,
inference(reduction,[status(thm),parent(t6:2)],[t6:2,t2:2]) ).
cnf(t9,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| hollywood_placename(sK7,sK12) ),
inference(extension,[status(thm),parent(t4:3)],[f_1_52]) ).
cnf(t10,plain,
$false,
inference(connection,[status(thm),parent(t9:1)],[t9:1,t4:3]) ).
cnf(t11,plain,
$false,
inference(reduction,[status(thm),parent(t9:2)],[t9:2,t2:2]) ).
cnf(t12,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| of(sK7,sK12,sK8) ),
inference(extension,[status(thm),parent(t4:4)],[f_1_51]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t4:4]) ).
cnf(t14,plain,
$false,
inference(reduction,[status(thm),parent(t12:2)],[t12:2,t2:2]) ).
cnf(t15,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| in(sK7,sK11,sK8) ),
inference(extension,[status(thm),parent(t4:5)],[f_1_50]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t4:5]) ).
cnf(t17,plain,
$false,
inference(reduction,[status(thm),parent(t15:2)],[t15:2,t2:2]) ).
cnf(t18,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| down(sK7,sK11,sK9) ),
inference(extension,[status(thm),parent(t4:6)],[f_1_49]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t4:6]) ).
cnf(t20,plain,
$false,
inference(reduction,[status(thm),parent(t18:2)],[t18:2,t2:2]) ).
cnf(t21,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| barrel(sK7,sK11) ),
inference(extension,[status(thm),parent(t4:7)],[f_1_48]) ).
cnf(t22,plain,
$false,
inference(connection,[status(thm),parent(t21:1)],[t21:1,t4:7]) ).
cnf(t23,plain,
$false,
inference(reduction,[status(thm),parent(t21:2)],[t21:2,t2:2]) ).
cnf(t24,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| present(sK7,sK11) ),
inference(extension,[status(thm),parent(t4:8)],[f_1_47]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t4:8]) ).
cnf(t26,plain,
$false,
inference(reduction,[status(thm),parent(t24:2)],[t24:2,t2:2]) ).
cnf(t27,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| agent(sK7,sK11,sK10) ),
inference(extension,[status(thm),parent(t4:9)],[f_1_46]) ).
cnf(t28,plain,
$false,
inference(connection,[status(thm),parent(t27:1)],[t27:1,t4:9]) ).
cnf(t29,plain,
$false,
inference(reduction,[status(thm),parent(t27:2)],[t27:2,t2:2]) ).
cnf(t30,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| event(sK7,sK11) ),
inference(extension,[status(thm),parent(t4:10)],[f_1_45]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t4:10]) ).
cnf(t32,plain,
$false,
inference(reduction,[status(thm),parent(t30:2)],[t30:2,t2:2]) ).
cnf(t33,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| lonely(sK7,sK9) ),
inference(extension,[status(thm),parent(t4:11)],[f_1_40]) ).
cnf(t34,plain,
$false,
inference(connection,[status(thm),parent(t33:1)],[t33:1,t4:11]) ).
cnf(t35,plain,
$false,
inference(reduction,[status(thm),parent(t33:2)],[t33:2,t2:2]) ).
cnf(t36,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| street(sK7,sK9) ),
inference(extension,[status(thm),parent(t4:12)],[f_1_39]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t4:12]) ).
cnf(t38,plain,
$false,
inference(reduction,[status(thm),parent(t36:2)],[t36:2,t2:2]) ).
cnf(t39,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| old(sK7,sK10) ),
inference(extension,[status(thm),parent(t4:13)],[f_1_44]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t4:13]) ).
cnf(t41,plain,
$false,
inference(reduction,[status(thm),parent(t39:2)],[t39:2,t2:2]) ).
cnf(t42,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| dirty(sK7,sK10) ),
inference(extension,[status(thm),parent(t4:14)],[f_1_43]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t4:14]) ).
cnf(t44,plain,
$false,
inference(reduction,[status(thm),parent(t42:2)],[t42:2,t2:2]) ).
cnf(t45,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| white(sK7,sK10) ),
inference(extension,[status(thm),parent(t4:15)],[f_1_42]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t4:15]) ).
cnf(t47,plain,
$false,
inference(reduction,[status(thm),parent(t45:2)],[t45:2,t2:2]) ).
cnf(t48,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| chevy(sK7,sK10) ),
inference(extension,[status(thm),parent(t4:16)],[f_1_41]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t4:16]) ).
cnf(t50,plain,
$false,
inference(reduction,[status(thm),parent(t48:2)],[t48:2,t2:2]) ).
cnf(t51,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| city(sK7,sK8) ),
inference(extension,[status(thm),parent(t4:17)],[f_1_38]) ).
cnf(t52,plain,
$false,
inference(connection,[status(thm),parent(t51:1)],[t51:1,t4:17]) ).
cnf(t53,plain,
$false,
inference(reduction,[status(thm),parent(t51:2)],[t51:2,t2:2]) ).
cnf(t54,plain,
( ~ sP1(sK10,sK12,sK8,sK7,sK11,sK9)
| actual_world(sK7) ),
inference(extension,[status(thm),parent(t4:18)],[f_1_37]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t4:18]) ).
cnf(t56,plain,
$false,
inference(reduction,[status(thm),parent(t54:2)],[t54:2,t2:2]) ).
cnf(t57,plain,
( ~ sP1(U_2892,U_2893,U_2894,U_2895,U_2896,U_2897)
| placename(sK7,sK12) ),
inference(extension,[status(thm),parent(t1:2)],[f_1_53]) ).
cnf(t58,plain,
$false,
inference(connection,[status(thm),parent(t57:1)],[t57:1,t1:2]) ).
cnf(t59,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_2892,U_2893,U_2894,U_2895,U_2896,U_2897) ),
inference(extension,[status(thm),parent(t57:2)],[f_1_18]) ).
cnf(t60,plain,
$false,
inference(connection,[status(thm),parent(t59:1)],[t59:1,t57:2]) ).
cnf(t61,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t59:2)],[f_1_36]) ).
cnf(t62,plain,
$false,
inference(connection,[status(thm),parent(t61:1)],[t61:1,t59:2]) ).
cnf(t63,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t61:2)],[f_1_35]) ).
cnf(t64,plain,
$false,
inference(connection,[status(thm),parent(t63:1)],[t63:1,t61:2]) ).
cnf(t65,plain,
$false,
inference(reduction,[status(thm),parent(t63:2)],[t63:2,t59:2]) ).
cnf(t66,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t61:3)],[f_1_34]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t61:3]) ).
cnf(t68,plain,
$false,
inference(reduction,[status(thm),parent(t66:2)],[t66:2,t59:2]) ).
cnf(t69,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t61:4)],[f_1_33]) ).
cnf(t70,plain,
$false,
inference(connection,[status(thm),parent(t69:1)],[t69:1,t61:4]) ).
cnf(t71,plain,
$false,
inference(reduction,[status(thm),parent(t69:2)],[t69:2,t59:2]) ).
cnf(t72,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t61:5)],[f_1_32]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t61:5]) ).
cnf(t74,plain,
$false,
inference(reduction,[status(thm),parent(t72:2)],[t72:2,t59:2]) ).
cnf(t75,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t61:6)],[f_1_31]) ).
cnf(t76,plain,
$false,
inference(connection,[status(thm),parent(t75:1)],[t75:1,t61:6]) ).
cnf(t77,plain,
$false,
inference(reduction,[status(thm),parent(t75:2)],[t75:2,t59:2]) ).
cnf(t78,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t61:7)],[f_1_30]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t61:7]) ).
cnf(t80,plain,
$false,
inference(reduction,[status(thm),parent(t78:2)],[t78:2,t59:2]) ).
cnf(t81,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t61:8)],[f_1_29]) ).
cnf(t82,plain,
$false,
inference(connection,[status(thm),parent(t81:1)],[t81:1,t61:8]) ).
cnf(t83,plain,
$false,
inference(reduction,[status(thm),parent(t81:2)],[t81:2,t59:2]) ).
cnf(t84,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t61:9)],[f_1_28]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t61:9]) ).
cnf(t86,plain,
$false,
inference(reduction,[status(thm),parent(t84:2)],[t84:2,t59:2]) ).
cnf(t87,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t61:10)],[f_1_27]) ).
cnf(t88,plain,
$false,
inference(connection,[status(thm),parent(t87:1)],[t87:1,t61:10]) ).
cnf(t89,plain,
$false,
inference(reduction,[status(thm),parent(t87:2)],[t87:2,t59:2]) ).
cnf(t90,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t61:11)],[f_1_24]) ).
cnf(t91,plain,
$false,
inference(connection,[status(thm),parent(t90:1)],[t90:1,t61:11]) ).
cnf(t92,plain,
$false,
inference(reduction,[status(thm),parent(t90:2)],[t90:2,t59:2]) ).
cnf(t93,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t61:12)],[f_1_23]) ).
cnf(t94,plain,
$false,
inference(connection,[status(thm),parent(t93:1)],[t93:1,t61:12]) ).
cnf(t95,plain,
$false,
inference(reduction,[status(thm),parent(t93:2)],[t93:2,t59:2]) ).
cnf(t96,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t61:13)],[f_1_22]) ).
cnf(t97,plain,
$false,
inference(connection,[status(thm),parent(t96:1)],[t96:1,t61:13]) ).
cnf(t98,plain,
$false,
inference(reduction,[status(thm),parent(t96:2)],[t96:2,t59:2]) ).
cnf(t99,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t61:14)],[f_1_21]) ).
cnf(t100,plain,
$false,
inference(connection,[status(thm),parent(t99:1)],[t99:1,t61:14]) ).
cnf(t101,plain,
$false,
inference(reduction,[status(thm),parent(t99:2)],[t99:2,t59:2]) ).
cnf(t102,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t61:15)],[f_1_26]) ).
cnf(t103,plain,
$false,
inference(connection,[status(thm),parent(t102:1)],[t102:1,t61:15]) ).
cnf(t104,plain,
$false,
inference(reduction,[status(thm),parent(t102:2)],[t102:2,t59:2]) ).
cnf(t105,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t61:16)],[f_1_25]) ).
cnf(t106,plain,
$false,
inference(connection,[status(thm),parent(t105:1)],[t105:1,t61:16]) ).
cnf(t107,plain,
$false,
inference(reduction,[status(thm),parent(t105:2)],[t105:2,t59:2]) ).
cnf(t108,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t61:17)],[f_1_20]) ).
cnf(t109,plain,
$false,
inference(connection,[status(thm),parent(t108:1)],[t108:1,t61:17]) ).
cnf(t110,plain,
$false,
inference(reduction,[status(thm),parent(t108:2)],[t108:2,t59:2]) ).
cnf(t111,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t61:18)],[f_1_19]) ).
cnf(t112,plain,
$false,
inference(connection,[status(thm),parent(t111:1)],[t111:1,t61:18]) ).
cnf(t113,plain,
$false,
inference(reduction,[status(thm),parent(t111:2)],[t111:2,t59:2]) ).
cnf(t114,plain,
( ~ sP1(U_3018,U_3019,U_3020,U_3021,U_3022,U_3023)
| hollywood_placename(sK7,sK12) ),
inference(extension,[status(thm),parent(t1:3)],[f_1_52]) ).
cnf(t115,plain,
$false,
inference(connection,[status(thm),parent(t114:1)],[t114:1,t1:3]) ).
cnf(t116,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3018,U_3019,U_3020,U_3021,U_3022,U_3023) ),
inference(extension,[status(thm),parent(t114:2)],[f_1_18]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t114:2]) ).
cnf(t118,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t116:2)],[f_1_36]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t116:2]) ).
cnf(t120,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t118:2)],[f_1_35]) ).
cnf(t121,plain,
$false,
inference(connection,[status(thm),parent(t120:1)],[t120:1,t118:2]) ).
cnf(t122,plain,
$false,
inference(reduction,[status(thm),parent(t120:2)],[t120:2,t116:2]) ).
cnf(t123,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t118:3)],[f_1_34]) ).
cnf(t124,plain,
$false,
inference(connection,[status(thm),parent(t123:1)],[t123:1,t118:3]) ).
cnf(t125,plain,
$false,
inference(reduction,[status(thm),parent(t123:2)],[t123:2,t116:2]) ).
cnf(t126,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t118:4)],[f_1_33]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t118:4]) ).
cnf(t128,plain,
$false,
inference(reduction,[status(thm),parent(t126:2)],[t126:2,t116:2]) ).
cnf(t129,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t118:5)],[f_1_32]) ).
cnf(t130,plain,
$false,
inference(connection,[status(thm),parent(t129:1)],[t129:1,t118:5]) ).
cnf(t131,plain,
$false,
inference(reduction,[status(thm),parent(t129:2)],[t129:2,t116:2]) ).
cnf(t132,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t118:6)],[f_1_31]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t118:6]) ).
cnf(t134,plain,
$false,
inference(reduction,[status(thm),parent(t132:2)],[t132:2,t116:2]) ).
cnf(t135,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t118:7)],[f_1_30]) ).
cnf(t136,plain,
$false,
inference(connection,[status(thm),parent(t135:1)],[t135:1,t118:7]) ).
cnf(t137,plain,
$false,
inference(reduction,[status(thm),parent(t135:2)],[t135:2,t116:2]) ).
cnf(t138,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t118:8)],[f_1_29]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t118:8]) ).
cnf(t140,plain,
$false,
inference(reduction,[status(thm),parent(t138:2)],[t138:2,t116:2]) ).
cnf(t141,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t118:9)],[f_1_28]) ).
cnf(t142,plain,
$false,
inference(connection,[status(thm),parent(t141:1)],[t141:1,t118:9]) ).
cnf(t143,plain,
$false,
inference(reduction,[status(thm),parent(t141:2)],[t141:2,t116:2]) ).
cnf(t144,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t118:10)],[f_1_27]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t118:10]) ).
cnf(t146,plain,
$false,
inference(reduction,[status(thm),parent(t144:2)],[t144:2,t116:2]) ).
cnf(t147,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t118:11)],[f_1_24]) ).
cnf(t148,plain,
$false,
inference(connection,[status(thm),parent(t147:1)],[t147:1,t118:11]) ).
cnf(t149,plain,
$false,
inference(reduction,[status(thm),parent(t147:2)],[t147:2,t116:2]) ).
cnf(t150,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t118:12)],[f_1_23]) ).
cnf(t151,plain,
$false,
inference(connection,[status(thm),parent(t150:1)],[t150:1,t118:12]) ).
cnf(t152,plain,
$false,
inference(reduction,[status(thm),parent(t150:2)],[t150:2,t116:2]) ).
cnf(t153,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t118:13)],[f_1_22]) ).
cnf(t154,plain,
$false,
inference(connection,[status(thm),parent(t153:1)],[t153:1,t118:13]) ).
cnf(t155,plain,
$false,
inference(reduction,[status(thm),parent(t153:2)],[t153:2,t116:2]) ).
cnf(t156,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t118:14)],[f_1_21]) ).
cnf(t157,plain,
$false,
inference(connection,[status(thm),parent(t156:1)],[t156:1,t118:14]) ).
cnf(t158,plain,
$false,
inference(reduction,[status(thm),parent(t156:2)],[t156:2,t116:2]) ).
cnf(t159,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t118:15)],[f_1_26]) ).
cnf(t160,plain,
$false,
inference(connection,[status(thm),parent(t159:1)],[t159:1,t118:15]) ).
cnf(t161,plain,
$false,
inference(reduction,[status(thm),parent(t159:2)],[t159:2,t116:2]) ).
cnf(t162,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t118:16)],[f_1_25]) ).
cnf(t163,plain,
$false,
inference(connection,[status(thm),parent(t162:1)],[t162:1,t118:16]) ).
cnf(t164,plain,
$false,
inference(reduction,[status(thm),parent(t162:2)],[t162:2,t116:2]) ).
cnf(t165,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t118:17)],[f_1_20]) ).
cnf(t166,plain,
$false,
inference(connection,[status(thm),parent(t165:1)],[t165:1,t118:17]) ).
cnf(t167,plain,
$false,
inference(reduction,[status(thm),parent(t165:2)],[t165:2,t116:2]) ).
cnf(t168,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t118:18)],[f_1_19]) ).
cnf(t169,plain,
$false,
inference(connection,[status(thm),parent(t168:1)],[t168:1,t118:18]) ).
cnf(t170,plain,
$false,
inference(reduction,[status(thm),parent(t168:2)],[t168:2,t116:2]) ).
cnf(t171,plain,
( ~ sP1(U_3144,U_3145,U_3146,U_3147,U_3148,U_3149)
| of(sK7,sK12,sK8) ),
inference(extension,[status(thm),parent(t1:4)],[f_1_51]) ).
cnf(t172,plain,
$false,
inference(connection,[status(thm),parent(t171:1)],[t171:1,t1:4]) ).
cnf(t173,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3144,U_3145,U_3146,U_3147,U_3148,U_3149) ),
inference(extension,[status(thm),parent(t171:2)],[f_1_18]) ).
cnf(t174,plain,
$false,
inference(connection,[status(thm),parent(t173:1)],[t173:1,t171:2]) ).
cnf(t175,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t173:2)],[f_1_36]) ).
cnf(t176,plain,
$false,
inference(connection,[status(thm),parent(t175:1)],[t175:1,t173:2]) ).
cnf(t177,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t175:2)],[f_1_35]) ).
cnf(t178,plain,
$false,
inference(connection,[status(thm),parent(t177:1)],[t177:1,t175:2]) ).
cnf(t179,plain,
$false,
inference(reduction,[status(thm),parent(t177:2)],[t177:2,t173:2]) ).
cnf(t180,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t175:3)],[f_1_34]) ).
cnf(t181,plain,
$false,
inference(connection,[status(thm),parent(t180:1)],[t180:1,t175:3]) ).
cnf(t182,plain,
$false,
inference(reduction,[status(thm),parent(t180:2)],[t180:2,t173:2]) ).
cnf(t183,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t175:4)],[f_1_33]) ).
cnf(t184,plain,
$false,
inference(connection,[status(thm),parent(t183:1)],[t183:1,t175:4]) ).
cnf(t185,plain,
$false,
inference(reduction,[status(thm),parent(t183:2)],[t183:2,t173:2]) ).
cnf(t186,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t175:5)],[f_1_32]) ).
cnf(t187,plain,
$false,
inference(connection,[status(thm),parent(t186:1)],[t186:1,t175:5]) ).
cnf(t188,plain,
$false,
inference(reduction,[status(thm),parent(t186:2)],[t186:2,t173:2]) ).
cnf(t189,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t175:6)],[f_1_31]) ).
cnf(t190,plain,
$false,
inference(connection,[status(thm),parent(t189:1)],[t189:1,t175:6]) ).
cnf(t191,plain,
$false,
inference(reduction,[status(thm),parent(t189:2)],[t189:2,t173:2]) ).
cnf(t192,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t175:7)],[f_1_30]) ).
cnf(t193,plain,
$false,
inference(connection,[status(thm),parent(t192:1)],[t192:1,t175:7]) ).
cnf(t194,plain,
$false,
inference(reduction,[status(thm),parent(t192:2)],[t192:2,t173:2]) ).
cnf(t195,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t175:8)],[f_1_29]) ).
cnf(t196,plain,
$false,
inference(connection,[status(thm),parent(t195:1)],[t195:1,t175:8]) ).
cnf(t197,plain,
$false,
inference(reduction,[status(thm),parent(t195:2)],[t195:2,t173:2]) ).
cnf(t198,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t175:9)],[f_1_28]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t175:9]) ).
cnf(t200,plain,
$false,
inference(reduction,[status(thm),parent(t198:2)],[t198:2,t173:2]) ).
cnf(t201,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t175:10)],[f_1_27]) ).
cnf(t202,plain,
$false,
inference(connection,[status(thm),parent(t201:1)],[t201:1,t175:10]) ).
cnf(t203,plain,
$false,
inference(reduction,[status(thm),parent(t201:2)],[t201:2,t173:2]) ).
cnf(t204,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t175:11)],[f_1_24]) ).
cnf(t205,plain,
$false,
inference(connection,[status(thm),parent(t204:1)],[t204:1,t175:11]) ).
cnf(t206,plain,
$false,
inference(reduction,[status(thm),parent(t204:2)],[t204:2,t173:2]) ).
cnf(t207,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t175:12)],[f_1_23]) ).
cnf(t208,plain,
$false,
inference(connection,[status(thm),parent(t207:1)],[t207:1,t175:12]) ).
cnf(t209,plain,
$false,
inference(reduction,[status(thm),parent(t207:2)],[t207:2,t173:2]) ).
cnf(t210,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t175:13)],[f_1_22]) ).
cnf(t211,plain,
$false,
inference(connection,[status(thm),parent(t210:1)],[t210:1,t175:13]) ).
cnf(t212,plain,
$false,
inference(reduction,[status(thm),parent(t210:2)],[t210:2,t173:2]) ).
cnf(t213,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t175:14)],[f_1_21]) ).
cnf(t214,plain,
$false,
inference(connection,[status(thm),parent(t213:1)],[t213:1,t175:14]) ).
cnf(t215,plain,
$false,
inference(reduction,[status(thm),parent(t213:2)],[t213:2,t173:2]) ).
cnf(t216,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t175:15)],[f_1_26]) ).
cnf(t217,plain,
$false,
inference(connection,[status(thm),parent(t216:1)],[t216:1,t175:15]) ).
cnf(t218,plain,
$false,
inference(reduction,[status(thm),parent(t216:2)],[t216:2,t173:2]) ).
cnf(t219,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t175:16)],[f_1_25]) ).
cnf(t220,plain,
$false,
inference(connection,[status(thm),parent(t219:1)],[t219:1,t175:16]) ).
cnf(t221,plain,
$false,
inference(reduction,[status(thm),parent(t219:2)],[t219:2,t173:2]) ).
cnf(t222,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t175:17)],[f_1_20]) ).
cnf(t223,plain,
$false,
inference(connection,[status(thm),parent(t222:1)],[t222:1,t175:17]) ).
cnf(t224,plain,
$false,
inference(reduction,[status(thm),parent(t222:2)],[t222:2,t173:2]) ).
cnf(t225,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t175:18)],[f_1_19]) ).
cnf(t226,plain,
$false,
inference(connection,[status(thm),parent(t225:1)],[t225:1,t175:18]) ).
cnf(t227,plain,
$false,
inference(reduction,[status(thm),parent(t225:2)],[t225:2,t173:2]) ).
cnf(t228,plain,
( ~ sP1(U_3270,U_3271,U_3272,U_3273,U_3274,U_3275)
| in(sK7,sK11,sK8) ),
inference(extension,[status(thm),parent(t1:5)],[f_1_50]) ).
cnf(t229,plain,
$false,
inference(connection,[status(thm),parent(t228:1)],[t228:1,t1:5]) ).
cnf(t230,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3270,U_3271,U_3272,U_3273,U_3274,U_3275) ),
inference(extension,[status(thm),parent(t228:2)],[f_1_18]) ).
cnf(t231,plain,
$false,
inference(connection,[status(thm),parent(t230:1)],[t230:1,t228:2]) ).
cnf(t232,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t230:2)],[f_1_36]) ).
cnf(t233,plain,
$false,
inference(connection,[status(thm),parent(t232:1)],[t232:1,t230:2]) ).
cnf(t234,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t232:2)],[f_1_35]) ).
cnf(t235,plain,
$false,
inference(connection,[status(thm),parent(t234:1)],[t234:1,t232:2]) ).
cnf(t236,plain,
$false,
inference(reduction,[status(thm),parent(t234:2)],[t234:2,t230:2]) ).
cnf(t237,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t232:3)],[f_1_34]) ).
cnf(t238,plain,
$false,
inference(connection,[status(thm),parent(t237:1)],[t237:1,t232:3]) ).
cnf(t239,plain,
$false,
inference(reduction,[status(thm),parent(t237:2)],[t237:2,t230:2]) ).
cnf(t240,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t232:4)],[f_1_33]) ).
cnf(t241,plain,
$false,
inference(connection,[status(thm),parent(t240:1)],[t240:1,t232:4]) ).
cnf(t242,plain,
$false,
inference(reduction,[status(thm),parent(t240:2)],[t240:2,t230:2]) ).
cnf(t243,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t232:5)],[f_1_32]) ).
cnf(t244,plain,
$false,
inference(connection,[status(thm),parent(t243:1)],[t243:1,t232:5]) ).
cnf(t245,plain,
$false,
inference(reduction,[status(thm),parent(t243:2)],[t243:2,t230:2]) ).
cnf(t246,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t232:6)],[f_1_31]) ).
cnf(t247,plain,
$false,
inference(connection,[status(thm),parent(t246:1)],[t246:1,t232:6]) ).
cnf(t248,plain,
$false,
inference(reduction,[status(thm),parent(t246:2)],[t246:2,t230:2]) ).
cnf(t249,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t232:7)],[f_1_30]) ).
cnf(t250,plain,
$false,
inference(connection,[status(thm),parent(t249:1)],[t249:1,t232:7]) ).
cnf(t251,plain,
$false,
inference(reduction,[status(thm),parent(t249:2)],[t249:2,t230:2]) ).
cnf(t252,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t232:8)],[f_1_29]) ).
cnf(t253,plain,
$false,
inference(connection,[status(thm),parent(t252:1)],[t252:1,t232:8]) ).
cnf(t254,plain,
$false,
inference(reduction,[status(thm),parent(t252:2)],[t252:2,t230:2]) ).
cnf(t255,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t232:9)],[f_1_28]) ).
cnf(t256,plain,
$false,
inference(connection,[status(thm),parent(t255:1)],[t255:1,t232:9]) ).
cnf(t257,plain,
$false,
inference(reduction,[status(thm),parent(t255:2)],[t255:2,t230:2]) ).
cnf(t258,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t232:10)],[f_1_27]) ).
cnf(t259,plain,
$false,
inference(connection,[status(thm),parent(t258:1)],[t258:1,t232:10]) ).
cnf(t260,plain,
$false,
inference(reduction,[status(thm),parent(t258:2)],[t258:2,t230:2]) ).
cnf(t261,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t232:11)],[f_1_24]) ).
cnf(t262,plain,
$false,
inference(connection,[status(thm),parent(t261:1)],[t261:1,t232:11]) ).
cnf(t263,plain,
$false,
inference(reduction,[status(thm),parent(t261:2)],[t261:2,t230:2]) ).
cnf(t264,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t232:12)],[f_1_23]) ).
cnf(t265,plain,
$false,
inference(connection,[status(thm),parent(t264:1)],[t264:1,t232:12]) ).
cnf(t266,plain,
$false,
inference(reduction,[status(thm),parent(t264:2)],[t264:2,t230:2]) ).
cnf(t267,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t232:13)],[f_1_22]) ).
cnf(t268,plain,
$false,
inference(connection,[status(thm),parent(t267:1)],[t267:1,t232:13]) ).
cnf(t269,plain,
$false,
inference(reduction,[status(thm),parent(t267:2)],[t267:2,t230:2]) ).
cnf(t270,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t232:14)],[f_1_21]) ).
cnf(t271,plain,
$false,
inference(connection,[status(thm),parent(t270:1)],[t270:1,t232:14]) ).
cnf(t272,plain,
$false,
inference(reduction,[status(thm),parent(t270:2)],[t270:2,t230:2]) ).
cnf(t273,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t232:15)],[f_1_26]) ).
cnf(t274,plain,
$false,
inference(connection,[status(thm),parent(t273:1)],[t273:1,t232:15]) ).
cnf(t275,plain,
$false,
inference(reduction,[status(thm),parent(t273:2)],[t273:2,t230:2]) ).
cnf(t276,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t232:16)],[f_1_25]) ).
cnf(t277,plain,
$false,
inference(connection,[status(thm),parent(t276:1)],[t276:1,t232:16]) ).
cnf(t278,plain,
$false,
inference(reduction,[status(thm),parent(t276:2)],[t276:2,t230:2]) ).
cnf(t279,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t232:17)],[f_1_20]) ).
cnf(t280,plain,
$false,
inference(connection,[status(thm),parent(t279:1)],[t279:1,t232:17]) ).
cnf(t281,plain,
$false,
inference(reduction,[status(thm),parent(t279:2)],[t279:2,t230:2]) ).
cnf(t282,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t232:18)],[f_1_19]) ).
cnf(t283,plain,
$false,
inference(connection,[status(thm),parent(t282:1)],[t282:1,t232:18]) ).
cnf(t284,plain,
$false,
inference(reduction,[status(thm),parent(t282:2)],[t282:2,t230:2]) ).
cnf(t285,plain,
( ~ sP1(U_3396,U_3397,U_3398,U_3399,U_3400,U_3401)
| down(sK7,sK11,sK9) ),
inference(extension,[status(thm),parent(t1:6)],[f_1_49]) ).
cnf(t286,plain,
$false,
inference(connection,[status(thm),parent(t285:1)],[t285:1,t1:6]) ).
cnf(t287,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3396,U_3397,U_3398,U_3399,U_3400,U_3401) ),
inference(extension,[status(thm),parent(t285:2)],[f_1_18]) ).
cnf(t288,plain,
$false,
inference(connection,[status(thm),parent(t287:1)],[t287:1,t285:2]) ).
cnf(t289,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t287:2)],[f_1_36]) ).
cnf(t290,plain,
$false,
inference(connection,[status(thm),parent(t289:1)],[t289:1,t287:2]) ).
cnf(t291,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t289:2)],[f_1_35]) ).
cnf(t292,plain,
$false,
inference(connection,[status(thm),parent(t291:1)],[t291:1,t289:2]) ).
cnf(t293,plain,
$false,
inference(reduction,[status(thm),parent(t291:2)],[t291:2,t287:2]) ).
cnf(t294,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t289:3)],[f_1_34]) ).
cnf(t295,plain,
$false,
inference(connection,[status(thm),parent(t294:1)],[t294:1,t289:3]) ).
cnf(t296,plain,
$false,
inference(reduction,[status(thm),parent(t294:2)],[t294:2,t287:2]) ).
cnf(t297,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t289:4)],[f_1_33]) ).
cnf(t298,plain,
$false,
inference(connection,[status(thm),parent(t297:1)],[t297:1,t289:4]) ).
cnf(t299,plain,
$false,
inference(reduction,[status(thm),parent(t297:2)],[t297:2,t287:2]) ).
cnf(t300,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t289:5)],[f_1_32]) ).
cnf(t301,plain,
$false,
inference(connection,[status(thm),parent(t300:1)],[t300:1,t289:5]) ).
cnf(t302,plain,
$false,
inference(reduction,[status(thm),parent(t300:2)],[t300:2,t287:2]) ).
cnf(t303,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t289:6)],[f_1_31]) ).
cnf(t304,plain,
$false,
inference(connection,[status(thm),parent(t303:1)],[t303:1,t289:6]) ).
cnf(t305,plain,
$false,
inference(reduction,[status(thm),parent(t303:2)],[t303:2,t287:2]) ).
cnf(t306,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t289:7)],[f_1_30]) ).
cnf(t307,plain,
$false,
inference(connection,[status(thm),parent(t306:1)],[t306:1,t289:7]) ).
cnf(t308,plain,
$false,
inference(reduction,[status(thm),parent(t306:2)],[t306:2,t287:2]) ).
cnf(t309,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t289:8)],[f_1_29]) ).
cnf(t310,plain,
$false,
inference(connection,[status(thm),parent(t309:1)],[t309:1,t289:8]) ).
cnf(t311,plain,
$false,
inference(reduction,[status(thm),parent(t309:2)],[t309:2,t287:2]) ).
cnf(t312,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t289:9)],[f_1_28]) ).
cnf(t313,plain,
$false,
inference(connection,[status(thm),parent(t312:1)],[t312:1,t289:9]) ).
cnf(t314,plain,
$false,
inference(reduction,[status(thm),parent(t312:2)],[t312:2,t287:2]) ).
cnf(t315,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t289:10)],[f_1_27]) ).
cnf(t316,plain,
$false,
inference(connection,[status(thm),parent(t315:1)],[t315:1,t289:10]) ).
cnf(t317,plain,
$false,
inference(reduction,[status(thm),parent(t315:2)],[t315:2,t287:2]) ).
cnf(t318,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t289:11)],[f_1_24]) ).
cnf(t319,plain,
$false,
inference(connection,[status(thm),parent(t318:1)],[t318:1,t289:11]) ).
cnf(t320,plain,
$false,
inference(reduction,[status(thm),parent(t318:2)],[t318:2,t287:2]) ).
cnf(t321,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t289:12)],[f_1_23]) ).
cnf(t322,plain,
$false,
inference(connection,[status(thm),parent(t321:1)],[t321:1,t289:12]) ).
cnf(t323,plain,
$false,
inference(reduction,[status(thm),parent(t321:2)],[t321:2,t287:2]) ).
cnf(t324,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t289:13)],[f_1_22]) ).
cnf(t325,plain,
$false,
inference(connection,[status(thm),parent(t324:1)],[t324:1,t289:13]) ).
cnf(t326,plain,
$false,
inference(reduction,[status(thm),parent(t324:2)],[t324:2,t287:2]) ).
cnf(t327,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t289:14)],[f_1_21]) ).
cnf(t328,plain,
$false,
inference(connection,[status(thm),parent(t327:1)],[t327:1,t289:14]) ).
cnf(t329,plain,
$false,
inference(reduction,[status(thm),parent(t327:2)],[t327:2,t287:2]) ).
cnf(t330,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t289:15)],[f_1_26]) ).
cnf(t331,plain,
$false,
inference(connection,[status(thm),parent(t330:1)],[t330:1,t289:15]) ).
cnf(t332,plain,
$false,
inference(reduction,[status(thm),parent(t330:2)],[t330:2,t287:2]) ).
cnf(t333,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t289:16)],[f_1_25]) ).
cnf(t334,plain,
$false,
inference(connection,[status(thm),parent(t333:1)],[t333:1,t289:16]) ).
cnf(t335,plain,
$false,
inference(reduction,[status(thm),parent(t333:2)],[t333:2,t287:2]) ).
cnf(t336,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t289:17)],[f_1_20]) ).
cnf(t337,plain,
$false,
inference(connection,[status(thm),parent(t336:1)],[t336:1,t289:17]) ).
cnf(t338,plain,
$false,
inference(reduction,[status(thm),parent(t336:2)],[t336:2,t287:2]) ).
cnf(t339,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t289:18)],[f_1_19]) ).
cnf(t340,plain,
$false,
inference(connection,[status(thm),parent(t339:1)],[t339:1,t289:18]) ).
cnf(t341,plain,
$false,
inference(reduction,[status(thm),parent(t339:2)],[t339:2,t287:2]) ).
cnf(t342,plain,
( ~ sP1(U_3522,U_3523,U_3524,U_3525,U_3526,U_3527)
| barrel(sK7,sK11) ),
inference(extension,[status(thm),parent(t1:7)],[f_1_48]) ).
cnf(t343,plain,
$false,
inference(connection,[status(thm),parent(t342:1)],[t342:1,t1:7]) ).
cnf(t344,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3522,U_3523,U_3524,U_3525,U_3526,U_3527) ),
inference(extension,[status(thm),parent(t342:2)],[f_1_18]) ).
cnf(t345,plain,
$false,
inference(connection,[status(thm),parent(t344:1)],[t344:1,t342:2]) ).
cnf(t346,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t344:2)],[f_1_36]) ).
cnf(t347,plain,
$false,
inference(connection,[status(thm),parent(t346:1)],[t346:1,t344:2]) ).
cnf(t348,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t346:2)],[f_1_35]) ).
cnf(t349,plain,
$false,
inference(connection,[status(thm),parent(t348:1)],[t348:1,t346:2]) ).
cnf(t350,plain,
$false,
inference(reduction,[status(thm),parent(t348:2)],[t348:2,t344:2]) ).
cnf(t351,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t346:3)],[f_1_34]) ).
cnf(t352,plain,
$false,
inference(connection,[status(thm),parent(t351:1)],[t351:1,t346:3]) ).
cnf(t353,plain,
$false,
inference(reduction,[status(thm),parent(t351:2)],[t351:2,t344:2]) ).
cnf(t354,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t346:4)],[f_1_33]) ).
cnf(t355,plain,
$false,
inference(connection,[status(thm),parent(t354:1)],[t354:1,t346:4]) ).
cnf(t356,plain,
$false,
inference(reduction,[status(thm),parent(t354:2)],[t354:2,t344:2]) ).
cnf(t357,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t346:5)],[f_1_32]) ).
cnf(t358,plain,
$false,
inference(connection,[status(thm),parent(t357:1)],[t357:1,t346:5]) ).
cnf(t359,plain,
$false,
inference(reduction,[status(thm),parent(t357:2)],[t357:2,t344:2]) ).
cnf(t360,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t346:6)],[f_1_31]) ).
cnf(t361,plain,
$false,
inference(connection,[status(thm),parent(t360:1)],[t360:1,t346:6]) ).
cnf(t362,plain,
$false,
inference(reduction,[status(thm),parent(t360:2)],[t360:2,t344:2]) ).
cnf(t363,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t346:7)],[f_1_30]) ).
cnf(t364,plain,
$false,
inference(connection,[status(thm),parent(t363:1)],[t363:1,t346:7]) ).
cnf(t365,plain,
$false,
inference(reduction,[status(thm),parent(t363:2)],[t363:2,t344:2]) ).
cnf(t366,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t346:8)],[f_1_29]) ).
cnf(t367,plain,
$false,
inference(connection,[status(thm),parent(t366:1)],[t366:1,t346:8]) ).
cnf(t368,plain,
$false,
inference(reduction,[status(thm),parent(t366:2)],[t366:2,t344:2]) ).
cnf(t369,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t346:9)],[f_1_28]) ).
cnf(t370,plain,
$false,
inference(connection,[status(thm),parent(t369:1)],[t369:1,t346:9]) ).
cnf(t371,plain,
$false,
inference(reduction,[status(thm),parent(t369:2)],[t369:2,t344:2]) ).
cnf(t372,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t346:10)],[f_1_27]) ).
cnf(t373,plain,
$false,
inference(connection,[status(thm),parent(t372:1)],[t372:1,t346:10]) ).
cnf(t374,plain,
$false,
inference(reduction,[status(thm),parent(t372:2)],[t372:2,t344:2]) ).
cnf(t375,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t346:11)],[f_1_24]) ).
cnf(t376,plain,
$false,
inference(connection,[status(thm),parent(t375:1)],[t375:1,t346:11]) ).
cnf(t377,plain,
$false,
inference(reduction,[status(thm),parent(t375:2)],[t375:2,t344:2]) ).
cnf(t378,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t346:12)],[f_1_23]) ).
cnf(t379,plain,
$false,
inference(connection,[status(thm),parent(t378:1)],[t378:1,t346:12]) ).
cnf(t380,plain,
$false,
inference(reduction,[status(thm),parent(t378:2)],[t378:2,t344:2]) ).
cnf(t381,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t346:13)],[f_1_22]) ).
cnf(t382,plain,
$false,
inference(connection,[status(thm),parent(t381:1)],[t381:1,t346:13]) ).
cnf(t383,plain,
$false,
inference(reduction,[status(thm),parent(t381:2)],[t381:2,t344:2]) ).
cnf(t384,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t346:14)],[f_1_21]) ).
cnf(t385,plain,
$false,
inference(connection,[status(thm),parent(t384:1)],[t384:1,t346:14]) ).
cnf(t386,plain,
$false,
inference(reduction,[status(thm),parent(t384:2)],[t384:2,t344:2]) ).
cnf(t387,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t346:15)],[f_1_26]) ).
cnf(t388,plain,
$false,
inference(connection,[status(thm),parent(t387:1)],[t387:1,t346:15]) ).
cnf(t389,plain,
$false,
inference(reduction,[status(thm),parent(t387:2)],[t387:2,t344:2]) ).
cnf(t390,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t346:16)],[f_1_25]) ).
cnf(t391,plain,
$false,
inference(connection,[status(thm),parent(t390:1)],[t390:1,t346:16]) ).
cnf(t392,plain,
$false,
inference(reduction,[status(thm),parent(t390:2)],[t390:2,t344:2]) ).
cnf(t393,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t346:17)],[f_1_20]) ).
cnf(t394,plain,
$false,
inference(connection,[status(thm),parent(t393:1)],[t393:1,t346:17]) ).
cnf(t395,plain,
$false,
inference(reduction,[status(thm),parent(t393:2)],[t393:2,t344:2]) ).
cnf(t396,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t346:18)],[f_1_19]) ).
cnf(t397,plain,
$false,
inference(connection,[status(thm),parent(t396:1)],[t396:1,t346:18]) ).
cnf(t398,plain,
$false,
inference(reduction,[status(thm),parent(t396:2)],[t396:2,t344:2]) ).
cnf(t399,plain,
( ~ sP1(U_3648,U_3649,U_3650,U_3651,U_3652,U_3653)
| present(sK7,sK11) ),
inference(extension,[status(thm),parent(t1:8)],[f_1_47]) ).
cnf(t400,plain,
$false,
inference(connection,[status(thm),parent(t399:1)],[t399:1,t1:8]) ).
cnf(t401,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3648,U_3649,U_3650,U_3651,U_3652,U_3653) ),
inference(extension,[status(thm),parent(t399:2)],[f_1_18]) ).
cnf(t402,plain,
$false,
inference(connection,[status(thm),parent(t401:1)],[t401:1,t399:2]) ).
cnf(t403,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t401:2)],[f_1_36]) ).
cnf(t404,plain,
$false,
inference(connection,[status(thm),parent(t403:1)],[t403:1,t401:2]) ).
cnf(t405,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t403:2)],[f_1_35]) ).
cnf(t406,plain,
$false,
inference(connection,[status(thm),parent(t405:1)],[t405:1,t403:2]) ).
cnf(t407,plain,
$false,
inference(reduction,[status(thm),parent(t405:2)],[t405:2,t401:2]) ).
cnf(t408,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t403:3)],[f_1_34]) ).
cnf(t409,plain,
$false,
inference(connection,[status(thm),parent(t408:1)],[t408:1,t403:3]) ).
cnf(t410,plain,
$false,
inference(reduction,[status(thm),parent(t408:2)],[t408:2,t401:2]) ).
cnf(t411,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t403:4)],[f_1_33]) ).
cnf(t412,plain,
$false,
inference(connection,[status(thm),parent(t411:1)],[t411:1,t403:4]) ).
cnf(t413,plain,
$false,
inference(reduction,[status(thm),parent(t411:2)],[t411:2,t401:2]) ).
cnf(t414,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t403:5)],[f_1_32]) ).
cnf(t415,plain,
$false,
inference(connection,[status(thm),parent(t414:1)],[t414:1,t403:5]) ).
cnf(t416,plain,
$false,
inference(reduction,[status(thm),parent(t414:2)],[t414:2,t401:2]) ).
cnf(t417,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t403:6)],[f_1_31]) ).
cnf(t418,plain,
$false,
inference(connection,[status(thm),parent(t417:1)],[t417:1,t403:6]) ).
cnf(t419,plain,
$false,
inference(reduction,[status(thm),parent(t417:2)],[t417:2,t401:2]) ).
cnf(t420,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t403:7)],[f_1_30]) ).
cnf(t421,plain,
$false,
inference(connection,[status(thm),parent(t420:1)],[t420:1,t403:7]) ).
cnf(t422,plain,
$false,
inference(reduction,[status(thm),parent(t420:2)],[t420:2,t401:2]) ).
cnf(t423,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t403:8)],[f_1_29]) ).
cnf(t424,plain,
$false,
inference(connection,[status(thm),parent(t423:1)],[t423:1,t403:8]) ).
cnf(t425,plain,
$false,
inference(reduction,[status(thm),parent(t423:2)],[t423:2,t401:2]) ).
cnf(t426,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t403:9)],[f_1_28]) ).
cnf(t427,plain,
$false,
inference(connection,[status(thm),parent(t426:1)],[t426:1,t403:9]) ).
cnf(t428,plain,
$false,
inference(reduction,[status(thm),parent(t426:2)],[t426:2,t401:2]) ).
cnf(t429,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t403:10)],[f_1_27]) ).
cnf(t430,plain,
$false,
inference(connection,[status(thm),parent(t429:1)],[t429:1,t403:10]) ).
cnf(t431,plain,
$false,
inference(reduction,[status(thm),parent(t429:2)],[t429:2,t401:2]) ).
cnf(t432,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t403:11)],[f_1_24]) ).
cnf(t433,plain,
$false,
inference(connection,[status(thm),parent(t432:1)],[t432:1,t403:11]) ).
cnf(t434,plain,
$false,
inference(reduction,[status(thm),parent(t432:2)],[t432:2,t401:2]) ).
cnf(t435,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t403:12)],[f_1_23]) ).
cnf(t436,plain,
$false,
inference(connection,[status(thm),parent(t435:1)],[t435:1,t403:12]) ).
cnf(t437,plain,
$false,
inference(reduction,[status(thm),parent(t435:2)],[t435:2,t401:2]) ).
cnf(t438,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t403:13)],[f_1_22]) ).
cnf(t439,plain,
$false,
inference(connection,[status(thm),parent(t438:1)],[t438:1,t403:13]) ).
cnf(t440,plain,
$false,
inference(reduction,[status(thm),parent(t438:2)],[t438:2,t401:2]) ).
cnf(t441,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t403:14)],[f_1_21]) ).
cnf(t442,plain,
$false,
inference(connection,[status(thm),parent(t441:1)],[t441:1,t403:14]) ).
cnf(t443,plain,
$false,
inference(reduction,[status(thm),parent(t441:2)],[t441:2,t401:2]) ).
cnf(t444,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t403:15)],[f_1_26]) ).
cnf(t445,plain,
$false,
inference(connection,[status(thm),parent(t444:1)],[t444:1,t403:15]) ).
cnf(t446,plain,
$false,
inference(reduction,[status(thm),parent(t444:2)],[t444:2,t401:2]) ).
cnf(t447,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t403:16)],[f_1_25]) ).
cnf(t448,plain,
$false,
inference(connection,[status(thm),parent(t447:1)],[t447:1,t403:16]) ).
cnf(t449,plain,
$false,
inference(reduction,[status(thm),parent(t447:2)],[t447:2,t401:2]) ).
cnf(t450,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t403:17)],[f_1_20]) ).
cnf(t451,plain,
$false,
inference(connection,[status(thm),parent(t450:1)],[t450:1,t403:17]) ).
cnf(t452,plain,
$false,
inference(reduction,[status(thm),parent(t450:2)],[t450:2,t401:2]) ).
cnf(t453,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t403:18)],[f_1_19]) ).
cnf(t454,plain,
$false,
inference(connection,[status(thm),parent(t453:1)],[t453:1,t403:18]) ).
cnf(t455,plain,
$false,
inference(reduction,[status(thm),parent(t453:2)],[t453:2,t401:2]) ).
cnf(t456,plain,
( ~ sP1(U_3774,U_3775,U_3776,U_3777,U_3778,U_3779)
| agent(sK7,sK11,sK10) ),
inference(extension,[status(thm),parent(t1:9)],[f_1_46]) ).
cnf(t457,plain,
$false,
inference(connection,[status(thm),parent(t456:1)],[t456:1,t1:9]) ).
cnf(t458,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3774,U_3775,U_3776,U_3777,U_3778,U_3779) ),
inference(extension,[status(thm),parent(t456:2)],[f_1_18]) ).
cnf(t459,plain,
$false,
inference(connection,[status(thm),parent(t458:1)],[t458:1,t456:2]) ).
cnf(t460,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t458:2)],[f_1_36]) ).
cnf(t461,plain,
$false,
inference(connection,[status(thm),parent(t460:1)],[t460:1,t458:2]) ).
cnf(t462,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t460:2)],[f_1_35]) ).
cnf(t463,plain,
$false,
inference(connection,[status(thm),parent(t462:1)],[t462:1,t460:2]) ).
cnf(t464,plain,
$false,
inference(reduction,[status(thm),parent(t462:2)],[t462:2,t458:2]) ).
cnf(t465,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t460:3)],[f_1_34]) ).
cnf(t466,plain,
$false,
inference(connection,[status(thm),parent(t465:1)],[t465:1,t460:3]) ).
cnf(t467,plain,
$false,
inference(reduction,[status(thm),parent(t465:2)],[t465:2,t458:2]) ).
cnf(t468,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t460:4)],[f_1_33]) ).
cnf(t469,plain,
$false,
inference(connection,[status(thm),parent(t468:1)],[t468:1,t460:4]) ).
cnf(t470,plain,
$false,
inference(reduction,[status(thm),parent(t468:2)],[t468:2,t458:2]) ).
cnf(t471,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t460:5)],[f_1_32]) ).
cnf(t472,plain,
$false,
inference(connection,[status(thm),parent(t471:1)],[t471:1,t460:5]) ).
cnf(t473,plain,
$false,
inference(reduction,[status(thm),parent(t471:2)],[t471:2,t458:2]) ).
cnf(t474,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t460:6)],[f_1_31]) ).
cnf(t475,plain,
$false,
inference(connection,[status(thm),parent(t474:1)],[t474:1,t460:6]) ).
cnf(t476,plain,
$false,
inference(reduction,[status(thm),parent(t474:2)],[t474:2,t458:2]) ).
cnf(t477,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t460:7)],[f_1_30]) ).
cnf(t478,plain,
$false,
inference(connection,[status(thm),parent(t477:1)],[t477:1,t460:7]) ).
cnf(t479,plain,
$false,
inference(reduction,[status(thm),parent(t477:2)],[t477:2,t458:2]) ).
cnf(t480,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t460:8)],[f_1_29]) ).
cnf(t481,plain,
$false,
inference(connection,[status(thm),parent(t480:1)],[t480:1,t460:8]) ).
cnf(t482,plain,
$false,
inference(reduction,[status(thm),parent(t480:2)],[t480:2,t458:2]) ).
cnf(t483,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t460:9)],[f_1_28]) ).
cnf(t484,plain,
$false,
inference(connection,[status(thm),parent(t483:1)],[t483:1,t460:9]) ).
cnf(t485,plain,
$false,
inference(reduction,[status(thm),parent(t483:2)],[t483:2,t458:2]) ).
cnf(t486,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t460:10)],[f_1_27]) ).
cnf(t487,plain,
$false,
inference(connection,[status(thm),parent(t486:1)],[t486:1,t460:10]) ).
cnf(t488,plain,
$false,
inference(reduction,[status(thm),parent(t486:2)],[t486:2,t458:2]) ).
cnf(t489,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t460:11)],[f_1_24]) ).
cnf(t490,plain,
$false,
inference(connection,[status(thm),parent(t489:1)],[t489:1,t460:11]) ).
cnf(t491,plain,
$false,
inference(reduction,[status(thm),parent(t489:2)],[t489:2,t458:2]) ).
cnf(t492,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t460:12)],[f_1_23]) ).
cnf(t493,plain,
$false,
inference(connection,[status(thm),parent(t492:1)],[t492:1,t460:12]) ).
cnf(t494,plain,
$false,
inference(reduction,[status(thm),parent(t492:2)],[t492:2,t458:2]) ).
cnf(t495,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t460:13)],[f_1_22]) ).
cnf(t496,plain,
$false,
inference(connection,[status(thm),parent(t495:1)],[t495:1,t460:13]) ).
cnf(t497,plain,
$false,
inference(reduction,[status(thm),parent(t495:2)],[t495:2,t458:2]) ).
cnf(t498,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t460:14)],[f_1_21]) ).
cnf(t499,plain,
$false,
inference(connection,[status(thm),parent(t498:1)],[t498:1,t460:14]) ).
cnf(t500,plain,
$false,
inference(reduction,[status(thm),parent(t498:2)],[t498:2,t458:2]) ).
cnf(t501,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t460:15)],[f_1_26]) ).
cnf(t502,plain,
$false,
inference(connection,[status(thm),parent(t501:1)],[t501:1,t460:15]) ).
cnf(t503,plain,
$false,
inference(reduction,[status(thm),parent(t501:2)],[t501:2,t458:2]) ).
cnf(t504,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t460:16)],[f_1_25]) ).
cnf(t505,plain,
$false,
inference(connection,[status(thm),parent(t504:1)],[t504:1,t460:16]) ).
cnf(t506,plain,
$false,
inference(reduction,[status(thm),parent(t504:2)],[t504:2,t458:2]) ).
cnf(t507,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t460:17)],[f_1_20]) ).
cnf(t508,plain,
$false,
inference(connection,[status(thm),parent(t507:1)],[t507:1,t460:17]) ).
cnf(t509,plain,
$false,
inference(reduction,[status(thm),parent(t507:2)],[t507:2,t458:2]) ).
cnf(t510,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t460:18)],[f_1_19]) ).
cnf(t511,plain,
$false,
inference(connection,[status(thm),parent(t510:1)],[t510:1,t460:18]) ).
cnf(t512,plain,
$false,
inference(reduction,[status(thm),parent(t510:2)],[t510:2,t458:2]) ).
cnf(t513,plain,
( ~ sP1(U_3900,U_3901,U_3902,U_3903,U_3904,U_3905)
| event(sK7,sK11) ),
inference(extension,[status(thm),parent(t1:10)],[f_1_45]) ).
cnf(t514,plain,
$false,
inference(connection,[status(thm),parent(t513:1)],[t513:1,t1:10]) ).
cnf(t515,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_3900,U_3901,U_3902,U_3903,U_3904,U_3905) ),
inference(extension,[status(thm),parent(t513:2)],[f_1_18]) ).
cnf(t516,plain,
$false,
inference(connection,[status(thm),parent(t515:1)],[t515:1,t513:2]) ).
cnf(t517,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t515:2)],[f_1_36]) ).
cnf(t518,plain,
$false,
inference(connection,[status(thm),parent(t517:1)],[t517:1,t515:2]) ).
cnf(t519,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t517:2)],[f_1_35]) ).
cnf(t520,plain,
$false,
inference(connection,[status(thm),parent(t519:1)],[t519:1,t517:2]) ).
cnf(t521,plain,
$false,
inference(reduction,[status(thm),parent(t519:2)],[t519:2,t515:2]) ).
cnf(t522,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t517:3)],[f_1_34]) ).
cnf(t523,plain,
$false,
inference(connection,[status(thm),parent(t522:1)],[t522:1,t517:3]) ).
cnf(t524,plain,
$false,
inference(reduction,[status(thm),parent(t522:2)],[t522:2,t515:2]) ).
cnf(t525,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t517:4)],[f_1_33]) ).
cnf(t526,plain,
$false,
inference(connection,[status(thm),parent(t525:1)],[t525:1,t517:4]) ).
cnf(t527,plain,
$false,
inference(reduction,[status(thm),parent(t525:2)],[t525:2,t515:2]) ).
cnf(t528,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t517:5)],[f_1_32]) ).
cnf(t529,plain,
$false,
inference(connection,[status(thm),parent(t528:1)],[t528:1,t517:5]) ).
cnf(t530,plain,
$false,
inference(reduction,[status(thm),parent(t528:2)],[t528:2,t515:2]) ).
cnf(t531,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t517:6)],[f_1_31]) ).
cnf(t532,plain,
$false,
inference(connection,[status(thm),parent(t531:1)],[t531:1,t517:6]) ).
cnf(t533,plain,
$false,
inference(reduction,[status(thm),parent(t531:2)],[t531:2,t515:2]) ).
cnf(t534,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t517:7)],[f_1_30]) ).
cnf(t535,plain,
$false,
inference(connection,[status(thm),parent(t534:1)],[t534:1,t517:7]) ).
cnf(t536,plain,
$false,
inference(reduction,[status(thm),parent(t534:2)],[t534:2,t515:2]) ).
cnf(t537,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t517:8)],[f_1_29]) ).
cnf(t538,plain,
$false,
inference(connection,[status(thm),parent(t537:1)],[t537:1,t517:8]) ).
cnf(t539,plain,
$false,
inference(reduction,[status(thm),parent(t537:2)],[t537:2,t515:2]) ).
cnf(t540,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t517:9)],[f_1_28]) ).
cnf(t541,plain,
$false,
inference(connection,[status(thm),parent(t540:1)],[t540:1,t517:9]) ).
cnf(t542,plain,
$false,
inference(reduction,[status(thm),parent(t540:2)],[t540:2,t515:2]) ).
cnf(t543,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t517:10)],[f_1_27]) ).
cnf(t544,plain,
$false,
inference(connection,[status(thm),parent(t543:1)],[t543:1,t517:10]) ).
cnf(t545,plain,
$false,
inference(reduction,[status(thm),parent(t543:2)],[t543:2,t515:2]) ).
cnf(t546,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t517:11)],[f_1_24]) ).
cnf(t547,plain,
$false,
inference(connection,[status(thm),parent(t546:1)],[t546:1,t517:11]) ).
cnf(t548,plain,
$false,
inference(reduction,[status(thm),parent(t546:2)],[t546:2,t515:2]) ).
cnf(t549,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t517:12)],[f_1_23]) ).
cnf(t550,plain,
$false,
inference(connection,[status(thm),parent(t549:1)],[t549:1,t517:12]) ).
cnf(t551,plain,
$false,
inference(reduction,[status(thm),parent(t549:2)],[t549:2,t515:2]) ).
cnf(t552,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t517:13)],[f_1_22]) ).
cnf(t553,plain,
$false,
inference(connection,[status(thm),parent(t552:1)],[t552:1,t517:13]) ).
cnf(t554,plain,
$false,
inference(reduction,[status(thm),parent(t552:2)],[t552:2,t515:2]) ).
cnf(t555,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t517:14)],[f_1_21]) ).
cnf(t556,plain,
$false,
inference(connection,[status(thm),parent(t555:1)],[t555:1,t517:14]) ).
cnf(t557,plain,
$false,
inference(reduction,[status(thm),parent(t555:2)],[t555:2,t515:2]) ).
cnf(t558,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t517:15)],[f_1_26]) ).
cnf(t559,plain,
$false,
inference(connection,[status(thm),parent(t558:1)],[t558:1,t517:15]) ).
cnf(t560,plain,
$false,
inference(reduction,[status(thm),parent(t558:2)],[t558:2,t515:2]) ).
cnf(t561,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t517:16)],[f_1_25]) ).
cnf(t562,plain,
$false,
inference(connection,[status(thm),parent(t561:1)],[t561:1,t517:16]) ).
cnf(t563,plain,
$false,
inference(reduction,[status(thm),parent(t561:2)],[t561:2,t515:2]) ).
cnf(t564,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t517:17)],[f_1_20]) ).
cnf(t565,plain,
$false,
inference(connection,[status(thm),parent(t564:1)],[t564:1,t517:17]) ).
cnf(t566,plain,
$false,
inference(reduction,[status(thm),parent(t564:2)],[t564:2,t515:2]) ).
cnf(t567,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t517:18)],[f_1_19]) ).
cnf(t568,plain,
$false,
inference(connection,[status(thm),parent(t567:1)],[t567:1,t517:18]) ).
cnf(t569,plain,
$false,
inference(reduction,[status(thm),parent(t567:2)],[t567:2,t515:2]) ).
cnf(t570,plain,
( ~ sP1(U_4026,U_4027,U_4028,U_4029,U_4030,U_4031)
| old(sK7,sK10) ),
inference(extension,[status(thm),parent(t1:11)],[f_1_44]) ).
cnf(t571,plain,
$false,
inference(connection,[status(thm),parent(t570:1)],[t570:1,t1:11]) ).
cnf(t572,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4026,U_4027,U_4028,U_4029,U_4030,U_4031) ),
inference(extension,[status(thm),parent(t570:2)],[f_1_18]) ).
cnf(t573,plain,
$false,
inference(connection,[status(thm),parent(t572:1)],[t572:1,t570:2]) ).
cnf(t574,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t572:2)],[f_1_36]) ).
cnf(t575,plain,
$false,
inference(connection,[status(thm),parent(t574:1)],[t574:1,t572:2]) ).
cnf(t576,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t574:2)],[f_1_35]) ).
cnf(t577,plain,
$false,
inference(connection,[status(thm),parent(t576:1)],[t576:1,t574:2]) ).
cnf(t578,plain,
$false,
inference(reduction,[status(thm),parent(t576:2)],[t576:2,t572:2]) ).
cnf(t579,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t574:3)],[f_1_34]) ).
cnf(t580,plain,
$false,
inference(connection,[status(thm),parent(t579:1)],[t579:1,t574:3]) ).
cnf(t581,plain,
$false,
inference(reduction,[status(thm),parent(t579:2)],[t579:2,t572:2]) ).
cnf(t582,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t574:4)],[f_1_33]) ).
cnf(t583,plain,
$false,
inference(connection,[status(thm),parent(t582:1)],[t582:1,t574:4]) ).
cnf(t584,plain,
$false,
inference(reduction,[status(thm),parent(t582:2)],[t582:2,t572:2]) ).
cnf(t585,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t574:5)],[f_1_32]) ).
cnf(t586,plain,
$false,
inference(connection,[status(thm),parent(t585:1)],[t585:1,t574:5]) ).
cnf(t587,plain,
$false,
inference(reduction,[status(thm),parent(t585:2)],[t585:2,t572:2]) ).
cnf(t588,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t574:6)],[f_1_31]) ).
cnf(t589,plain,
$false,
inference(connection,[status(thm),parent(t588:1)],[t588:1,t574:6]) ).
cnf(t590,plain,
$false,
inference(reduction,[status(thm),parent(t588:2)],[t588:2,t572:2]) ).
cnf(t591,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t574:7)],[f_1_30]) ).
cnf(t592,plain,
$false,
inference(connection,[status(thm),parent(t591:1)],[t591:1,t574:7]) ).
cnf(t593,plain,
$false,
inference(reduction,[status(thm),parent(t591:2)],[t591:2,t572:2]) ).
cnf(t594,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t574:8)],[f_1_29]) ).
cnf(t595,plain,
$false,
inference(connection,[status(thm),parent(t594:1)],[t594:1,t574:8]) ).
cnf(t596,plain,
$false,
inference(reduction,[status(thm),parent(t594:2)],[t594:2,t572:2]) ).
cnf(t597,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t574:9)],[f_1_28]) ).
cnf(t598,plain,
$false,
inference(connection,[status(thm),parent(t597:1)],[t597:1,t574:9]) ).
cnf(t599,plain,
$false,
inference(reduction,[status(thm),parent(t597:2)],[t597:2,t572:2]) ).
cnf(t600,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t574:10)],[f_1_27]) ).
cnf(t601,plain,
$false,
inference(connection,[status(thm),parent(t600:1)],[t600:1,t574:10]) ).
cnf(t602,plain,
$false,
inference(reduction,[status(thm),parent(t600:2)],[t600:2,t572:2]) ).
cnf(t603,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t574:11)],[f_1_24]) ).
cnf(t604,plain,
$false,
inference(connection,[status(thm),parent(t603:1)],[t603:1,t574:11]) ).
cnf(t605,plain,
$false,
inference(reduction,[status(thm),parent(t603:2)],[t603:2,t572:2]) ).
cnf(t606,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t574:12)],[f_1_23]) ).
cnf(t607,plain,
$false,
inference(connection,[status(thm),parent(t606:1)],[t606:1,t574:12]) ).
cnf(t608,plain,
$false,
inference(reduction,[status(thm),parent(t606:2)],[t606:2,t572:2]) ).
cnf(t609,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t574:13)],[f_1_22]) ).
cnf(t610,plain,
$false,
inference(connection,[status(thm),parent(t609:1)],[t609:1,t574:13]) ).
cnf(t611,plain,
$false,
inference(reduction,[status(thm),parent(t609:2)],[t609:2,t572:2]) ).
cnf(t612,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t574:14)],[f_1_21]) ).
cnf(t613,plain,
$false,
inference(connection,[status(thm),parent(t612:1)],[t612:1,t574:14]) ).
cnf(t614,plain,
$false,
inference(reduction,[status(thm),parent(t612:2)],[t612:2,t572:2]) ).
cnf(t615,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t574:15)],[f_1_26]) ).
cnf(t616,plain,
$false,
inference(connection,[status(thm),parent(t615:1)],[t615:1,t574:15]) ).
cnf(t617,plain,
$false,
inference(reduction,[status(thm),parent(t615:2)],[t615:2,t572:2]) ).
cnf(t618,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t574:16)],[f_1_25]) ).
cnf(t619,plain,
$false,
inference(connection,[status(thm),parent(t618:1)],[t618:1,t574:16]) ).
cnf(t620,plain,
$false,
inference(reduction,[status(thm),parent(t618:2)],[t618:2,t572:2]) ).
cnf(t621,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t574:17)],[f_1_20]) ).
cnf(t622,plain,
$false,
inference(connection,[status(thm),parent(t621:1)],[t621:1,t574:17]) ).
cnf(t623,plain,
$false,
inference(reduction,[status(thm),parent(t621:2)],[t621:2,t572:2]) ).
cnf(t624,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t574:18)],[f_1_19]) ).
cnf(t625,plain,
$false,
inference(connection,[status(thm),parent(t624:1)],[t624:1,t574:18]) ).
cnf(t626,plain,
$false,
inference(reduction,[status(thm),parent(t624:2)],[t624:2,t572:2]) ).
cnf(t627,plain,
( ~ sP1(U_4152,U_4153,U_4154,U_4155,U_4156,U_4157)
| dirty(sK7,sK10) ),
inference(extension,[status(thm),parent(t1:12)],[f_1_43]) ).
cnf(t628,plain,
$false,
inference(connection,[status(thm),parent(t627:1)],[t627:1,t1:12]) ).
cnf(t629,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4152,U_4153,U_4154,U_4155,U_4156,U_4157) ),
inference(extension,[status(thm),parent(t627:2)],[f_1_18]) ).
cnf(t630,plain,
$false,
inference(connection,[status(thm),parent(t629:1)],[t629:1,t627:2]) ).
cnf(t631,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t629:2)],[f_1_36]) ).
cnf(t632,plain,
$false,
inference(connection,[status(thm),parent(t631:1)],[t631:1,t629:2]) ).
cnf(t633,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t631:2)],[f_1_35]) ).
cnf(t634,plain,
$false,
inference(connection,[status(thm),parent(t633:1)],[t633:1,t631:2]) ).
cnf(t635,plain,
$false,
inference(reduction,[status(thm),parent(t633:2)],[t633:2,t629:2]) ).
cnf(t636,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t631:3)],[f_1_34]) ).
cnf(t637,plain,
$false,
inference(connection,[status(thm),parent(t636:1)],[t636:1,t631:3]) ).
cnf(t638,plain,
$false,
inference(reduction,[status(thm),parent(t636:2)],[t636:2,t629:2]) ).
cnf(t639,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t631:4)],[f_1_33]) ).
cnf(t640,plain,
$false,
inference(connection,[status(thm),parent(t639:1)],[t639:1,t631:4]) ).
cnf(t641,plain,
$false,
inference(reduction,[status(thm),parent(t639:2)],[t639:2,t629:2]) ).
cnf(t642,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t631:5)],[f_1_32]) ).
cnf(t643,plain,
$false,
inference(connection,[status(thm),parent(t642:1)],[t642:1,t631:5]) ).
cnf(t644,plain,
$false,
inference(reduction,[status(thm),parent(t642:2)],[t642:2,t629:2]) ).
cnf(t645,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t631:6)],[f_1_31]) ).
cnf(t646,plain,
$false,
inference(connection,[status(thm),parent(t645:1)],[t645:1,t631:6]) ).
cnf(t647,plain,
$false,
inference(reduction,[status(thm),parent(t645:2)],[t645:2,t629:2]) ).
cnf(t648,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t631:7)],[f_1_30]) ).
cnf(t649,plain,
$false,
inference(connection,[status(thm),parent(t648:1)],[t648:1,t631:7]) ).
cnf(t650,plain,
$false,
inference(reduction,[status(thm),parent(t648:2)],[t648:2,t629:2]) ).
cnf(t651,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t631:8)],[f_1_29]) ).
cnf(t652,plain,
$false,
inference(connection,[status(thm),parent(t651:1)],[t651:1,t631:8]) ).
cnf(t653,plain,
$false,
inference(reduction,[status(thm),parent(t651:2)],[t651:2,t629:2]) ).
cnf(t654,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t631:9)],[f_1_28]) ).
cnf(t655,plain,
$false,
inference(connection,[status(thm),parent(t654:1)],[t654:1,t631:9]) ).
cnf(t656,plain,
$false,
inference(reduction,[status(thm),parent(t654:2)],[t654:2,t629:2]) ).
cnf(t657,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t631:10)],[f_1_27]) ).
cnf(t658,plain,
$false,
inference(connection,[status(thm),parent(t657:1)],[t657:1,t631:10]) ).
cnf(t659,plain,
$false,
inference(reduction,[status(thm),parent(t657:2)],[t657:2,t629:2]) ).
cnf(t660,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t631:11)],[f_1_24]) ).
cnf(t661,plain,
$false,
inference(connection,[status(thm),parent(t660:1)],[t660:1,t631:11]) ).
cnf(t662,plain,
$false,
inference(reduction,[status(thm),parent(t660:2)],[t660:2,t629:2]) ).
cnf(t663,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t631:12)],[f_1_23]) ).
cnf(t664,plain,
$false,
inference(connection,[status(thm),parent(t663:1)],[t663:1,t631:12]) ).
cnf(t665,plain,
$false,
inference(reduction,[status(thm),parent(t663:2)],[t663:2,t629:2]) ).
cnf(t666,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t631:13)],[f_1_22]) ).
cnf(t667,plain,
$false,
inference(connection,[status(thm),parent(t666:1)],[t666:1,t631:13]) ).
cnf(t668,plain,
$false,
inference(reduction,[status(thm),parent(t666:2)],[t666:2,t629:2]) ).
cnf(t669,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t631:14)],[f_1_21]) ).
cnf(t670,plain,
$false,
inference(connection,[status(thm),parent(t669:1)],[t669:1,t631:14]) ).
cnf(t671,plain,
$false,
inference(reduction,[status(thm),parent(t669:2)],[t669:2,t629:2]) ).
cnf(t672,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t631:15)],[f_1_26]) ).
cnf(t673,plain,
$false,
inference(connection,[status(thm),parent(t672:1)],[t672:1,t631:15]) ).
cnf(t674,plain,
$false,
inference(reduction,[status(thm),parent(t672:2)],[t672:2,t629:2]) ).
cnf(t675,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t631:16)],[f_1_25]) ).
cnf(t676,plain,
$false,
inference(connection,[status(thm),parent(t675:1)],[t675:1,t631:16]) ).
cnf(t677,plain,
$false,
inference(reduction,[status(thm),parent(t675:2)],[t675:2,t629:2]) ).
cnf(t678,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t631:17)],[f_1_20]) ).
cnf(t679,plain,
$false,
inference(connection,[status(thm),parent(t678:1)],[t678:1,t631:17]) ).
cnf(t680,plain,
$false,
inference(reduction,[status(thm),parent(t678:2)],[t678:2,t629:2]) ).
cnf(t681,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t631:18)],[f_1_19]) ).
cnf(t682,plain,
$false,
inference(connection,[status(thm),parent(t681:1)],[t681:1,t631:18]) ).
cnf(t683,plain,
$false,
inference(reduction,[status(thm),parent(t681:2)],[t681:2,t629:2]) ).
cnf(t684,plain,
( ~ sP1(U_4278,U_4279,U_4280,U_4281,U_4282,U_4283)
| white(sK7,sK10) ),
inference(extension,[status(thm),parent(t1:13)],[f_1_42]) ).
cnf(t685,plain,
$false,
inference(connection,[status(thm),parent(t684:1)],[t684:1,t1:13]) ).
cnf(t686,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4278,U_4279,U_4280,U_4281,U_4282,U_4283) ),
inference(extension,[status(thm),parent(t684:2)],[f_1_18]) ).
cnf(t687,plain,
$false,
inference(connection,[status(thm),parent(t686:1)],[t686:1,t684:2]) ).
cnf(t688,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t686:2)],[f_1_36]) ).
cnf(t689,plain,
$false,
inference(connection,[status(thm),parent(t688:1)],[t688:1,t686:2]) ).
cnf(t690,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t688:2)],[f_1_35]) ).
cnf(t691,plain,
$false,
inference(connection,[status(thm),parent(t690:1)],[t690:1,t688:2]) ).
cnf(t692,plain,
$false,
inference(reduction,[status(thm),parent(t690:2)],[t690:2,t686:2]) ).
cnf(t693,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t688:3)],[f_1_34]) ).
cnf(t694,plain,
$false,
inference(connection,[status(thm),parent(t693:1)],[t693:1,t688:3]) ).
cnf(t695,plain,
$false,
inference(reduction,[status(thm),parent(t693:2)],[t693:2,t686:2]) ).
cnf(t696,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t688:4)],[f_1_33]) ).
cnf(t697,plain,
$false,
inference(connection,[status(thm),parent(t696:1)],[t696:1,t688:4]) ).
cnf(t698,plain,
$false,
inference(reduction,[status(thm),parent(t696:2)],[t696:2,t686:2]) ).
cnf(t699,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t688:5)],[f_1_32]) ).
cnf(t700,plain,
$false,
inference(connection,[status(thm),parent(t699:1)],[t699:1,t688:5]) ).
cnf(t701,plain,
$false,
inference(reduction,[status(thm),parent(t699:2)],[t699:2,t686:2]) ).
cnf(t702,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t688:6)],[f_1_31]) ).
cnf(t703,plain,
$false,
inference(connection,[status(thm),parent(t702:1)],[t702:1,t688:6]) ).
cnf(t704,plain,
$false,
inference(reduction,[status(thm),parent(t702:2)],[t702:2,t686:2]) ).
cnf(t705,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t688:7)],[f_1_30]) ).
cnf(t706,plain,
$false,
inference(connection,[status(thm),parent(t705:1)],[t705:1,t688:7]) ).
cnf(t707,plain,
$false,
inference(reduction,[status(thm),parent(t705:2)],[t705:2,t686:2]) ).
cnf(t708,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t688:8)],[f_1_29]) ).
cnf(t709,plain,
$false,
inference(connection,[status(thm),parent(t708:1)],[t708:1,t688:8]) ).
cnf(t710,plain,
$false,
inference(reduction,[status(thm),parent(t708:2)],[t708:2,t686:2]) ).
cnf(t711,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t688:9)],[f_1_28]) ).
cnf(t712,plain,
$false,
inference(connection,[status(thm),parent(t711:1)],[t711:1,t688:9]) ).
cnf(t713,plain,
$false,
inference(reduction,[status(thm),parent(t711:2)],[t711:2,t686:2]) ).
cnf(t714,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t688:10)],[f_1_27]) ).
cnf(t715,plain,
$false,
inference(connection,[status(thm),parent(t714:1)],[t714:1,t688:10]) ).
cnf(t716,plain,
$false,
inference(reduction,[status(thm),parent(t714:2)],[t714:2,t686:2]) ).
cnf(t717,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t688:11)],[f_1_24]) ).
cnf(t718,plain,
$false,
inference(connection,[status(thm),parent(t717:1)],[t717:1,t688:11]) ).
cnf(t719,plain,
$false,
inference(reduction,[status(thm),parent(t717:2)],[t717:2,t686:2]) ).
cnf(t720,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t688:12)],[f_1_23]) ).
cnf(t721,plain,
$false,
inference(connection,[status(thm),parent(t720:1)],[t720:1,t688:12]) ).
cnf(t722,plain,
$false,
inference(reduction,[status(thm),parent(t720:2)],[t720:2,t686:2]) ).
cnf(t723,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t688:13)],[f_1_22]) ).
cnf(t724,plain,
$false,
inference(connection,[status(thm),parent(t723:1)],[t723:1,t688:13]) ).
cnf(t725,plain,
$false,
inference(reduction,[status(thm),parent(t723:2)],[t723:2,t686:2]) ).
cnf(t726,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t688:14)],[f_1_21]) ).
cnf(t727,plain,
$false,
inference(connection,[status(thm),parent(t726:1)],[t726:1,t688:14]) ).
cnf(t728,plain,
$false,
inference(reduction,[status(thm),parent(t726:2)],[t726:2,t686:2]) ).
cnf(t729,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t688:15)],[f_1_26]) ).
cnf(t730,plain,
$false,
inference(connection,[status(thm),parent(t729:1)],[t729:1,t688:15]) ).
cnf(t731,plain,
$false,
inference(reduction,[status(thm),parent(t729:2)],[t729:2,t686:2]) ).
cnf(t732,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t688:16)],[f_1_25]) ).
cnf(t733,plain,
$false,
inference(connection,[status(thm),parent(t732:1)],[t732:1,t688:16]) ).
cnf(t734,plain,
$false,
inference(reduction,[status(thm),parent(t732:2)],[t732:2,t686:2]) ).
cnf(t735,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t688:17)],[f_1_20]) ).
cnf(t736,plain,
$false,
inference(connection,[status(thm),parent(t735:1)],[t735:1,t688:17]) ).
cnf(t737,plain,
$false,
inference(reduction,[status(thm),parent(t735:2)],[t735:2,t686:2]) ).
cnf(t738,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t688:18)],[f_1_19]) ).
cnf(t739,plain,
$false,
inference(connection,[status(thm),parent(t738:1)],[t738:1,t688:18]) ).
cnf(t740,plain,
$false,
inference(reduction,[status(thm),parent(t738:2)],[t738:2,t686:2]) ).
cnf(t741,plain,
( ~ sP1(U_4404,U_4405,U_4406,U_4407,U_4408,U_4409)
| chevy(sK7,sK10) ),
inference(extension,[status(thm),parent(t1:14)],[f_1_41]) ).
cnf(t742,plain,
$false,
inference(connection,[status(thm),parent(t741:1)],[t741:1,t1:14]) ).
cnf(t743,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4404,U_4405,U_4406,U_4407,U_4408,U_4409) ),
inference(extension,[status(thm),parent(t741:2)],[f_1_18]) ).
cnf(t744,plain,
$false,
inference(connection,[status(thm),parent(t743:1)],[t743:1,t741:2]) ).
cnf(t745,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t743:2)],[f_1_36]) ).
cnf(t746,plain,
$false,
inference(connection,[status(thm),parent(t745:1)],[t745:1,t743:2]) ).
cnf(t747,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t745:2)],[f_1_35]) ).
cnf(t748,plain,
$false,
inference(connection,[status(thm),parent(t747:1)],[t747:1,t745:2]) ).
cnf(t749,plain,
$false,
inference(reduction,[status(thm),parent(t747:2)],[t747:2,t743:2]) ).
cnf(t750,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t745:3)],[f_1_34]) ).
cnf(t751,plain,
$false,
inference(connection,[status(thm),parent(t750:1)],[t750:1,t745:3]) ).
cnf(t752,plain,
$false,
inference(reduction,[status(thm),parent(t750:2)],[t750:2,t743:2]) ).
cnf(t753,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t745:4)],[f_1_33]) ).
cnf(t754,plain,
$false,
inference(connection,[status(thm),parent(t753:1)],[t753:1,t745:4]) ).
cnf(t755,plain,
$false,
inference(reduction,[status(thm),parent(t753:2)],[t753:2,t743:2]) ).
cnf(t756,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t745:5)],[f_1_32]) ).
cnf(t757,plain,
$false,
inference(connection,[status(thm),parent(t756:1)],[t756:1,t745:5]) ).
cnf(t758,plain,
$false,
inference(reduction,[status(thm),parent(t756:2)],[t756:2,t743:2]) ).
cnf(t759,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t745:6)],[f_1_31]) ).
cnf(t760,plain,
$false,
inference(connection,[status(thm),parent(t759:1)],[t759:1,t745:6]) ).
cnf(t761,plain,
$false,
inference(reduction,[status(thm),parent(t759:2)],[t759:2,t743:2]) ).
cnf(t762,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t745:7)],[f_1_30]) ).
cnf(t763,plain,
$false,
inference(connection,[status(thm),parent(t762:1)],[t762:1,t745:7]) ).
cnf(t764,plain,
$false,
inference(reduction,[status(thm),parent(t762:2)],[t762:2,t743:2]) ).
cnf(t765,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t745:8)],[f_1_29]) ).
cnf(t766,plain,
$false,
inference(connection,[status(thm),parent(t765:1)],[t765:1,t745:8]) ).
cnf(t767,plain,
$false,
inference(reduction,[status(thm),parent(t765:2)],[t765:2,t743:2]) ).
cnf(t768,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t745:9)],[f_1_28]) ).
cnf(t769,plain,
$false,
inference(connection,[status(thm),parent(t768:1)],[t768:1,t745:9]) ).
cnf(t770,plain,
$false,
inference(reduction,[status(thm),parent(t768:2)],[t768:2,t743:2]) ).
cnf(t771,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t745:10)],[f_1_27]) ).
cnf(t772,plain,
$false,
inference(connection,[status(thm),parent(t771:1)],[t771:1,t745:10]) ).
cnf(t773,plain,
$false,
inference(reduction,[status(thm),parent(t771:2)],[t771:2,t743:2]) ).
cnf(t774,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t745:11)],[f_1_24]) ).
cnf(t775,plain,
$false,
inference(connection,[status(thm),parent(t774:1)],[t774:1,t745:11]) ).
cnf(t776,plain,
$false,
inference(reduction,[status(thm),parent(t774:2)],[t774:2,t743:2]) ).
cnf(t777,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t745:12)],[f_1_23]) ).
cnf(t778,plain,
$false,
inference(connection,[status(thm),parent(t777:1)],[t777:1,t745:12]) ).
cnf(t779,plain,
$false,
inference(reduction,[status(thm),parent(t777:2)],[t777:2,t743:2]) ).
cnf(t780,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t745:13)],[f_1_22]) ).
cnf(t781,plain,
$false,
inference(connection,[status(thm),parent(t780:1)],[t780:1,t745:13]) ).
cnf(t782,plain,
$false,
inference(reduction,[status(thm),parent(t780:2)],[t780:2,t743:2]) ).
cnf(t783,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t745:14)],[f_1_21]) ).
cnf(t784,plain,
$false,
inference(connection,[status(thm),parent(t783:1)],[t783:1,t745:14]) ).
cnf(t785,plain,
$false,
inference(reduction,[status(thm),parent(t783:2)],[t783:2,t743:2]) ).
cnf(t786,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t745:15)],[f_1_26]) ).
cnf(t787,plain,
$false,
inference(connection,[status(thm),parent(t786:1)],[t786:1,t745:15]) ).
cnf(t788,plain,
$false,
inference(reduction,[status(thm),parent(t786:2)],[t786:2,t743:2]) ).
cnf(t789,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t745:16)],[f_1_25]) ).
cnf(t790,plain,
$false,
inference(connection,[status(thm),parent(t789:1)],[t789:1,t745:16]) ).
cnf(t791,plain,
$false,
inference(reduction,[status(thm),parent(t789:2)],[t789:2,t743:2]) ).
cnf(t792,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t745:17)],[f_1_20]) ).
cnf(t793,plain,
$false,
inference(connection,[status(thm),parent(t792:1)],[t792:1,t745:17]) ).
cnf(t794,plain,
$false,
inference(reduction,[status(thm),parent(t792:2)],[t792:2,t743:2]) ).
cnf(t795,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t745:18)],[f_1_19]) ).
cnf(t796,plain,
$false,
inference(connection,[status(thm),parent(t795:1)],[t795:1,t745:18]) ).
cnf(t797,plain,
$false,
inference(reduction,[status(thm),parent(t795:2)],[t795:2,t743:2]) ).
cnf(t798,plain,
( ~ sP1(U_4530,U_4531,U_4532,U_4533,U_4534,U_4535)
| lonely(sK7,sK9) ),
inference(extension,[status(thm),parent(t1:15)],[f_1_40]) ).
cnf(t799,plain,
$false,
inference(connection,[status(thm),parent(t798:1)],[t798:1,t1:15]) ).
cnf(t800,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4530,U_4531,U_4532,U_4533,U_4534,U_4535) ),
inference(extension,[status(thm),parent(t798:2)],[f_1_18]) ).
cnf(t801,plain,
$false,
inference(connection,[status(thm),parent(t800:1)],[t800:1,t798:2]) ).
cnf(t802,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t800:2)],[f_1_36]) ).
cnf(t803,plain,
$false,
inference(connection,[status(thm),parent(t802:1)],[t802:1,t800:2]) ).
cnf(t804,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t802:2)],[f_1_35]) ).
cnf(t805,plain,
$false,
inference(connection,[status(thm),parent(t804:1)],[t804:1,t802:2]) ).
cnf(t806,plain,
$false,
inference(reduction,[status(thm),parent(t804:2)],[t804:2,t800:2]) ).
cnf(t807,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t802:3)],[f_1_34]) ).
cnf(t808,plain,
$false,
inference(connection,[status(thm),parent(t807:1)],[t807:1,t802:3]) ).
cnf(t809,plain,
$false,
inference(reduction,[status(thm),parent(t807:2)],[t807:2,t800:2]) ).
cnf(t810,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t802:4)],[f_1_33]) ).
cnf(t811,plain,
$false,
inference(connection,[status(thm),parent(t810:1)],[t810:1,t802:4]) ).
cnf(t812,plain,
$false,
inference(reduction,[status(thm),parent(t810:2)],[t810:2,t800:2]) ).
cnf(t813,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t802:5)],[f_1_32]) ).
cnf(t814,plain,
$false,
inference(connection,[status(thm),parent(t813:1)],[t813:1,t802:5]) ).
cnf(t815,plain,
$false,
inference(reduction,[status(thm),parent(t813:2)],[t813:2,t800:2]) ).
cnf(t816,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t802:6)],[f_1_31]) ).
cnf(t817,plain,
$false,
inference(connection,[status(thm),parent(t816:1)],[t816:1,t802:6]) ).
cnf(t818,plain,
$false,
inference(reduction,[status(thm),parent(t816:2)],[t816:2,t800:2]) ).
cnf(t819,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t802:7)],[f_1_30]) ).
cnf(t820,plain,
$false,
inference(connection,[status(thm),parent(t819:1)],[t819:1,t802:7]) ).
cnf(t821,plain,
$false,
inference(reduction,[status(thm),parent(t819:2)],[t819:2,t800:2]) ).
cnf(t822,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t802:8)],[f_1_29]) ).
cnf(t823,plain,
$false,
inference(connection,[status(thm),parent(t822:1)],[t822:1,t802:8]) ).
cnf(t824,plain,
$false,
inference(reduction,[status(thm),parent(t822:2)],[t822:2,t800:2]) ).
cnf(t825,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t802:9)],[f_1_28]) ).
cnf(t826,plain,
$false,
inference(connection,[status(thm),parent(t825:1)],[t825:1,t802:9]) ).
cnf(t827,plain,
$false,
inference(reduction,[status(thm),parent(t825:2)],[t825:2,t800:2]) ).
cnf(t828,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t802:10)],[f_1_27]) ).
cnf(t829,plain,
$false,
inference(connection,[status(thm),parent(t828:1)],[t828:1,t802:10]) ).
cnf(t830,plain,
$false,
inference(reduction,[status(thm),parent(t828:2)],[t828:2,t800:2]) ).
cnf(t831,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t802:11)],[f_1_24]) ).
cnf(t832,plain,
$false,
inference(connection,[status(thm),parent(t831:1)],[t831:1,t802:11]) ).
cnf(t833,plain,
$false,
inference(reduction,[status(thm),parent(t831:2)],[t831:2,t800:2]) ).
cnf(t834,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t802:12)],[f_1_23]) ).
cnf(t835,plain,
$false,
inference(connection,[status(thm),parent(t834:1)],[t834:1,t802:12]) ).
cnf(t836,plain,
$false,
inference(reduction,[status(thm),parent(t834:2)],[t834:2,t800:2]) ).
cnf(t837,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t802:13)],[f_1_22]) ).
cnf(t838,plain,
$false,
inference(connection,[status(thm),parent(t837:1)],[t837:1,t802:13]) ).
cnf(t839,plain,
$false,
inference(reduction,[status(thm),parent(t837:2)],[t837:2,t800:2]) ).
cnf(t840,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t802:14)],[f_1_21]) ).
cnf(t841,plain,
$false,
inference(connection,[status(thm),parent(t840:1)],[t840:1,t802:14]) ).
cnf(t842,plain,
$false,
inference(reduction,[status(thm),parent(t840:2)],[t840:2,t800:2]) ).
cnf(t843,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t802:15)],[f_1_26]) ).
cnf(t844,plain,
$false,
inference(connection,[status(thm),parent(t843:1)],[t843:1,t802:15]) ).
cnf(t845,plain,
$false,
inference(reduction,[status(thm),parent(t843:2)],[t843:2,t800:2]) ).
cnf(t846,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t802:16)],[f_1_25]) ).
cnf(t847,plain,
$false,
inference(connection,[status(thm),parent(t846:1)],[t846:1,t802:16]) ).
cnf(t848,plain,
$false,
inference(reduction,[status(thm),parent(t846:2)],[t846:2,t800:2]) ).
cnf(t849,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t802:17)],[f_1_20]) ).
cnf(t850,plain,
$false,
inference(connection,[status(thm),parent(t849:1)],[t849:1,t802:17]) ).
cnf(t851,plain,
$false,
inference(reduction,[status(thm),parent(t849:2)],[t849:2,t800:2]) ).
cnf(t852,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t802:18)],[f_1_19]) ).
cnf(t853,plain,
$false,
inference(connection,[status(thm),parent(t852:1)],[t852:1,t802:18]) ).
cnf(t854,plain,
$false,
inference(reduction,[status(thm),parent(t852:2)],[t852:2,t800:2]) ).
cnf(t855,plain,
( ~ sP1(U_4656,U_4657,U_4658,U_4659,U_4660,U_4661)
| street(sK7,sK9) ),
inference(extension,[status(thm),parent(t1:16)],[f_1_39]) ).
cnf(t856,plain,
$false,
inference(connection,[status(thm),parent(t855:1)],[t855:1,t1:16]) ).
cnf(t857,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4656,U_4657,U_4658,U_4659,U_4660,U_4661) ),
inference(extension,[status(thm),parent(t855:2)],[f_1_18]) ).
cnf(t858,plain,
$false,
inference(connection,[status(thm),parent(t857:1)],[t857:1,t855:2]) ).
cnf(t859,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t857:2)],[f_1_36]) ).
cnf(t860,plain,
$false,
inference(connection,[status(thm),parent(t859:1)],[t859:1,t857:2]) ).
cnf(t861,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t859:2)],[f_1_35]) ).
cnf(t862,plain,
$false,
inference(connection,[status(thm),parent(t861:1)],[t861:1,t859:2]) ).
cnf(t863,plain,
$false,
inference(reduction,[status(thm),parent(t861:2)],[t861:2,t857:2]) ).
cnf(t864,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t859:3)],[f_1_34]) ).
cnf(t865,plain,
$false,
inference(connection,[status(thm),parent(t864:1)],[t864:1,t859:3]) ).
cnf(t866,plain,
$false,
inference(reduction,[status(thm),parent(t864:2)],[t864:2,t857:2]) ).
cnf(t867,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t859:4)],[f_1_33]) ).
cnf(t868,plain,
$false,
inference(connection,[status(thm),parent(t867:1)],[t867:1,t859:4]) ).
cnf(t869,plain,
$false,
inference(reduction,[status(thm),parent(t867:2)],[t867:2,t857:2]) ).
cnf(t870,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t859:5)],[f_1_32]) ).
cnf(t871,plain,
$false,
inference(connection,[status(thm),parent(t870:1)],[t870:1,t859:5]) ).
cnf(t872,plain,
$false,
inference(reduction,[status(thm),parent(t870:2)],[t870:2,t857:2]) ).
cnf(t873,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t859:6)],[f_1_31]) ).
cnf(t874,plain,
$false,
inference(connection,[status(thm),parent(t873:1)],[t873:1,t859:6]) ).
cnf(t875,plain,
$false,
inference(reduction,[status(thm),parent(t873:2)],[t873:2,t857:2]) ).
cnf(t876,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t859:7)],[f_1_30]) ).
cnf(t877,plain,
$false,
inference(connection,[status(thm),parent(t876:1)],[t876:1,t859:7]) ).
cnf(t878,plain,
$false,
inference(reduction,[status(thm),parent(t876:2)],[t876:2,t857:2]) ).
cnf(t879,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t859:8)],[f_1_29]) ).
cnf(t880,plain,
$false,
inference(connection,[status(thm),parent(t879:1)],[t879:1,t859:8]) ).
cnf(t881,plain,
$false,
inference(reduction,[status(thm),parent(t879:2)],[t879:2,t857:2]) ).
cnf(t882,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t859:9)],[f_1_28]) ).
cnf(t883,plain,
$false,
inference(connection,[status(thm),parent(t882:1)],[t882:1,t859:9]) ).
cnf(t884,plain,
$false,
inference(reduction,[status(thm),parent(t882:2)],[t882:2,t857:2]) ).
cnf(t885,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t859:10)],[f_1_27]) ).
cnf(t886,plain,
$false,
inference(connection,[status(thm),parent(t885:1)],[t885:1,t859:10]) ).
cnf(t887,plain,
$false,
inference(reduction,[status(thm),parent(t885:2)],[t885:2,t857:2]) ).
cnf(t888,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t859:11)],[f_1_24]) ).
cnf(t889,plain,
$false,
inference(connection,[status(thm),parent(t888:1)],[t888:1,t859:11]) ).
cnf(t890,plain,
$false,
inference(reduction,[status(thm),parent(t888:2)],[t888:2,t857:2]) ).
cnf(t891,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t859:12)],[f_1_23]) ).
cnf(t892,plain,
$false,
inference(connection,[status(thm),parent(t891:1)],[t891:1,t859:12]) ).
cnf(t893,plain,
$false,
inference(reduction,[status(thm),parent(t891:2)],[t891:2,t857:2]) ).
cnf(t894,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t859:13)],[f_1_22]) ).
cnf(t895,plain,
$false,
inference(connection,[status(thm),parent(t894:1)],[t894:1,t859:13]) ).
cnf(t896,plain,
$false,
inference(reduction,[status(thm),parent(t894:2)],[t894:2,t857:2]) ).
cnf(t897,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t859:14)],[f_1_21]) ).
cnf(t898,plain,
$false,
inference(connection,[status(thm),parent(t897:1)],[t897:1,t859:14]) ).
cnf(t899,plain,
$false,
inference(reduction,[status(thm),parent(t897:2)],[t897:2,t857:2]) ).
cnf(t900,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t859:15)],[f_1_26]) ).
cnf(t901,plain,
$false,
inference(connection,[status(thm),parent(t900:1)],[t900:1,t859:15]) ).
cnf(t902,plain,
$false,
inference(reduction,[status(thm),parent(t900:2)],[t900:2,t857:2]) ).
cnf(t903,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t859:16)],[f_1_25]) ).
cnf(t904,plain,
$false,
inference(connection,[status(thm),parent(t903:1)],[t903:1,t859:16]) ).
cnf(t905,plain,
$false,
inference(reduction,[status(thm),parent(t903:2)],[t903:2,t857:2]) ).
cnf(t906,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t859:17)],[f_1_20]) ).
cnf(t907,plain,
$false,
inference(connection,[status(thm),parent(t906:1)],[t906:1,t859:17]) ).
cnf(t908,plain,
$false,
inference(reduction,[status(thm),parent(t906:2)],[t906:2,t857:2]) ).
cnf(t909,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t859:18)],[f_1_19]) ).
cnf(t910,plain,
$false,
inference(connection,[status(thm),parent(t909:1)],[t909:1,t859:18]) ).
cnf(t911,plain,
$false,
inference(reduction,[status(thm),parent(t909:2)],[t909:2,t857:2]) ).
cnf(t912,plain,
( ~ sP1(U_4782,U_4783,U_4784,U_4785,U_4786,U_4787)
| city(sK7,sK8) ),
inference(extension,[status(thm),parent(t1:17)],[f_1_38]) ).
cnf(t913,plain,
$false,
inference(connection,[status(thm),parent(t912:1)],[t912:1,t1:17]) ).
cnf(t914,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4782,U_4783,U_4784,U_4785,U_4786,U_4787) ),
inference(extension,[status(thm),parent(t912:2)],[f_1_18]) ).
cnf(t915,plain,
$false,
inference(connection,[status(thm),parent(t914:1)],[t914:1,t912:2]) ).
cnf(t916,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t914:2)],[f_1_36]) ).
cnf(t917,plain,
$false,
inference(connection,[status(thm),parent(t916:1)],[t916:1,t914:2]) ).
cnf(t918,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t916:2)],[f_1_35]) ).
cnf(t919,plain,
$false,
inference(connection,[status(thm),parent(t918:1)],[t918:1,t916:2]) ).
cnf(t920,plain,
$false,
inference(reduction,[status(thm),parent(t918:2)],[t918:2,t914:2]) ).
cnf(t921,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t916:3)],[f_1_34]) ).
cnf(t922,plain,
$false,
inference(connection,[status(thm),parent(t921:1)],[t921:1,t916:3]) ).
cnf(t923,plain,
$false,
inference(reduction,[status(thm),parent(t921:2)],[t921:2,t914:2]) ).
cnf(t924,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t916:4)],[f_1_33]) ).
cnf(t925,plain,
$false,
inference(connection,[status(thm),parent(t924:1)],[t924:1,t916:4]) ).
cnf(t926,plain,
$false,
inference(reduction,[status(thm),parent(t924:2)],[t924:2,t914:2]) ).
cnf(t927,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t916:5)],[f_1_32]) ).
cnf(t928,plain,
$false,
inference(connection,[status(thm),parent(t927:1)],[t927:1,t916:5]) ).
cnf(t929,plain,
$false,
inference(reduction,[status(thm),parent(t927:2)],[t927:2,t914:2]) ).
cnf(t930,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t916:6)],[f_1_31]) ).
cnf(t931,plain,
$false,
inference(connection,[status(thm),parent(t930:1)],[t930:1,t916:6]) ).
cnf(t932,plain,
$false,
inference(reduction,[status(thm),parent(t930:2)],[t930:2,t914:2]) ).
cnf(t933,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t916:7)],[f_1_30]) ).
cnf(t934,plain,
$false,
inference(connection,[status(thm),parent(t933:1)],[t933:1,t916:7]) ).
cnf(t935,plain,
$false,
inference(reduction,[status(thm),parent(t933:2)],[t933:2,t914:2]) ).
cnf(t936,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t916:8)],[f_1_29]) ).
cnf(t937,plain,
$false,
inference(connection,[status(thm),parent(t936:1)],[t936:1,t916:8]) ).
cnf(t938,plain,
$false,
inference(reduction,[status(thm),parent(t936:2)],[t936:2,t914:2]) ).
cnf(t939,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t916:9)],[f_1_28]) ).
cnf(t940,plain,
$false,
inference(connection,[status(thm),parent(t939:1)],[t939:1,t916:9]) ).
cnf(t941,plain,
$false,
inference(reduction,[status(thm),parent(t939:2)],[t939:2,t914:2]) ).
cnf(t942,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t916:10)],[f_1_27]) ).
cnf(t943,plain,
$false,
inference(connection,[status(thm),parent(t942:1)],[t942:1,t916:10]) ).
cnf(t944,plain,
$false,
inference(reduction,[status(thm),parent(t942:2)],[t942:2,t914:2]) ).
cnf(t945,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t916:11)],[f_1_24]) ).
cnf(t946,plain,
$false,
inference(connection,[status(thm),parent(t945:1)],[t945:1,t916:11]) ).
cnf(t947,plain,
$false,
inference(reduction,[status(thm),parent(t945:2)],[t945:2,t914:2]) ).
cnf(t948,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t916:12)],[f_1_23]) ).
cnf(t949,plain,
$false,
inference(connection,[status(thm),parent(t948:1)],[t948:1,t916:12]) ).
cnf(t950,plain,
$false,
inference(reduction,[status(thm),parent(t948:2)],[t948:2,t914:2]) ).
cnf(t951,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t916:13)],[f_1_22]) ).
cnf(t952,plain,
$false,
inference(connection,[status(thm),parent(t951:1)],[t951:1,t916:13]) ).
cnf(t953,plain,
$false,
inference(reduction,[status(thm),parent(t951:2)],[t951:2,t914:2]) ).
cnf(t954,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t916:14)],[f_1_21]) ).
cnf(t955,plain,
$false,
inference(connection,[status(thm),parent(t954:1)],[t954:1,t916:14]) ).
cnf(t956,plain,
$false,
inference(reduction,[status(thm),parent(t954:2)],[t954:2,t914:2]) ).
cnf(t957,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t916:15)],[f_1_26]) ).
cnf(t958,plain,
$false,
inference(connection,[status(thm),parent(t957:1)],[t957:1,t916:15]) ).
cnf(t959,plain,
$false,
inference(reduction,[status(thm),parent(t957:2)],[t957:2,t914:2]) ).
cnf(t960,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t916:16)],[f_1_25]) ).
cnf(t961,plain,
$false,
inference(connection,[status(thm),parent(t960:1)],[t960:1,t916:16]) ).
cnf(t962,plain,
$false,
inference(reduction,[status(thm),parent(t960:2)],[t960:2,t914:2]) ).
cnf(t963,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t916:17)],[f_1_20]) ).
cnf(t964,plain,
$false,
inference(connection,[status(thm),parent(t963:1)],[t963:1,t916:17]) ).
cnf(t965,plain,
$false,
inference(reduction,[status(thm),parent(t963:2)],[t963:2,t914:2]) ).
cnf(t966,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t916:18)],[f_1_19]) ).
cnf(t967,plain,
$false,
inference(connection,[status(thm),parent(t966:1)],[t966:1,t916:18]) ).
cnf(t968,plain,
$false,
inference(reduction,[status(thm),parent(t966:2)],[t966:2,t914:2]) ).
cnf(t969,plain,
( ~ sP1(U_4908,U_4909,U_4910,U_4911,U_4912,U_4913)
| actual_world(sK7) ),
inference(extension,[status(thm),parent(t1:18)],[f_1_37]) ).
cnf(t970,plain,
$false,
inference(connection,[status(thm),parent(t969:1)],[t969:1,t1:18]) ).
cnf(t971,plain,
( sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| sP1(U_4908,U_4909,U_4910,U_4911,U_4912,U_4913) ),
inference(extension,[status(thm),parent(t969:2)],[f_1_18]) ).
cnf(t972,plain,
$false,
inference(connection,[status(thm),parent(t971:1)],[t971:1,t969:2]) ).
cnf(t973,plain,
( ~ actual_world(sK1)
| ~ city(sK1,sK2)
| ~ street(sK1,sK4)
| ~ lonely(sK1,sK4)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK2)
| ~ of(sK1,sK6,sK2)
| ~ hollywood_placename(sK1,sK6)
| ~ placename(sK1,sK6)
| ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1) ),
inference(extension,[status(thm),parent(t971:2)],[f_1_36]) ).
cnf(t974,plain,
$false,
inference(connection,[status(thm),parent(t973:1)],[t973:1,t971:2]) ).
cnf(t975,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t973:2)],[f_1_35]) ).
cnf(t976,plain,
$false,
inference(connection,[status(thm),parent(t975:1)],[t975:1,t973:2]) ).
cnf(t977,plain,
$false,
inference(reduction,[status(thm),parent(t975:2)],[t975:2,t971:2]) ).
cnf(t978,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| hollywood_placename(sK1,sK6) ),
inference(extension,[status(thm),parent(t973:3)],[f_1_34]) ).
cnf(t979,plain,
$false,
inference(connection,[status(thm),parent(t978:1)],[t978:1,t973:3]) ).
cnf(t980,plain,
$false,
inference(reduction,[status(thm),parent(t978:2)],[t978:2,t971:2]) ).
cnf(t981,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| of(sK1,sK6,sK2) ),
inference(extension,[status(thm),parent(t973:4)],[f_1_33]) ).
cnf(t982,plain,
$false,
inference(connection,[status(thm),parent(t981:1)],[t981:1,t973:4]) ).
cnf(t983,plain,
$false,
inference(reduction,[status(thm),parent(t981:2)],[t981:2,t971:2]) ).
cnf(t984,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| in(sK1,sK5,sK2) ),
inference(extension,[status(thm),parent(t973:5)],[f_1_32]) ).
cnf(t985,plain,
$false,
inference(connection,[status(thm),parent(t984:1)],[t984:1,t973:5]) ).
cnf(t986,plain,
$false,
inference(reduction,[status(thm),parent(t984:2)],[t984:2,t971:2]) ).
cnf(t987,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| down(sK1,sK5,sK4) ),
inference(extension,[status(thm),parent(t973:6)],[f_1_31]) ).
cnf(t988,plain,
$false,
inference(connection,[status(thm),parent(t987:1)],[t987:1,t973:6]) ).
cnf(t989,plain,
$false,
inference(reduction,[status(thm),parent(t987:2)],[t987:2,t971:2]) ).
cnf(t990,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| barrel(sK1,sK5) ),
inference(extension,[status(thm),parent(t973:7)],[f_1_30]) ).
cnf(t991,plain,
$false,
inference(connection,[status(thm),parent(t990:1)],[t990:1,t973:7]) ).
cnf(t992,plain,
$false,
inference(reduction,[status(thm),parent(t990:2)],[t990:2,t971:2]) ).
cnf(t993,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| present(sK1,sK5) ),
inference(extension,[status(thm),parent(t973:8)],[f_1_29]) ).
cnf(t994,plain,
$false,
inference(connection,[status(thm),parent(t993:1)],[t993:1,t973:8]) ).
cnf(t995,plain,
$false,
inference(reduction,[status(thm),parent(t993:2)],[t993:2,t971:2]) ).
cnf(t996,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| agent(sK1,sK5,sK3) ),
inference(extension,[status(thm),parent(t973:9)],[f_1_28]) ).
cnf(t997,plain,
$false,
inference(connection,[status(thm),parent(t996:1)],[t996:1,t973:9]) ).
cnf(t998,plain,
$false,
inference(reduction,[status(thm),parent(t996:2)],[t996:2,t971:2]) ).
cnf(t999,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| event(sK1,sK5) ),
inference(extension,[status(thm),parent(t973:10)],[f_1_27]) ).
cnf(t1000,plain,
$false,
inference(connection,[status(thm),parent(t999:1)],[t999:1,t973:10]) ).
cnf(t1001,plain,
$false,
inference(reduction,[status(thm),parent(t999:2)],[t999:2,t971:2]) ).
cnf(t1002,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| old(sK1,sK3) ),
inference(extension,[status(thm),parent(t973:11)],[f_1_24]) ).
cnf(t1003,plain,
$false,
inference(connection,[status(thm),parent(t1002:1)],[t1002:1,t973:11]) ).
cnf(t1004,plain,
$false,
inference(reduction,[status(thm),parent(t1002:2)],[t1002:2,t971:2]) ).
cnf(t1005,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| dirty(sK1,sK3) ),
inference(extension,[status(thm),parent(t973:12)],[f_1_23]) ).
cnf(t1006,plain,
$false,
inference(connection,[status(thm),parent(t1005:1)],[t1005:1,t973:12]) ).
cnf(t1007,plain,
$false,
inference(reduction,[status(thm),parent(t1005:2)],[t1005:2,t971:2]) ).
cnf(t1008,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| white(sK1,sK3) ),
inference(extension,[status(thm),parent(t973:13)],[f_1_22]) ).
cnf(t1009,plain,
$false,
inference(connection,[status(thm),parent(t1008:1)],[t1008:1,t973:13]) ).
cnf(t1010,plain,
$false,
inference(reduction,[status(thm),parent(t1008:2)],[t1008:2,t971:2]) ).
cnf(t1011,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| chevy(sK1,sK3) ),
inference(extension,[status(thm),parent(t973:14)],[f_1_21]) ).
cnf(t1012,plain,
$false,
inference(connection,[status(thm),parent(t1011:1)],[t1011:1,t973:14]) ).
cnf(t1013,plain,
$false,
inference(reduction,[status(thm),parent(t1011:2)],[t1011:2,t971:2]) ).
cnf(t1014,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| lonely(sK1,sK4) ),
inference(extension,[status(thm),parent(t973:15)],[f_1_26]) ).
cnf(t1015,plain,
$false,
inference(connection,[status(thm),parent(t1014:1)],[t1014:1,t973:15]) ).
cnf(t1016,plain,
$false,
inference(reduction,[status(thm),parent(t1014:2)],[t1014:2,t971:2]) ).
cnf(t1017,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| street(sK1,sK4) ),
inference(extension,[status(thm),parent(t973:16)],[f_1_25]) ).
cnf(t1018,plain,
$false,
inference(connection,[status(thm),parent(t1017:1)],[t1017:1,t973:16]) ).
cnf(t1019,plain,
$false,
inference(reduction,[status(thm),parent(t1017:2)],[t1017:2,t971:2]) ).
cnf(t1020,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| city(sK1,sK2) ),
inference(extension,[status(thm),parent(t973:17)],[f_1_20]) ).
cnf(t1021,plain,
$false,
inference(connection,[status(thm),parent(t1020:1)],[t1020:1,t973:17]) ).
cnf(t1022,plain,
$false,
inference(reduction,[status(thm),parent(t1020:2)],[t1020:2,t971:2]) ).
cnf(t1023,plain,
( ~ sP0(sK3,sK4,sK6,sK5,sK2,sK1)
| actual_world(sK1) ),
inference(extension,[status(thm),parent(t973:18)],[f_1_19]) ).
cnf(t1024,plain,
$false,
inference(connection,[status(thm),parent(t1023:1)],[t1023:1,t973:18]) ).
cnf(t1025,plain,
$false,
inference(reduction,[status(thm),parent(t1023:2)],[t1023:2,t971:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP117+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.38 % Computer : n006.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Sat Sep 19 16:54:45 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.15/11.00 % SZS status Theorem for theBenchmark
% 0.15/11.00 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------