%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP001+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 : n027.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:19 AM UTC 2025
% Result : Theorem 0.20s 0.46s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 1
% Syntax : Number of formulae : 273 ( 1 unt; 0 def)
% Number of atoms : 887 ( 0 equ)
% Maximal formula atoms : 56 ( 3 avg)
% Number of connectives : 1107 ( 493 ~; 504 |; 106 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 156 ( 116 sgn 0 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,plain,
( ( ? [U,V,W,X] :
( hollywood(U)
& city(U)
& event(V)
& street(W)
& way(W)
& lonely(W)
& chevy(X)
& car(X)
& white(X)
& dirty(X)
& old(X)
& barrel(V,X)
& down(V,W)
& in(V,U) )
=> ? [Y,Z,X1,X2] :
( hollywood(Y)
& city(Y)
& event(Z)
& chevy(X1)
& car(X1)
& white(X1)
& dirty(X1)
& old(X1)
& street(X2)
& way(X2)
& lonely(X2)
& barrel(Z,X1)
& down(Z,X2)
& in(Z,Y) ) )
& ( ? [X3,X4,X5,X6] :
( hollywood(X3)
& city(X3)
& event(X4)
& chevy(X5)
& car(X5)
& white(X5)
& dirty(X5)
& old(X5)
& street(X6)
& way(X6)
& lonely(X6)
& barrel(X4,X5)
& down(X4,X6)
& in(X4,X3) )
=> ? [X7,X8,X9,X10] :
( hollywood(X7)
& city(X7)
& event(X8)
& street(X9)
& way(X9)
& lonely(X9)
& chevy(X10)
& car(X10)
& white(X10)
& dirty(X10)
& old(X10)
& barrel(X8,X10)
& down(X8,X9)
& in(X8,X7) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(co1_negated,plain,
~ ( ( ? [U,V,W,X] :
( hollywood(U)
& city(U)
& event(V)
& street(W)
& way(W)
& lonely(W)
& chevy(X)
& car(X)
& white(X)
& dirty(X)
& old(X)
& barrel(V,X)
& down(V,W)
& in(V,U) )
=> ? [Y,Z,X1,X2] :
( hollywood(Y)
& city(Y)
& event(Z)
& chevy(X1)
& car(X1)
& white(X1)
& dirty(X1)
& old(X1)
& street(X2)
& way(X2)
& lonely(X2)
& barrel(Z,X1)
& down(Z,X2)
& in(Z,Y) ) )
& ( ? [X3,X4,X5,X6] :
( hollywood(X3)
& city(X3)
& event(X4)
& chevy(X5)
& car(X5)
& white(X5)
& dirty(X5)
& old(X5)
& street(X6)
& way(X6)
& lonely(X6)
& barrel(X4,X5)
& down(X4,X6)
& in(X4,X3) )
=> ? [X7,X8,X9,X10] :
( hollywood(X7)
& city(X7)
& event(X8)
& street(X9)
& way(X9)
& lonely(X9)
& chevy(X10)
& car(X10)
& white(X10)
& dirty(X10)
& old(X10)
& barrel(X8,X10)
& down(X8,X9)
& in(X8,X7) ) ) ),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(14,plain,
( ~ street(X0)
| ~ way(X0)
| ~ event(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ lonely(X0)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ barrel(X1,X3)
| ~ down(X1,X0)
| ~ in(X1,X2)
| sP0(X4,X5,X6,X7) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l0,plain,
( ~ street(sK3)
| ~ way(sK3)
| ~ event(sK2)
| ~ hollywood(sK1)
| ~ city(sK1)
| ~ lonely(sK3)
| ~ chevy(sK4)
| ~ car(sK4)
| ~ white(sK4)
| ~ dirty(sK4)
| ~ old(sK4)
| ~ barrel(sK2,sK4)
| ~ down(sK2,sK3)
| ~ in(sK2,sK1)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(1,plain,
( city(sK1)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l80,plain,
( city(sK1)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(2,plain,
( event(sK2)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l79,plain,
( event(sK2)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(3,plain,
( street(sK3)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1,plain,
( street(sK3)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(7,plain,
( car(sK4)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l77,plain,
( car(sK4)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(8,plain,
( white(sK4)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l90,plain,
( white(sK4)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(0,plain,
( hollywood(sK1)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l84,plain,
( hollywood(sK1)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(5,plain,
( lonely(sK3)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l78,plain,
( lonely(sK3)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(26,plain,
( chevy(sK7)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l76,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(15,plain,
( ~ street(X0)
| ~ way(X0)
| ~ event(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ lonely(X0)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ barrel(X1,X3)
| ~ down(X1,X0)
| ~ in(X1,X2)
| ~ sP0(X1,X2,X3,X0) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l93,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(28,plain,
( city(sK5)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l95,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(4,plain,
( way(sK3)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l2,plain,
( way(sK3)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(19,plain,
( lonely(sK8)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l94,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(9,plain,
( dirty(sK4)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l102,plain,
( dirty(sK4)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(27,plain,
( event(sK6)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l96,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(12,plain,
( down(sK2,sK3)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l92,plain,
( down(sK2,sK3)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(17,plain,
( down(sK6,sK8)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l110,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(13,plain,
( in(sK2,sK1)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l125,plain,
( in(sK2,sK1)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(20,plain,
( way(sK8)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l103,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(22,plain,
( old(sK7)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l97,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(29,plain,
( hollywood(sK5)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l174,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(24,plain,
( white(sK7)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l111,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l83,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l121,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l120,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l123,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l100,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l81,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l86,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(6,plain,
( chevy(sK4)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l89,plain,
( chevy(sK4)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(18,plain,
( barrel(sK6,sK7)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l259,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(11,plain,
( barrel(sK2,sK4)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l91,plain,
( barrel(sK2,sK4)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(25,plain,
( car(sK7)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l99,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(21,plain,
( street(sK8)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l88,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l260,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l261,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l106,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(23,plain,
( dirty(sK7)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l113,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l122,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(10,plain,
( old(sK4)
| sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l116,plain,
( old(sK4)
| sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l87,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l224,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l109,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l150,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l168,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l115,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l117,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(16,plain,
( in(sK6,sK5)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l175,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l159,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l256,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l273,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l266,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l262,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l161,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l169,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l181,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l285,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l142,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l166,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l107,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l178,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l278,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l133,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l156,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l276,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l177,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l288,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l105,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l263,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l279,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l286,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l200,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l104,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l195,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l135,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l127,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l277,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l272,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l280,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l227,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l192,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l197,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l270,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l191,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l82,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l264,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l149,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l222,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l132,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l271,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l228,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l114,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l254,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l198,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l296,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l221,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l294,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l136,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l134,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l292,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l165,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l251,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l201,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l190,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l196,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l268,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l202,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l155,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l250,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l225,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l282,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l85,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l126,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l242,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l229,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l226,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l137,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l303,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l244,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l144,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l101,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l301,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l304,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l236,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l253,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l129,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l243,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l291,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l231,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l235,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l281,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l275,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l146,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l128,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l241,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l267,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l274,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l297,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l193,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l252,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l258,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l310,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l138,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l139,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l189,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l112,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l307,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l245,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l293,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l283,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l118,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l300,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l16,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l234,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l141,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l152,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l171,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l232,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l162,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l147,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l204,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l298,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l207,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l151,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l308,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l249,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l238,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l140,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l248,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l311,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l158,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l233,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l223,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l179,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l247,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l265,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l148,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l306,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l124,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l203,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l185,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l255,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l289,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l205,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l176,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l257,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l269,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l182,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l180,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l157,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l240,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l98,plain,
( ~ street(sK8)
| ~ way(sK8)
| ~ event(sK6)
| ~ hollywood(sK5)
| ~ city(sK5)
| ~ lonely(sK8)
| ~ chevy(sK7)
| ~ car(sK7)
| ~ white(sK7)
| ~ dirty(sK7)
| ~ old(sK7)
| ~ barrel(sK6,sK7)
| ~ down(sK6,sK8)
| ~ in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l305,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l167,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l194,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l154,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l163,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l143,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l290,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l206,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l246,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l199,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l145,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l170,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l211,plain,
( car(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l173,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l239,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l210,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l302,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l209,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l299,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l153,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l216,plain,
( event(sK6)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l214,plain,
( barrel(sK6,sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l160,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l183,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l212,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l187,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l184,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l217,plain,
( dirty(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l219,plain,
( old(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l230,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l295,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l172,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l237,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l220,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l287,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l284,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l312,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l309,plain,
( hollywood(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l164,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l218,plain,
( city(sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l130,plain,
( street(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l215,plain,
( lonely(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l186,plain,
( down(sK6,sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l313,plain,
( white(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l208,plain,
( chevy(sK7)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l213,plain,
( way(sK8)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l119,plain,
( in(sK6,sK5)
| ~ sP0(sK6,sK5,sK7,sK8) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l80,l79,l1,l77,l90,l84,l78,l76,l93,l95,l2,l94,l102,l96,l92,l110,l125,l103,l97,l174,l111,l83,l121,l120,l123,l100,l81,l86,l89,l259,l91,l99,l88,l260,l261,l106,l113,l122,l116,l87,l224,l109,l150,l168,l115,l117,l175,l159,l256,l273,l266,l262,l161,l169,l181,l285,l142,l166,l107,l178,l278,l133,l156,l276,l177,l288,l105,l263,l279,l286,l200,l104,l195,l135,l127,l277,l272,l280,l227,l192,l197,l270,l191,l82,l264,l149,l222,l132,l271,l228,l114,l254,l198,l296,l221,l294,l136,l134,l292,l165,l251,l201,l190,l196,l268,l202,l155,l250,l225,l282,l85,l126,l242,l229,l226,l137,l303,l244,l8,l144,l101,l301,l304,l236,l253,l129,l243,l291,l231,l235,l281,l275,l146,l128,l241,l267,l274,l297,l193,l252,l258,l310,l138,l139,l189,l112,l307,l245,l293,l283,l118,l300,l16,l234,l141,l152,l171,l232,l162,l147,l204,l298,l207,l151,l308,l249,l238,l140,l248,l311,l158,l233,l223,l179,l247,l265,l148,l306,l124,l203,l185,l255,l289,l205,l176,l257,l269,l182,l180,l157,l240,l98,l305,l167,l194,l154,l163,l143,l290,l206,l246,l199,l145,l170,l211,l173,l239,l210,l302,l209,l299,l153,l216,l214,l160,l183,l212,l187,l184,l217,l219,l230,l295,l172,l237,l220,l287,l284,l312,l309,l164,l218,l130,l215,l186,l313,l208,l213,l119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NLP001+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.13/0.33 % Computer : n027.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 07:49:19 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 8
% 0.13/0.34 % launching worker at depth: 9
% 0.20/0.38 % launching worker at depth: 10
% 0.20/0.46 % SZS status Theorem for theBenchmark
% 0.20/0.46 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------