%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP117+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 11:59:38 AM UTC 2025
% Result : Theorem 2.52s 0.70s
% Output : CNFRefutation 2.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 1
% Syntax : Number of formulae : 381 ( 1 unt; 0 def)
% Number of atoms : 1229 ( 0 equ)
% Maximal formula atoms : 68 ( 3 avg)
% Number of connectives : 1552 ( 704 ~; 714 |; 130 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-6 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 270 ( 210 sgn 0 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,plain,
~ ~ ( ( ? [U] :
( actual_world(U)
& ? [V,W,X,Y,Z] :
( of(U,W,V)
& city(U,V)
& hollywood_placename(U,W)
& placename(U,W)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& street(U,Y)
& lonely(U,Y)
& event(U,Z)
& agent(U,Z,X)
& present(U,Z)
& barrel(U,Z)
& down(U,Z,Y)
& in(U,Z,V) ) )
=> ? [X1] :
( actual_world(X1)
& ? [X2,X3,X4,X5,X6] :
( of(X1,X3,X2)
& city(X1,X2)
& hollywood_placename(X1,X3)
& placename(X1,X3)
& street(X1,X4)
& lonely(X1,X4)
& chevy(X1,X5)
& white(X1,X5)
& dirty(X1,X5)
& old(X1,X5)
& event(X1,X6)
& agent(X1,X6,X5)
& present(X1,X6)
& barrel(X1,X6)
& down(X1,X6,X4)
& in(X1,X6,X2) ) ) )
& ( ? [X1] :
( actual_world(X1)
& ? [X2,X3,X4,X5,X6] :
( of(X1,X3,X2)
& city(X1,X2)
& hollywood_placename(X1,X3)
& placename(X1,X3)
& street(X1,X4)
& lonely(X1,X4)
& chevy(X1,X5)
& white(X1,X5)
& dirty(X1,X5)
& old(X1,X5)
& event(X1,X6)
& agent(X1,X6,X5)
& present(X1,X6)
& barrel(X1,X6)
& down(X1,X6,X4)
& in(X1,X6,X2) ) )
=> ? [U] :
( actual_world(U)
& ? [V,W,X,Y,Z] :
( of(U,W,V)
& city(U,V)
& hollywood_placename(U,W)
& placename(U,W)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& street(U,Y)
& lonely(U,Y)
& event(U,Z)
& agent(U,Z,X)
& present(U,Z)
& barrel(U,Z)
& down(U,Z,Y)
& in(U,Z,V) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(co1_negated,plain,
~ ~ ~ ( ( ? [U] :
( actual_world(U)
& ? [V,W,X,Y,Z] :
( of(U,W,V)
& city(U,V)
& hollywood_placename(U,W)
& placename(U,W)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& street(U,Y)
& lonely(U,Y)
& event(U,Z)
& agent(U,Z,X)
& present(U,Z)
& barrel(U,Z)
& down(U,Z,Y)
& in(U,Z,V) ) )
=> ? [X1] :
( actual_world(X1)
& ? [X2,X3,X4,X5,X6] :
( of(X1,X3,X2)
& city(X1,X2)
& hollywood_placename(X1,X3)
& placename(X1,X3)
& street(X1,X4)
& lonely(X1,X4)
& chevy(X1,X5)
& white(X1,X5)
& dirty(X1,X5)
& old(X1,X5)
& event(X1,X6)
& agent(X1,X6,X5)
& present(X1,X6)
& barrel(X1,X6)
& down(X1,X6,X4)
& in(X1,X6,X2) ) ) )
& ( ? [X1] :
( actual_world(X1)
& ? [X2,X3,X4,X5,X6] :
( of(X1,X3,X2)
& city(X1,X2)
& hollywood_placename(X1,X3)
& placename(X1,X3)
& street(X1,X4)
& lonely(X1,X4)
& chevy(X1,X5)
& white(X1,X5)
& dirty(X1,X5)
& old(X1,X5)
& event(X1,X6)
& agent(X1,X6,X5)
& present(X1,X6)
& barrel(X1,X6)
& down(X1,X6,X4)
& in(X1,X6,X2) ) )
=> ? [U] :
( actual_world(U)
& ? [V,W,X,Y,Z] :
( of(U,W,V)
& city(U,V)
& hollywood_placename(U,W)
& placename(U,W)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& street(U,Y)
& lonely(U,Y)
& event(U,Z)
& agent(U,Z,X)
& present(U,Z)
& barrel(U,Z)
& down(U,Z,Y)
& in(U,Z,V) ) ) ) ),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(0,plain,
( actual_world(sK1)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l0,plain,
( actual_world(sK1)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(29,plain,
( lonely(sK7,sK10)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l2,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(18,plain,
( ~ street(X0,X1)
| ~ city(X0,X2)
| ~ lonely(X0,X1)
| ~ event(X0,X3)
| ~ agent(X0,X3,X4)
| ~ actual_world(X0)
| ~ of(X0,X5,X2)
| ~ hollywood_placename(X0,X5)
| ~ placename(X0,X5)
| ~ chevy(X0,X4)
| ~ white(X0,X4)
| ~ dirty(X0,X4)
| ~ old(X0,X4)
| ~ present(X0,X3)
| ~ barrel(X0,X3)
| ~ down(X0,X3,X1)
| ~ in(X0,X3,X2)
| ~ sP0(X4,X5,X3,X1,X2,X0) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l25,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(20,plain,
( down(sK7,sK12,sK10)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l61,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(26,plain,
( dirty(sK7,sK11)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l60,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(25,plain,
( old(sK7,sK11)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l62,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(28,plain,
( chevy(sK7,sK11)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l41,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(17,plain,
( ~ street(X0,X1)
| ~ city(X0,X2)
| ~ lonely(X0,X1)
| ~ event(X0,X3)
| ~ agent(X0,X3,X4)
| ~ actual_world(X0)
| ~ of(X0,X5,X2)
| ~ hollywood_placename(X0,X5)
| ~ placename(X0,X5)
| ~ chevy(X0,X4)
| ~ white(X0,X4)
| ~ dirty(X0,X4)
| ~ old(X0,X4)
| ~ present(X0,X3)
| ~ barrel(X0,X3)
| ~ down(X0,X3,X1)
| ~ in(X0,X3,X2)
| sP0(X6,X7,X8,X9,X10,X11) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1,plain,
( ~ street(sK1,sK5)
| ~ city(sK1,sK2)
| ~ lonely(sK1,sK5)
| ~ event(sK1,sK6)
| ~ agent(sK1,sK6,sK4)
| ~ actual_world(sK1)
| ~ of(sK1,sK3,sK2)
| ~ hollywood_placename(sK1,sK3)
| ~ placename(sK1,sK3)
| ~ chevy(sK1,sK4)
| ~ white(sK1,sK4)
| ~ dirty(sK1,sK4)
| ~ old(sK1,sK4)
| ~ present(sK1,sK6)
| ~ barrel(sK1,sK6)
| ~ down(sK1,sK6,sK5)
| ~ in(sK1,sK6,sK2)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(4,plain,
( placename(sK1,sK3)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l55,plain,
( placename(sK1,sK3)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(14,plain,
( barrel(sK1,sK6)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l20,plain,
( barrel(sK1,sK6)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(34,plain,
( of(sK7,sK9,sK8)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l71,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(8,plain,
( old(sK1,sK4)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l69,plain,
( old(sK1,sK4)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(35,plain,
( actual_world(sK7)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l59,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(13,plain,
( present(sK1,sK6)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l52,plain,
( present(sK1,sK6)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(32,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l28,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(23,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l42,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(10,plain,
( lonely(sK1,sK5)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l12,plain,
( lonely(sK1,sK5)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l76,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(19,plain,
( in(sK7,sK12,sK8)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l190,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(15,plain,
( down(sK1,sK6,sK5)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l10,plain,
( down(sK1,sK6,sK5)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(1,plain,
( of(sK1,sK3,sK2)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l13,plain,
( of(sK1,sK3,sK2)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l191,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l100,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(12,plain,
( agent(sK1,sK6,sK4)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l3,plain,
( agent(sK1,sK6,sK4)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l284,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(6,plain,
( white(sK1,sK4)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l34,plain,
( white(sK1,sK4)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(2,plain,
( city(sK1,sK2)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l8,plain,
( city(sK1,sK2)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(24,plain,
( event(sK7,sK12)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l38,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l73,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(33,plain,
( city(sK7,sK8)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l186,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(21,plain,
( barrel(sK7,sK12)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l64,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l267,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l209,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l19,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(11,plain,
( event(sK1,sK6)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l39,plain,
( event(sK1,sK6)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l310,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(22,plain,
( present(sK7,sK12)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l250,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l257,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(31,plain,
( placename(sK7,sK9)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l26,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(27,plain,
( white(sK7,sK11)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l259,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l188,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l295,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l252,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l254,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l258,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l260,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l68,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l101,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(30,plain,
( street(sK7,sK10)
| ~ sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l74,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l208,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l293,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l296,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l189,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l105,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l314,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l37,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l264,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l297,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l313,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l78,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l206,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(5,plain,
( chevy(sK1,sK4)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l11,plain,
( chevy(sK1,sK4)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l253,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l240,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l249,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l43,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l304,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l72,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l181,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l65,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(16,plain,
( in(sK1,sK6,sK2)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l23,plain,
( in(sK1,sK6,sK2)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l322,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l330,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l16,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l333,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l291,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l182,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l325,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l184,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l176,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l31,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l14,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l118,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l326,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l207,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l327,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l315,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l21,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l36,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l331,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l110,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l108,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l179,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l245,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l248,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l67,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(9,plain,
( street(sK1,sK5)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l4,plain,
( street(sK1,sK5)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l48,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l228,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l332,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l107,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l323,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l218,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l180,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l63,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l35,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l236,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l266,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l212,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l123,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l294,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l177,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l120,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l229,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l109,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l230,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l329,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l328,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(3,plain,
( hollywood_placename(sK1,sK3)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l6,plain,
( hollywood_placename(sK1,sK3)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l47,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l54,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l160,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l134,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l183,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l251,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l49,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l269,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l40,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l324,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l303,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l102,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l320,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l273,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l272,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l122,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l187,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l157,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l143,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l152,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l275,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l45,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l268,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l306,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l185,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l154,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(7,plain,
( dirty(sK1,sK4)
| sP0(X0,X1,X2,X3,X4,X5) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l5,plain,
( dirty(sK1,sK4)
| sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l79,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l270,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l29,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l85,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l274,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l88,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l169,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l321,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l219,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l111,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l279,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l193,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l289,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l255,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l318,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l316,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l215,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l24,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l156,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l319,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l129,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l124,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l335,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l117,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l344,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l163,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l162,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l175,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l75,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l161,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l18,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l281,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l217,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l165,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l22,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l205,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l170,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l99,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l282,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l201,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l33,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l202,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l338,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l70,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l17,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l232,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l204,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l235,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l139,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l168,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l214,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l87,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l213,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l317,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l166,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l227,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l311,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l277,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l278,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l233,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l210,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l246,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l9,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l234,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l195,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l66,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l231,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l302,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l140,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l58,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l89,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l271,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l159,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l103,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l155,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l96,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l203,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l194,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l121,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l98,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l137,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l94,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l244,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l32,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l97,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l15,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l151,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l276,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l351,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l81,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l341,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l80,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l116,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l86,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l178,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l95,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l237,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l27,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l146,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l84,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l343,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l300,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l106,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l312,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l82,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l224,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l196,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l44,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l211,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l173,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l199,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l342,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l239,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l216,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l349,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l153,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l280,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l265,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l334,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l299,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l226,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l261,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l347,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l172,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l340,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l135,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l119,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l149,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l308,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l242,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l238,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l56,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l346,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l307,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l225,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l305,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l90,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l142,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l83,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l144,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l339,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l92,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l301,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l256,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l145,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l93,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l171,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l350,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l220,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l167,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l263,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l174,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l241,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l243,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l148,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l150,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l164,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l283,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l200,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l262,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l91,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l53,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l147,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l158,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l223,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l337,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l197,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l104,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l336,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l222,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l247,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l309,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l221,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l348,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l345,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l298,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l198,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l30,plain,
( ~ street(sK7,sK10)
| ~ city(sK7,sK8)
| ~ lonely(sK7,sK10)
| ~ event(sK7,sK12)
| ~ agent(sK7,sK12,sK11)
| ~ actual_world(sK7)
| ~ of(sK7,sK9,sK8)
| ~ hollywood_placename(sK7,sK9)
| ~ placename(sK7,sK9)
| ~ chevy(sK7,sK11)
| ~ white(sK7,sK11)
| ~ dirty(sK7,sK11)
| ~ old(sK7,sK11)
| ~ present(sK7,sK12)
| ~ barrel(sK7,sK12)
| ~ down(sK7,sK12,sK10)
| ~ in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l192,plain,
( city(sK7,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l138,plain,
( dirty(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l136,plain,
( in(sK7,sK12,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l115,plain,
( present(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l113,plain,
( chevy(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l50,plain,
( street(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l132,plain,
( event(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l130,plain,
( down(sK7,sK12,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l126,plain,
( of(sK7,sK9,sK8)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l141,plain,
( lonely(sK7,sK10)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l128,plain,
( old(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l131,plain,
( agent(sK7,sK12,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l125,plain,
( white(sK7,sK11)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l112,plain,
( barrel(sK7,sK12)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l133,plain,
( actual_world(sK7)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l127,plain,
( hollywood_placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l114,plain,
( placename(sK7,sK9)
| ~ sP0(sK11,sK9,sK12,sK10,sK8,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l2,l25,l61,l60,l62,l41,l1,l55,l20,l71,l69,l59,l52,l28,l42,l12,l76,l190,l10,l13,l191,l100,l3,l284,l34,l8,l38,l73,l186,l64,l267,l209,l19,l39,l310,l250,l257,l26,l259,l188,l295,l252,l254,l258,l260,l68,l101,l74,l208,l293,l296,l189,l105,l314,l37,l264,l297,l313,l78,l206,l11,l253,l240,l249,l43,l304,l72,l181,l65,l23,l322,l330,l7,l16,l333,l291,l182,l325,l184,l176,l31,l14,l118,l326,l207,l327,l315,l21,l36,l331,l110,l108,l179,l245,l248,l67,l4,l48,l228,l332,l107,l323,l218,l180,l63,l35,l236,l266,l212,l123,l294,l177,l120,l229,l109,l230,l329,l328,l6,l47,l54,l160,l134,l183,l251,l49,l269,l40,l324,l303,l102,l320,l273,l272,l122,l187,l157,l143,l152,l275,l45,l268,l306,l185,l154,l5,l79,l270,l29,l85,l274,l88,l169,l321,l219,l111,l279,l193,l289,l255,l318,l316,l215,l24,l156,l319,l129,l124,l335,l117,l344,l163,l162,l175,l75,l161,l18,l281,l217,l165,l22,l205,l170,l99,l282,l201,l33,l202,l338,l70,l17,l232,l204,l235,l139,l168,l214,l87,l213,l317,l166,l227,l311,l277,l278,l233,l210,l246,l9,l234,l195,l66,l231,l302,l140,l58,l89,l271,l159,l103,l155,l96,l203,l194,l121,l98,l137,l94,l244,l32,l97,l15,l151,l276,l351,l81,l341,l80,l116,l86,l178,l95,l237,l27,l146,l84,l343,l300,l106,l312,l82,l224,l196,l44,l211,l173,l199,l342,l239,l216,l349,l153,l280,l265,l334,l299,l226,l261,l347,l172,l340,l135,l119,l149,l308,l242,l238,l56,l346,l307,l225,l305,l90,l142,l83,l144,l339,l92,l301,l256,l145,l93,l171,l350,l220,l167,l263,l174,l241,l243,l148,l150,l164,l283,l200,l262,l91,l53,l147,l158,l223,l337,l197,l104,l336,l222,l247,l309,l221,l348,l345,l298,l198,l30,l192,l138,l136,l115,l113,l50,l132,l130,l126,l141,l128,l131,l125,l112,l133,l127,l114]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP117+1 : TPTP v9.0.0. Released v2.4.0.
% 0.12/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n026.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Jul 21 08:48:49 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.19/0.34 % launching worker at depth: 1
% 0.19/0.34 % launching worker at depth: 7
% 0.19/0.34 % launching worker at depth: 2
% 0.19/0.34 % launching worker at depth: 6
% 0.19/0.34 % launching worker at depth: 4
% 0.19/0.34 % launching worker at depth: 3
% 0.19/0.34 % launching worker at depth: 5
% 0.19/0.34 % launching worker at depth: 8
% 0.19/0.34 % launching worker at depth: 9
% 0.19/0.38 % launching worker at depth: 10
% 2.14/0.63 % launching worker at depth: 11
% 2.52/0.70 % SZS status Theorem for theBenchmark
% 2.52/0.70 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------