%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP122+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:39 AM UTC 2025
% Result : Theorem 2.36s 0.63s
% Output : CNFRefutation 2.36s
% 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 : 27 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-5 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 225 ( 175 sgn 0 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,plain,
~ ~ ( ( ? [U] :
( actual_world(U)
& ? [V,W,X,Y] :
( of(U,V,W)
& city(U,W)
& hollywood_placename(U,V)
& placename(U,V)
& chevy(U,W)
& white(U,W)
& dirty(U,W)
& old(U,W)
& street(U,X)
& lonely(U,X)
& event(U,Y)
& agent(U,Y,W)
& present(U,Y)
& barrel(U,Y)
& down(U,Y,X)
& in(U,Y,W) ) )
=> ? [Z] :
( actual_world(Z)
& ? [X1,X2,X3,X4] :
( street(Z,X1)
& lonely(Z,X1)
& of(Z,X2,X3)
& city(Z,X3)
& hollywood_placename(Z,X2)
& placename(Z,X2)
& chevy(Z,X3)
& white(Z,X3)
& dirty(Z,X3)
& old(Z,X3)
& event(Z,X4)
& agent(Z,X4,X3)
& present(Z,X4)
& barrel(Z,X4)
& down(Z,X4,X1)
& in(Z,X4,X3) ) ) )
& ( ? [Z] :
( actual_world(Z)
& ? [X1,X2,X3,X4] :
( street(Z,X1)
& lonely(Z,X1)
& of(Z,X2,X3)
& city(Z,X3)
& hollywood_placename(Z,X2)
& placename(Z,X2)
& chevy(Z,X3)
& white(Z,X3)
& dirty(Z,X3)
& old(Z,X3)
& event(Z,X4)
& agent(Z,X4,X3)
& present(Z,X4)
& barrel(Z,X4)
& down(Z,X4,X1)
& in(Z,X4,X3) ) )
=> ? [U] :
( actual_world(U)
& ? [V,W,X,Y] :
( of(U,V,W)
& city(U,W)
& hollywood_placename(U,V)
& placename(U,V)
& chevy(U,W)
& white(U,W)
& dirty(U,W)
& old(U,W)
& street(U,X)
& lonely(U,X)
& event(U,Y)
& agent(U,Y,W)
& present(U,Y)
& barrel(U,Y)
& down(U,Y,X)
& in(U,Y,W) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(co1_negated,plain,
~ ~ ~ ( ( ? [U] :
( actual_world(U)
& ? [V,W,X,Y] :
( of(U,V,W)
& city(U,W)
& hollywood_placename(U,V)
& placename(U,V)
& chevy(U,W)
& white(U,W)
& dirty(U,W)
& old(U,W)
& street(U,X)
& lonely(U,X)
& event(U,Y)
& agent(U,Y,W)
& present(U,Y)
& barrel(U,Y)
& down(U,Y,X)
& in(U,Y,W) ) )
=> ? [Z] :
( actual_world(Z)
& ? [X1,X2,X3,X4] :
( street(Z,X1)
& lonely(Z,X1)
& of(Z,X2,X3)
& city(Z,X3)
& hollywood_placename(Z,X2)
& placename(Z,X2)
& chevy(Z,X3)
& white(Z,X3)
& dirty(Z,X3)
& old(Z,X3)
& event(Z,X4)
& agent(Z,X4,X3)
& present(Z,X4)
& barrel(Z,X4)
& down(Z,X4,X1)
& in(Z,X4,X3) ) ) )
& ( ? [Z] :
( actual_world(Z)
& ? [X1,X2,X3,X4] :
( street(Z,X1)
& lonely(Z,X1)
& of(Z,X2,X3)
& city(Z,X3)
& hollywood_placename(Z,X2)
& placename(Z,X2)
& chevy(Z,X3)
& white(Z,X3)
& dirty(Z,X3)
& old(Z,X3)
& event(Z,X4)
& agent(Z,X4,X3)
& present(Z,X4)
& barrel(Z,X4)
& down(Z,X4,X1)
& in(Z,X4,X3) ) )
=> ? [U] :
( actual_world(U)
& ? [V,W,X,Y] :
( of(U,V,W)
& city(U,W)
& hollywood_placename(U,V)
& placename(U,V)
& chevy(U,W)
& white(U,W)
& dirty(U,W)
& old(U,W)
& street(U,X)
& lonely(U,X)
& event(U,Y)
& agent(U,Y,W)
& present(U,Y)
& barrel(U,Y)
& down(U,Y,X)
& in(U,Y,W) ) ) ) ),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(17,plain,
( ~ street(X0,X1)
| ~ city(X0,X2)
| ~ lonely(X0,X1)
| ~ event(X0,X3)
| ~ agent(X0,X3,X2)
| ~ actual_world(X0)
| ~ of(X0,X4,X2)
| ~ hollywood_placename(X0,X4)
| ~ placename(X0,X4)
| ~ chevy(X0,X2)
| ~ white(X0,X2)
| ~ dirty(X0,X2)
| ~ old(X0,X2)
| ~ present(X0,X3)
| ~ barrel(X0,X3)
| ~ down(X0,X3,X1)
| ~ in(X0,X3,X2)
| sP0(X5,X6,X7,X8,X9) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l0,plain,
( ~ street(sK1,sK4)
| ~ city(sK1,sK3)
| ~ lonely(sK1,sK4)
| ~ event(sK1,sK5)
| ~ agent(sK1,sK5,sK3)
| ~ actual_world(sK1)
| ~ of(sK1,sK2,sK3)
| ~ hollywood_placename(sK1,sK2)
| ~ placename(sK1,sK2)
| ~ chevy(sK1,sK3)
| ~ white(sK1,sK3)
| ~ dirty(sK1,sK3)
| ~ old(sK1,sK3)
| ~ present(sK1,sK5)
| ~ barrel(sK1,sK5)
| ~ down(sK1,sK5,sK4)
| ~ in(sK1,sK5,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(5,plain,
( chevy(sK1,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l110,plain,
( chevy(sK1,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(12,plain,
( agent(sK1,sK5,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l93,plain,
( agent(sK1,sK5,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(1,plain,
( of(sK1,sK2,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l99,plain,
( of(sK1,sK2,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(4,plain,
( placename(sK1,sK2)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l94,plain,
( placename(sK1,sK2)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(11,plain,
( event(sK1,sK5)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l103,plain,
( event(sK1,sK5)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(14,plain,
( barrel(sK1,sK5)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l126,plain,
( barrel(sK1,sK5)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(7,plain,
( dirty(sK1,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l125,plain,
( dirty(sK1,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(18,plain,
( ~ street(X0,X1)
| ~ city(X0,X2)
| ~ lonely(X0,X1)
| ~ event(X0,X3)
| ~ agent(X0,X3,X2)
| ~ actual_world(X0)
| ~ of(X0,X4,X2)
| ~ hollywood_placename(X0,X4)
| ~ placename(X0,X4)
| ~ chevy(X0,X2)
| ~ white(X0,X2)
| ~ dirty(X0,X2)
| ~ old(X0,X2)
| ~ present(X0,X3)
| ~ barrel(X0,X3)
| ~ down(X0,X3,X1)
| ~ in(X0,X3,X2)
| ~ sP0(X0,X2,X4,X3,X1) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l163,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(6,plain,
( white(sK1,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l109,plain,
( white(sK1,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(34,plain,
( street(sK6,sK7)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l165,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(26,plain,
( dirty(sK6,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l106,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(16,plain,
( in(sK1,sK5,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l107,plain,
( in(sK1,sK5,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(35,plain,
( actual_world(sK6)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l340,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(20,plain,
( down(sK6,sK10,sK7)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l322,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(21,plain,
( barrel(sK6,sK10)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l318,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l96,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(31,plain,
( city(sK6,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l180,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(27,plain,
( white(sK6,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l320,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(24,plain,
( event(sK6,sK10)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l186,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l115,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(19,plain,
( in(sK6,sK10,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l388,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l187,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(2,plain,
( city(sK1,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l2,plain,
( city(sK1,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(32,plain,
( of(sK6,sK8,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l191,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(8,plain,
( old(sK1,sK3)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l92,plain,
( old(sK1,sK3)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(25,plain,
( old(sK6,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l371,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(22,plain,
( present(sK6,sK10)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l338,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(3,plain,
( hollywood_placename(sK1,sK2)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l97,plain,
( hollywood_placename(sK1,sK2)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l406,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l407,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l317,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l333,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l427,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l416,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(33,plain,
( lonely(sK6,sK7)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l392,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(0,plain,
( actual_world(sK1)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l101,plain,
( actual_world(sK1)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l428,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(30,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l372,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l319,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l411,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l181,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l113,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l410,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l418,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l429,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l336,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(28,plain,
( chevy(sK6,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l391,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(23,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l419,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l138,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l430,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l412,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(9,plain,
( street(sK1,sK4)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1,plain,
( street(sK1,sK4)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l123,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l394,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l276,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(29,plain,
( placename(sK6,sK8)
| ~ sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l341,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(15,plain,
( down(sK1,sK5,sK4)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l102,plain,
( down(sK1,sK5,sK4)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l434,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l127,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l402,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l275,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l280,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l384,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l169,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l335,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l414,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l130,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l257,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l248,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l272,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l269,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l278,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l383,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l304,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l132,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l282,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l128,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l260,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l270,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l408,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l279,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l403,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l417,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l370,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l274,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(13,plain,
( present(sK1,sK5)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l114,plain,
( present(sK1,sK5)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l334,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l124,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l437,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l393,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l310,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l405,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l409,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l436,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l431,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l413,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l404,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l432,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l254,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l255,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l258,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l356,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l111,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l277,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l350,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l349,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l442,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l355,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l390,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l337,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l385,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l339,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l347,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l189,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l352,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l348,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l351,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l433,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l439,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l118,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l308,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l143,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l223,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l173,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l345,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l171,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l95,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l344,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(10,plain,
( lonely(sK1,sK4)
| sP0(X0,X1,X2,X3,X4) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l105,plain,
( lonely(sK1,sK4)
| sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l415,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l353,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l141,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l150,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l158,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l197,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l139,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l129,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l157,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l200,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l152,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l435,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l264,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l122,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l156,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l147,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l153,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l210,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l441,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l151,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l217,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l440,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l307,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l155,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l120,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l361,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l368,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l369,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l273,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l121,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l160,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l159,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l228,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l229,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l364,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l221,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l112,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l142,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l306,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l168,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l378,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l240,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l363,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l246,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l140,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l226,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l148,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l381,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l227,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l367,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l154,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l185,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l343,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l261,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l438,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l119,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l358,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l213,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l135,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l362,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l443,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l131,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l346,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l450,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l222,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l117,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l454,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l455,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l374,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l456,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l449,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l426,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l215,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l377,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l424,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l373,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l457,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l247,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l382,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l446,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l452,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l365,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l359,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l209,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l161,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l458,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l219,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l386,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l375,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l212,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l216,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l379,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l244,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l444,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l225,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l460,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l389,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l366,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l459,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l104,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l445,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l192,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l162,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l220,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l172,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l376,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l425,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l234,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l195,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l183,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l380,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l196,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l184,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l177,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l108,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l243,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l451,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l236,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l188,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l231,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l271,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l149,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l241,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l360,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l422,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l116,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l133,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l214,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l190,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l263,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l251,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l201,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l232,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l420,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l194,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l136,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l203,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l170,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l175,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l202,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l395,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l176,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l259,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l423,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l134,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l204,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l399,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l166,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l38,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l174,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l208,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l224,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l239,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l281,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l245,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l401,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l342,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l357,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l400,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l179,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l205,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l267,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l354,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l398,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l233,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l265,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l182,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l237,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l252,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l249,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l230,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l206,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l238,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l268,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l396,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l211,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l218,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l266,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l447,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l193,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l250,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l256,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l448,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l387,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l453,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l262,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l397,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l283,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l242,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l98,plain,
( ~ street(sK6,sK7)
| ~ city(sK6,sK9)
| ~ lonely(sK6,sK7)
| ~ event(sK6,sK10)
| ~ agent(sK6,sK10,sK9)
| ~ actual_world(sK6)
| ~ of(sK6,sK8,sK9)
| ~ hollywood_placename(sK6,sK8)
| ~ placename(sK6,sK8)
| ~ chevy(sK6,sK9)
| ~ white(sK6,sK9)
| ~ dirty(sK6,sK9)
| ~ old(sK6,sK9)
| ~ present(sK6,sK10)
| ~ barrel(sK6,sK10)
| ~ down(sK6,sK10,sK7)
| ~ in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l137,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l145,plain,
( event(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l330,plain,
( down(sK6,sK10,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l144,plain,
( chevy(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l332,plain,
( old(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l324,plain,
( lonely(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l198,plain,
( of(sK6,sK8,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l328,plain,
( actual_world(sK6)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l289,plain,
( dirty(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l100,plain,
( street(sK6,sK7)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l178,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l207,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l321,plain,
( agent(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l253,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l326,plain,
( present(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l329,plain,
( white(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l331,plain,
( barrel(sK6,sK10)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l323,plain,
( placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l325,plain,
( city(sK6,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l146,plain,
( hollywood_placename(sK6,sK8)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l327,plain,
( in(sK6,sK10,sK9)
| ~ sP0(sK6,sK9,sK8,sK10,sK7) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l110,l93,l99,l94,l103,l126,l125,l163,l109,l165,l106,l107,l340,l322,l318,l96,l180,l320,l186,l115,l388,l187,l2,l191,l92,l371,l338,l97,l406,l407,l317,l333,l427,l416,l392,l101,l428,l372,l319,l411,l181,l113,l410,l418,l429,l336,l391,l419,l138,l430,l412,l1,l123,l394,l276,l341,l102,l434,l127,l402,l275,l280,l384,l169,l335,l414,l130,l257,l248,l272,l269,l278,l383,l304,l132,l282,l128,l260,l270,l408,l279,l403,l417,l370,l274,l114,l334,l124,l437,l393,l310,l405,l409,l436,l431,l413,l404,l432,l254,l255,l258,l356,l111,l277,l350,l349,l442,l355,l390,l337,l385,l339,l347,l189,l352,l348,l351,l433,l439,l118,l308,l143,l223,l173,l345,l171,l95,l344,l105,l415,l353,l141,l150,l158,l197,l139,l129,l157,l200,l152,l435,l264,l122,l156,l147,l153,l210,l441,l151,l217,l440,l307,l155,l120,l8,l361,l368,l369,l273,l121,l160,l159,l228,l229,l364,l221,l112,l142,l306,l168,l378,l240,l363,l246,l140,l226,l148,l381,l227,l367,l154,l185,l343,l261,l438,l119,l358,l213,l135,l362,l443,l131,l346,l450,l222,l117,l454,l455,l374,l456,l449,l426,l215,l377,l424,l373,l457,l247,l382,l446,l452,l365,l359,l209,l161,l458,l219,l386,l375,l212,l216,l379,l244,l444,l225,l460,l389,l366,l459,l104,l445,l192,l162,l220,l172,l376,l425,l234,l195,l183,l380,l196,l184,l177,l108,l243,l451,l236,l188,l231,l271,l149,l241,l360,l422,l116,l133,l214,l190,l263,l251,l201,l232,l420,l194,l136,l203,l170,l175,l202,l395,l176,l259,l423,l134,l204,l399,l166,l38,l174,l208,l224,l239,l281,l245,l401,l342,l357,l400,l179,l205,l267,l354,l398,l233,l265,l182,l237,l252,l249,l230,l206,l238,l268,l396,l211,l218,l266,l447,l193,l250,l256,l448,l387,l453,l262,l397,l283,l242,l98,l137,l145,l330,l144,l332,l324,l198,l328,l289,l100,l178,l207,l321,l253,l326,l329,l331,l323,l325,l146,l327]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NLP122+1 : TPTP v9.0.0. Released v2.4.0.
% 0.04/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 21 08:50:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.18/0.38 % launching worker at depth: 10
% 2.36/0.63 % SZS status Theorem for theBenchmark
% 2.36/0.63 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------