%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NLP001+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:07:11 AM UTC 2026
% Result : Theorem 0.54s 0.48s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 143
% Number of leaves : 1
% Syntax : Number of formulae : 706 ( 25 unt; 0 def)
% Number of atoms : 5299 ( 0 equ)
% Maximal formula atoms : 840 ( 7 avg)
% Number of connectives : 8257 (3664 ~;4203 |; 386 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 261 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 378 ( 0 sgn 136 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
( ( ? [X3,X4,X5,X6] :
( in(X4,X3)
& down(X4,X6)
& barrel(X4,X5)
& lonely(X6)
& way(X6)
& street(X6)
& old(X5)
& dirty(X5)
& white(X5)
& car(X5)
& chevy(X5)
& event(X4)
& city(X3)
& hollywood(X3) )
=> ? [X7,X8,X9,X10] :
( in(X8,X7)
& down(X8,X9)
& barrel(X8,X10)
& old(X10)
& dirty(X10)
& white(X10)
& car(X10)
& chevy(X10)
& lonely(X9)
& way(X9)
& street(X9)
& event(X8)
& city(X7)
& hollywood(X7) ) )
& ( ? [U,V,W,X] :
( in(V,U)
& down(V,W)
& barrel(V,X)
& old(X)
& dirty(X)
& white(X)
& car(X)
& chevy(X)
& lonely(W)
& way(W)
& street(W)
& event(V)
& city(U)
& hollywood(U) )
=> ? [Y,Z,X1,X2] :
( in(Z,Y)
& down(Z,X2)
& barrel(Z,X1)
& lonely(X2)
& way(X2)
& street(X2)
& old(X1)
& dirty(X1)
& white(X1)
& car(X1)
& chevy(X1)
& event(Z)
& city(Y)
& hollywood(Y) ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ? [X3,X4,X5,X6] :
( in(X4,X3)
& down(X4,X6)
& barrel(X4,X5)
& lonely(X6)
& way(X6)
& street(X6)
& old(X5)
& dirty(X5)
& white(X5)
& car(X5)
& chevy(X5)
& event(X4)
& city(X3)
& hollywood(X3) )
=> ? [X7,X8,X9,X10] :
( in(X8,X7)
& down(X8,X9)
& barrel(X8,X10)
& old(X10)
& dirty(X10)
& white(X10)
& car(X10)
& chevy(X10)
& lonely(X9)
& way(X9)
& street(X9)
& event(X8)
& city(X7)
& hollywood(X7) ) )
& ( ? [U,V,W,X] :
( in(V,U)
& down(V,W)
& barrel(V,X)
& old(X)
& dirty(X)
& white(X)
& car(X)
& chevy(X)
& lonely(W)
& way(W)
& street(W)
& event(V)
& city(U)
& hollywood(U) )
=> ? [Y,Z,X1,X2] :
( in(Z,Y)
& down(Z,X2)
& barrel(Z,X1)
& lonely(X2)
& way(X2)
& street(X2)
& old(X1)
& dirty(X1)
& white(X1)
& car(X1)
& chevy(X1)
& event(Z)
& city(Y)
& hollywood(Y) ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
fof(nnf_1,plain,
( ( ! [X7,X8,X9,X10] :
( ~ in(X8,X7)
| ~ down(X8,X9)
| ~ barrel(X8,X10)
| ~ old(X10)
| ~ dirty(X10)
| ~ white(X10)
| ~ car(X10)
| ~ chevy(X10)
| ~ lonely(X9)
| ~ way(X9)
| ~ street(X9)
| ~ event(X8)
| ~ city(X7)
| ~ hollywood(X7) )
& ? [X3,X4,X5,X6] :
( in(X4,X3)
& down(X4,X6)
& barrel(X4,X5)
& lonely(X6)
& way(X6)
& street(X6)
& old(X5)
& dirty(X5)
& white(X5)
& car(X5)
& chevy(X5)
& event(X4)
& city(X3)
& hollywood(X3) ) )
| ( ! [Y,Z,X1,X2] :
( ~ in(Z,Y)
| ~ down(Z,X2)
| ~ barrel(Z,X1)
| ~ lonely(X2)
| ~ way(X2)
| ~ street(X2)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ event(Z)
| ~ city(Y)
| ~ hollywood(Y) )
& ? [U,V,W,X] :
( in(V,U)
& down(V,W)
& barrel(V,X)
& old(X)
& dirty(X)
& white(X)
& car(X)
& chevy(X)
& lonely(W)
& way(W)
& street(W)
& event(V)
& city(U)
& hollywood(U) ) ) ),
inference(fof_nnf,[status(thm)],[co1_neg]) ).
fof(sk_co1_neg_sk,plain,
( ( ! [X7,X8,X9,X10] :
( ~ in(X8,X7)
| ~ down(X8,X9)
| ~ barrel(X8,X10)
| ~ old(X10)
| ~ dirty(X10)
| ~ white(X10)
| ~ car(X10)
| ~ chevy(X10)
| ~ lonely(X9)
| ~ way(X9)
| ~ street(X9)
| ~ event(X8)
| ~ city(X7)
| ~ hollywood(X7) )
& in(sK2,sK1)
& down(sK2,sK4)
& barrel(sK2,sK3)
& lonely(sK4)
& way(sK4)
& street(sK4)
& old(sK3)
& dirty(sK3)
& white(sK3)
& car(sK3)
& chevy(sK3)
& event(sK2)
& city(sK1)
& hollywood(sK1) )
| ( ! [Y,Z,X1,X2] :
( ~ in(Z,Y)
| ~ down(Z,X2)
| ~ barrel(Z,X1)
| ~ lonely(X2)
| ~ way(X2)
| ~ street(X2)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ event(Z)
| ~ city(Y)
| ~ hollywood(Y) )
& in(sK5,sK0)
& down(sK5,sK6)
& barrel(sK5,sK7)
& old(sK7)
& dirty(sK7)
& white(sK7)
& car(sK7)
& chevy(sK7)
& lonely(sK6)
& way(sK6)
& street(sK6)
& event(sK5)
& city(sK0)
& hollywood(sK0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK5,sK6,sK7,sK1,sK2,sK3,sK4]),skolemize(U,sK0),skolemize(V,sK5),skolemize(W,sK6),skolemize(X,sK7),skolemize(X3,sK1),skolemize(X4,sK2),skolemize(X5,sK3),skolemize(X6,sK4)],[nnf_1]) ).
fof(sk_co1_neg,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( ~ in(VAR_5,VAR_4)
| ~ down(VAR_5,VAR_6)
| ~ barrel(VAR_5,VAR_7)
| ~ old(VAR_7)
| ~ dirty(VAR_7)
| ~ white(VAR_7)
| ~ car(VAR_7)
| ~ chevy(VAR_7)
| ~ lonely(VAR_6)
| ~ way(VAR_6)
| ~ street(VAR_6)
| ~ event(VAR_5)
| ~ city(VAR_4)
| ~ hollywood(VAR_4)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( in(sK2,sK1)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( down(sK2,sK4)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( barrel(sK2,sK3)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( lonely(sK4)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( way(sK4)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( street(sK4)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( old(sK3)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( dirty(sK3)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( white(sK3)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( car(sK3)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( chevy(sK3)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( event(sK2)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( city(sK1)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( hollywood(sK1)
| ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_3)
| ~ barrel(VAR_1,VAR_2)
| ~ lonely(VAR_3)
| ~ way(VAR_3)
| ~ street(VAR_3)
| ~ old(VAR_2)
| ~ dirty(VAR_2)
| ~ white(VAR_2)
| ~ car(VAR_2)
| ~ chevy(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| in(sK5,sK0) )
& ( in(sK2,sK1)
| in(sK5,sK0) )
& ( down(sK2,sK4)
| in(sK5,sK0) )
& ( barrel(sK2,sK3)
| in(sK5,sK0) )
& ( lonely(sK4)
| in(sK5,sK0) )
& ( way(sK4)
| in(sK5,sK0) )
& ( street(sK4)
| in(sK5,sK0) )
& ( old(sK3)
| in(sK5,sK0) )
& ( dirty(sK3)
| in(sK5,sK0) )
& ( white(sK3)
| in(sK5,sK0) )
& ( car(sK3)
| in(sK5,sK0) )
& ( chevy(sK3)
| in(sK5,sK0) )
& ( event(sK2)
| in(sK5,sK0) )
& ( city(sK1)
| in(sK5,sK0) )
& ( hollywood(sK1)
| in(sK5,sK0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| down(sK5,sK6) )
& ( in(sK2,sK1)
| down(sK5,sK6) )
& ( down(sK2,sK4)
| down(sK5,sK6) )
& ( barrel(sK2,sK3)
| down(sK5,sK6) )
& ( lonely(sK4)
| down(sK5,sK6) )
& ( way(sK4)
| down(sK5,sK6) )
& ( street(sK4)
| down(sK5,sK6) )
& ( old(sK3)
| down(sK5,sK6) )
& ( dirty(sK3)
| down(sK5,sK6) )
& ( white(sK3)
| down(sK5,sK6) )
& ( car(sK3)
| down(sK5,sK6) )
& ( chevy(sK3)
| down(sK5,sK6) )
& ( event(sK2)
| down(sK5,sK6) )
& ( city(sK1)
| down(sK5,sK6) )
& ( hollywood(sK1)
| down(sK5,sK6) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| barrel(sK5,sK7) )
& ( in(sK2,sK1)
| barrel(sK5,sK7) )
& ( down(sK2,sK4)
| barrel(sK5,sK7) )
& ( barrel(sK2,sK3)
| barrel(sK5,sK7) )
& ( lonely(sK4)
| barrel(sK5,sK7) )
& ( way(sK4)
| barrel(sK5,sK7) )
& ( street(sK4)
| barrel(sK5,sK7) )
& ( old(sK3)
| barrel(sK5,sK7) )
& ( dirty(sK3)
| barrel(sK5,sK7) )
& ( white(sK3)
| barrel(sK5,sK7) )
& ( car(sK3)
| barrel(sK5,sK7) )
& ( chevy(sK3)
| barrel(sK5,sK7) )
& ( event(sK2)
| barrel(sK5,sK7) )
& ( city(sK1)
| barrel(sK5,sK7) )
& ( hollywood(sK1)
| barrel(sK5,sK7) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| old(sK7) )
& ( in(sK2,sK1)
| old(sK7) )
& ( down(sK2,sK4)
| old(sK7) )
& ( barrel(sK2,sK3)
| old(sK7) )
& ( lonely(sK4)
| old(sK7) )
& ( way(sK4)
| old(sK7) )
& ( street(sK4)
| old(sK7) )
& ( old(sK3)
| old(sK7) )
& ( dirty(sK3)
| old(sK7) )
& ( white(sK3)
| old(sK7) )
& ( car(sK3)
| old(sK7) )
& ( chevy(sK3)
| old(sK7) )
& ( event(sK2)
| old(sK7) )
& ( city(sK1)
| old(sK7) )
& ( hollywood(sK1)
| old(sK7) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| dirty(sK7) )
& ( in(sK2,sK1)
| dirty(sK7) )
& ( down(sK2,sK4)
| dirty(sK7) )
& ( barrel(sK2,sK3)
| dirty(sK7) )
& ( lonely(sK4)
| dirty(sK7) )
& ( way(sK4)
| dirty(sK7) )
& ( street(sK4)
| dirty(sK7) )
& ( old(sK3)
| dirty(sK7) )
& ( dirty(sK3)
| dirty(sK7) )
& ( white(sK3)
| dirty(sK7) )
& ( car(sK3)
| dirty(sK7) )
& ( chevy(sK3)
| dirty(sK7) )
& ( event(sK2)
| dirty(sK7) )
& ( city(sK1)
| dirty(sK7) )
& ( hollywood(sK1)
| dirty(sK7) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| white(sK7) )
& ( in(sK2,sK1)
| white(sK7) )
& ( down(sK2,sK4)
| white(sK7) )
& ( barrel(sK2,sK3)
| white(sK7) )
& ( lonely(sK4)
| white(sK7) )
& ( way(sK4)
| white(sK7) )
& ( street(sK4)
| white(sK7) )
& ( old(sK3)
| white(sK7) )
& ( dirty(sK3)
| white(sK7) )
& ( white(sK3)
| white(sK7) )
& ( car(sK3)
| white(sK7) )
& ( chevy(sK3)
| white(sK7) )
& ( event(sK2)
| white(sK7) )
& ( city(sK1)
| white(sK7) )
& ( hollywood(sK1)
| white(sK7) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| car(sK7) )
& ( in(sK2,sK1)
| car(sK7) )
& ( down(sK2,sK4)
| car(sK7) )
& ( barrel(sK2,sK3)
| car(sK7) )
& ( lonely(sK4)
| car(sK7) )
& ( way(sK4)
| car(sK7) )
& ( street(sK4)
| car(sK7) )
& ( old(sK3)
| car(sK7) )
& ( dirty(sK3)
| car(sK7) )
& ( white(sK3)
| car(sK7) )
& ( car(sK3)
| car(sK7) )
& ( chevy(sK3)
| car(sK7) )
& ( event(sK2)
| car(sK7) )
& ( city(sK1)
| car(sK7) )
& ( hollywood(sK1)
| car(sK7) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| chevy(sK7) )
& ( in(sK2,sK1)
| chevy(sK7) )
& ( down(sK2,sK4)
| chevy(sK7) )
& ( barrel(sK2,sK3)
| chevy(sK7) )
& ( lonely(sK4)
| chevy(sK7) )
& ( way(sK4)
| chevy(sK7) )
& ( street(sK4)
| chevy(sK7) )
& ( old(sK3)
| chevy(sK7) )
& ( dirty(sK3)
| chevy(sK7) )
& ( white(sK3)
| chevy(sK7) )
& ( car(sK3)
| chevy(sK7) )
& ( chevy(sK3)
| chevy(sK7) )
& ( event(sK2)
| chevy(sK7) )
& ( city(sK1)
| chevy(sK7) )
& ( hollywood(sK1)
| chevy(sK7) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| lonely(sK6) )
& ( in(sK2,sK1)
| lonely(sK6) )
& ( down(sK2,sK4)
| lonely(sK6) )
& ( barrel(sK2,sK3)
| lonely(sK6) )
& ( lonely(sK4)
| lonely(sK6) )
& ( way(sK4)
| lonely(sK6) )
& ( street(sK4)
| lonely(sK6) )
& ( old(sK3)
| lonely(sK6) )
& ( dirty(sK3)
| lonely(sK6) )
& ( white(sK3)
| lonely(sK6) )
& ( car(sK3)
| lonely(sK6) )
& ( chevy(sK3)
| lonely(sK6) )
& ( event(sK2)
| lonely(sK6) )
& ( city(sK1)
| lonely(sK6) )
& ( hollywood(sK1)
| lonely(sK6) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| way(sK6) )
& ( in(sK2,sK1)
| way(sK6) )
& ( down(sK2,sK4)
| way(sK6) )
& ( barrel(sK2,sK3)
| way(sK6) )
& ( lonely(sK4)
| way(sK6) )
& ( way(sK4)
| way(sK6) )
& ( street(sK4)
| way(sK6) )
& ( old(sK3)
| way(sK6) )
& ( dirty(sK3)
| way(sK6) )
& ( white(sK3)
| way(sK6) )
& ( car(sK3)
| way(sK6) )
& ( chevy(sK3)
| way(sK6) )
& ( event(sK2)
| way(sK6) )
& ( city(sK1)
| way(sK6) )
& ( hollywood(sK1)
| way(sK6) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| street(sK6) )
& ( in(sK2,sK1)
| street(sK6) )
& ( down(sK2,sK4)
| street(sK6) )
& ( barrel(sK2,sK3)
| street(sK6) )
& ( lonely(sK4)
| street(sK6) )
& ( way(sK4)
| street(sK6) )
& ( street(sK4)
| street(sK6) )
& ( old(sK3)
| street(sK6) )
& ( dirty(sK3)
| street(sK6) )
& ( white(sK3)
| street(sK6) )
& ( car(sK3)
| street(sK6) )
& ( chevy(sK3)
| street(sK6) )
& ( event(sK2)
| street(sK6) )
& ( city(sK1)
| street(sK6) )
& ( hollywood(sK1)
| street(sK6) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| event(sK5) )
& ( in(sK2,sK1)
| event(sK5) )
& ( down(sK2,sK4)
| event(sK5) )
& ( barrel(sK2,sK3)
| event(sK5) )
& ( lonely(sK4)
| event(sK5) )
& ( way(sK4)
| event(sK5) )
& ( street(sK4)
| event(sK5) )
& ( old(sK3)
| event(sK5) )
& ( dirty(sK3)
| event(sK5) )
& ( white(sK3)
| event(sK5) )
& ( car(sK3)
| event(sK5) )
& ( chevy(sK3)
| event(sK5) )
& ( event(sK2)
| event(sK5) )
& ( city(sK1)
| event(sK5) )
& ( hollywood(sK1)
| event(sK5) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| city(sK0) )
& ( in(sK2,sK1)
| city(sK0) )
& ( down(sK2,sK4)
| city(sK0) )
& ( barrel(sK2,sK3)
| city(sK0) )
& ( lonely(sK4)
| city(sK0) )
& ( way(sK4)
| city(sK0) )
& ( street(sK4)
| city(sK0) )
& ( old(sK3)
| city(sK0) )
& ( dirty(sK3)
| city(sK0) )
& ( white(sK3)
| city(sK0) )
& ( car(sK3)
| city(sK0) )
& ( chevy(sK3)
| city(sK0) )
& ( event(sK2)
| city(sK0) )
& ( city(sK1)
| city(sK0) )
& ( hollywood(sK1)
| city(sK0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(VAR_1,VAR_0)
| ~ down(VAR_1,VAR_2)
| ~ barrel(VAR_1,VAR_3)
| ~ old(VAR_3)
| ~ dirty(VAR_3)
| ~ white(VAR_3)
| ~ car(VAR_3)
| ~ chevy(VAR_3)
| ~ lonely(VAR_2)
| ~ way(VAR_2)
| ~ street(VAR_2)
| ~ event(VAR_1)
| ~ city(VAR_0)
| ~ hollywood(VAR_0)
| hollywood(sK0) )
& ( in(sK2,sK1)
| hollywood(sK0) )
& ( down(sK2,sK4)
| hollywood(sK0) )
& ( barrel(sK2,sK3)
| hollywood(sK0) )
& ( lonely(sK4)
| hollywood(sK0) )
& ( way(sK4)
| hollywood(sK0) )
& ( street(sK4)
| hollywood(sK0) )
& ( old(sK3)
| hollywood(sK0) )
& ( dirty(sK3)
| hollywood(sK0) )
& ( white(sK3)
| hollywood(sK0) )
& ( car(sK3)
| hollywood(sK0) )
& ( chevy(sK3)
| hollywood(sK0) )
& ( event(sK2)
| hollywood(sK0) )
& ( city(sK1)
| hollywood(sK0) )
& ( hollywood(sK1)
| hollywood(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_co1_neg_sk]) ).
cnf(c_2,negated_conjecture,
( hollywood(sK1)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_3,negated_conjecture,
( city(sK1)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_4,negated_conjecture,
( event(sK2)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_5,negated_conjecture,
( chevy(sK3)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_6,negated_conjecture,
( car(sK3)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_7,negated_conjecture,
( white(sK3)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_8,negated_conjecture,
( dirty(sK3)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_9,negated_conjecture,
( old(sK3)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_10,negated_conjecture,
( street(sK4)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_11,negated_conjecture,
( way(sK4)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_12,negated_conjecture,
( lonely(sK4)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_13,negated_conjecture,
( barrel(sK2,sK3)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_14,negated_conjecture,
( down(sK2,sK4)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_15,negated_conjecture,
( in(sK2,sK1)
| hollywood(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_17,negated_conjecture,
( hollywood(sK1)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_18,negated_conjecture,
( city(sK1)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_19,negated_conjecture,
( event(sK2)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_20,negated_conjecture,
( chevy(sK3)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_21,negated_conjecture,
( car(sK3)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_22,negated_conjecture,
( white(sK3)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_23,negated_conjecture,
( dirty(sK3)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_24,negated_conjecture,
( old(sK3)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_25,negated_conjecture,
( street(sK4)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_26,negated_conjecture,
( way(sK4)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_27,negated_conjecture,
( lonely(sK4)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_28,negated_conjecture,
( barrel(sK2,sK3)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_29,negated_conjecture,
( down(sK2,sK4)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_30,negated_conjecture,
( in(sK2,sK1)
| city(sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_32,negated_conjecture,
( hollywood(sK1)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_33,negated_conjecture,
( city(sK1)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_34,negated_conjecture,
( event(sK2)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_35,negated_conjecture,
( chevy(sK3)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_36,negated_conjecture,
( car(sK3)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_37,negated_conjecture,
( white(sK3)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_38,negated_conjecture,
( dirty(sK3)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_39,negated_conjecture,
( old(sK3)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_40,negated_conjecture,
( street(sK4)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_41,negated_conjecture,
( way(sK4)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_42,negated_conjecture,
( lonely(sK4)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_43,negated_conjecture,
( barrel(sK2,sK3)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_44,negated_conjecture,
( down(sK2,sK4)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_45,negated_conjecture,
( in(sK2,sK1)
| event(sK5) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_47,negated_conjecture,
( hollywood(sK1)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_48,negated_conjecture,
( city(sK1)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_49,negated_conjecture,
( event(sK2)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_50,negated_conjecture,
( chevy(sK3)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_51,negated_conjecture,
( car(sK3)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_52,negated_conjecture,
( white(sK3)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_53,negated_conjecture,
( dirty(sK3)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_54,negated_conjecture,
( old(sK3)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_55,negated_conjecture,
( street(sK4)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_56,negated_conjecture,
( way(sK4)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_57,negated_conjecture,
( lonely(sK4)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_58,negated_conjecture,
( barrel(sK2,sK3)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_59,negated_conjecture,
( down(sK2,sK4)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_60,negated_conjecture,
( in(sK2,sK1)
| street(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_62,negated_conjecture,
( hollywood(sK1)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_63,negated_conjecture,
( city(sK1)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_64,negated_conjecture,
( event(sK2)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_65,negated_conjecture,
( chevy(sK3)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_66,negated_conjecture,
( car(sK3)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_67,negated_conjecture,
( white(sK3)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_68,negated_conjecture,
( dirty(sK3)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_69,negated_conjecture,
( old(sK3)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_70,negated_conjecture,
( street(sK4)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_71,negated_conjecture,
( way(sK4)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_72,negated_conjecture,
( lonely(sK4)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_73,negated_conjecture,
( barrel(sK2,sK3)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_74,negated_conjecture,
( down(sK2,sK4)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_75,negated_conjecture,
( in(sK2,sK1)
| way(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_77,negated_conjecture,
( hollywood(sK1)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_78,negated_conjecture,
( city(sK1)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_79,negated_conjecture,
( event(sK2)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_80,negated_conjecture,
( chevy(sK3)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_81,negated_conjecture,
( car(sK3)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_82,negated_conjecture,
( white(sK3)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_83,negated_conjecture,
( dirty(sK3)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_84,negated_conjecture,
( old(sK3)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_85,negated_conjecture,
( street(sK4)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_86,negated_conjecture,
( way(sK4)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_87,negated_conjecture,
( lonely(sK4)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_88,negated_conjecture,
( barrel(sK2,sK3)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_89,negated_conjecture,
( down(sK2,sK4)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_90,negated_conjecture,
( in(sK2,sK1)
| lonely(sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_92,negated_conjecture,
( hollywood(sK1)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_93,negated_conjecture,
( city(sK1)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_94,negated_conjecture,
( event(sK2)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_95,negated_conjecture,
( chevy(sK3)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_96,negated_conjecture,
( car(sK3)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_97,negated_conjecture,
( white(sK3)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_98,negated_conjecture,
( dirty(sK3)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_99,negated_conjecture,
( old(sK3)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_100,negated_conjecture,
( street(sK4)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_101,negated_conjecture,
( way(sK4)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_102,negated_conjecture,
( lonely(sK4)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_103,negated_conjecture,
( barrel(sK2,sK3)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_104,negated_conjecture,
( down(sK2,sK4)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_105,negated_conjecture,
( in(sK2,sK1)
| chevy(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_107,negated_conjecture,
( hollywood(sK1)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_108,negated_conjecture,
( city(sK1)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_109,negated_conjecture,
( event(sK2)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_110,negated_conjecture,
( chevy(sK3)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_111,negated_conjecture,
( car(sK3)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_112,negated_conjecture,
( white(sK3)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_113,negated_conjecture,
( dirty(sK3)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_114,negated_conjecture,
( old(sK3)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_115,negated_conjecture,
( street(sK4)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_116,negated_conjecture,
( way(sK4)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_117,negated_conjecture,
( lonely(sK4)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_118,negated_conjecture,
( barrel(sK2,sK3)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_119,negated_conjecture,
( down(sK2,sK4)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_120,negated_conjecture,
( in(sK2,sK1)
| car(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_122,negated_conjecture,
( hollywood(sK1)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_123,negated_conjecture,
( city(sK1)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_124,negated_conjecture,
( event(sK2)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_125,negated_conjecture,
( chevy(sK3)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_126,negated_conjecture,
( car(sK3)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_127,negated_conjecture,
( white(sK3)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_128,negated_conjecture,
( dirty(sK3)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_129,negated_conjecture,
( old(sK3)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_130,negated_conjecture,
( street(sK4)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_131,negated_conjecture,
( way(sK4)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_132,negated_conjecture,
( lonely(sK4)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_133,negated_conjecture,
( barrel(sK2,sK3)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_134,negated_conjecture,
( down(sK2,sK4)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_135,negated_conjecture,
( in(sK2,sK1)
| white(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_137,negated_conjecture,
( hollywood(sK1)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_138,negated_conjecture,
( city(sK1)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_139,negated_conjecture,
( event(sK2)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_140,negated_conjecture,
( chevy(sK3)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_141,negated_conjecture,
( car(sK3)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_142,negated_conjecture,
( white(sK3)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_143,negated_conjecture,
( dirty(sK3)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_144,negated_conjecture,
( old(sK3)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_145,negated_conjecture,
( street(sK4)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_146,negated_conjecture,
( way(sK4)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_147,negated_conjecture,
( lonely(sK4)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_148,negated_conjecture,
( barrel(sK2,sK3)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_149,negated_conjecture,
( down(sK2,sK4)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_150,negated_conjecture,
( in(sK2,sK1)
| dirty(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_152,negated_conjecture,
( hollywood(sK1)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_153,negated_conjecture,
( city(sK1)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_154,negated_conjecture,
( event(sK2)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_155,negated_conjecture,
( chevy(sK3)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_156,negated_conjecture,
( car(sK3)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_157,negated_conjecture,
( white(sK3)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_158,negated_conjecture,
( dirty(sK3)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_159,negated_conjecture,
( old(sK3)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_160,negated_conjecture,
( street(sK4)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_161,negated_conjecture,
( way(sK4)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_162,negated_conjecture,
( lonely(sK4)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_163,negated_conjecture,
( barrel(sK2,sK3)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_164,negated_conjecture,
( down(sK2,sK4)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_165,negated_conjecture,
( in(sK2,sK1)
| old(sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_167,negated_conjecture,
( hollywood(sK1)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_168,negated_conjecture,
( city(sK1)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_169,negated_conjecture,
( event(sK2)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_170,negated_conjecture,
( chevy(sK3)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_171,negated_conjecture,
( car(sK3)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_172,negated_conjecture,
( white(sK3)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_173,negated_conjecture,
( dirty(sK3)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_174,negated_conjecture,
( old(sK3)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_175,negated_conjecture,
( street(sK4)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_176,negated_conjecture,
( way(sK4)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_177,negated_conjecture,
( lonely(sK4)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_178,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_179,negated_conjecture,
( down(sK2,sK4)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_180,negated_conjecture,
( in(sK2,sK1)
| barrel(sK5,sK7) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_182,negated_conjecture,
( hollywood(sK1)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_183,negated_conjecture,
( city(sK1)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_184,negated_conjecture,
( event(sK2)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_185,negated_conjecture,
( chevy(sK3)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_186,negated_conjecture,
( car(sK3)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_187,negated_conjecture,
( white(sK3)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_188,negated_conjecture,
( dirty(sK3)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_189,negated_conjecture,
( old(sK3)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_190,negated_conjecture,
( street(sK4)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_191,negated_conjecture,
( way(sK4)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_192,negated_conjecture,
( lonely(sK4)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_193,negated_conjecture,
( barrel(sK2,sK3)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_194,negated_conjecture,
( down(sK2,sK4)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_195,negated_conjecture,
( in(sK2,sK1)
| down(sK5,sK6) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_197,negated_conjecture,
( hollywood(sK1)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_198,negated_conjecture,
( city(sK1)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_199,negated_conjecture,
( event(sK2)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_200,negated_conjecture,
( chevy(sK3)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_201,negated_conjecture,
( car(sK3)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_202,negated_conjecture,
( white(sK3)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_203,negated_conjecture,
( dirty(sK3)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_204,negated_conjecture,
( old(sK3)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_205,negated_conjecture,
( street(sK4)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_206,negated_conjecture,
( way(sK4)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_207,negated_conjecture,
( lonely(sK4)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_208,negated_conjecture,
( barrel(sK2,sK3)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_209,negated_conjecture,
( down(sK2,sK4)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_210,negated_conjecture,
( in(sK2,sK1)
| in(sK5,sK0) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_226,negated_conjecture,
( ~ in(F,E)
| ~ down(F,V6)
| ~ barrel(F,V7)
| ~ old(V7)
| ~ dirty(V7)
| ~ white(V7)
| ~ car(V7)
| ~ chevy(V7)
| ~ lonely(V6)
| ~ way(V6)
| ~ street(V6)
| ~ event(F)
| ~ city(E)
| ~ hollywood(E)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_934,plain,
( ~ in(E,A)
| ~ down(E,F)
| ~ barrel(E,V6)
| ~ old(V6)
| ~ dirty(V6)
| ~ white(V6)
| ~ car(V6)
| ~ chevy(V6)
| ~ lonely(F)
| ~ way(F)
| ~ street(F)
| ~ event(E)
| ~ city(A)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(factor,[status(thm)],[c_226]) ).
cnf(c_227,plain,
( ~ in(E,A)
| ~ down(E,F)
| ~ barrel(E,V6)
| ~ old(V6)
| ~ dirty(V6)
| ~ white(V6)
| ~ car(V6)
| ~ chevy(V6)
| ~ lonely(F)
| ~ way(F)
| ~ street(F)
| ~ event(E)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_934]) ).
cnf(c_935,plain,
( ~ in(E,A)
| ~ down(E,F)
| ~ barrel(E,C)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ lonely(F)
| ~ way(F)
| ~ street(F)
| ~ event(E)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(factor,[status(thm)],[c_227]) ).
cnf(c_936,plain,
( ~ in(E,A)
| ~ down(E,F)
| ~ barrel(E,C)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ lonely(F)
| ~ way(F)
| ~ street(F)
| ~ event(E)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_935]) ).
cnf(c_937,plain,
( ~ in(E,A)
| ~ down(E,F)
| ~ barrel(E,C)
| ~ old(C)
| ~ dirty(C)
| ~ lonely(F)
| ~ way(F)
| ~ street(F)
| ~ event(E)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_936]) ).
cnf(c_938,plain,
( ~ in(E,A)
| ~ down(E,F)
| ~ barrel(E,C)
| ~ old(C)
| ~ lonely(F)
| ~ way(F)
| ~ street(F)
| ~ event(E)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_937]) ).
cnf(c_234,plain,
( ~ in(E,A)
| ~ down(E,F)
| ~ barrel(E,C)
| ~ lonely(F)
| ~ way(F)
| ~ street(F)
| ~ event(E)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_938]) ).
cnf(c_939,plain,
( ~ in(B,A)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ event(B)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(factor,[status(thm)],[c_234]) ).
cnf(c_940,plain,
( ~ in(B,A)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_939]) ).
cnf(c_941,plain,
( ~ in(B,A)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_940]) ).
cnf(c_942,plain,
( ~ in(B,A)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_941]) ).
cnf(c_943,plain,
( ~ in(B,A)
| ~ barrel(B,C)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_942]) ).
cnf(c_944,plain,
( ~ in(B,A)
| ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_943]) ).
cnf(c_241,plain,
( ~ in(B,A)
| ~ down(B,D)
| ~ barrel(B,C)
| ~ lonely(D)
| ~ way(D)
| ~ street(D)
| ~ old(C)
| ~ dirty(C)
| ~ white(C)
| ~ car(C)
| ~ chevy(C)
| ~ event(B)
| ~ city(A)
| ~ hollywood(A) ),
inference(copy,[status(thm)],[c_944]) ).
cnf(c_242,plain,
( in(sK5,sK0)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_210]) ).
cnf(c_245,plain,
( barrel(sK2,sK3)
| ~ down(sK5,B)
| ~ barrel(sK5,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_241,c_208]) ).
cnf(c_246,plain,
( lonely(sK4)
| ~ down(sK5,B)
| ~ barrel(sK5,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_241,c_207]) ).
cnf(c_247,plain,
( way(sK4)
| ~ down(sK5,B)
| ~ barrel(sK5,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_241,c_206]) ).
cnf(c_248,plain,
( street(sK4)
| ~ down(sK5,B)
| ~ barrel(sK5,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_241,c_205]) ).
cnf(c_249,plain,
( old(sK3)
| ~ down(sK5,B)
| ~ barrel(sK5,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_241,c_204]) ).
cnf(c_250,plain,
( dirty(sK3)
| ~ down(sK5,B)
| ~ barrel(sK5,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_241,c_203]) ).
cnf(c_257,plain,
( down(sK5,sK6)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_195]) ).
cnf(c_258,plain,
( barrel(sK5,sK7)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_180]) ).
cnf(c_259,plain,
( old(sK7)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_165]) ).
cnf(c_260,plain,
( dirty(sK7)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_150]) ).
cnf(c_261,plain,
( white(sK7)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_135]) ).
cnf(c_262,plain,
( car(sK7)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_120]) ).
cnf(c_263,plain,
( chevy(sK7)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_105]) ).
cnf(c_264,plain,
( lonely(sK6)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_90]) ).
cnf(c_265,plain,
( way(sK6)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_75]) ).
cnf(c_266,plain,
( street(sK6)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_60]) ).
cnf(c_267,plain,
( event(sK5)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_45]) ).
cnf(c_268,plain,
( city(sK0)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_30]) ).
cnf(c_269,plain,
( hollywood(sK0)
| ~ down(sK2,B)
| ~ barrel(sK2,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_241,c_15]) ).
cnf(c_945,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_242,c_209]) ).
cnf(c_270,negated_conjecture,
( in(sK5,sK0)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_945]) ).
cnf(c_946,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_270,c_208]) ).
cnf(c_273,negated_conjecture,
( in(sK5,sK0)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_946]) ).
cnf(c_947,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_273,c_202]) ).
cnf(c_274,negated_conjecture,
( in(sK5,sK0)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_947]) ).
cnf(c_948,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ lonely(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_274,c_206]) ).
cnf(c_275,negated_conjecture,
( in(sK5,sK0)
| ~ lonely(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_948]) ).
cnf(c_949,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ lonely(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_275,c_205]) ).
cnf(c_276,negated_conjecture,
( in(sK5,sK0)
| ~ lonely(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_949]) ).
cnf(c_950,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ lonely(sK4)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_276,c_204]) ).
cnf(c_277,negated_conjecture,
( in(sK5,sK0)
| ~ lonely(sK4)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_950]) ).
cnf(c_951,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_277,c_207]) ).
cnf(c_278,negated_conjecture,
( in(sK5,sK0)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_951]) ).
cnf(c_952,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_245,c_193]) ).
cnf(c_279,negated_conjecture,
( barrel(sK2,sK3)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_952]) ).
cnf(c_953,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_246,c_192]) ).
cnf(c_280,negated_conjecture,
( lonely(sK4)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_953]) ).
cnf(c_954,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_247,c_191]) ).
cnf(c_281,negated_conjecture,
( way(sK4)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_954]) ).
cnf(c_955,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_278,c_197]) ).
cnf(c_282,negated_conjecture,
( in(sK5,sK0)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_955]) ).
cnf(c_956,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_282,c_199]) ).
cnf(c_283,negated_conjecture,
( in(sK5,sK0)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_956]) ).
cnf(c_957,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_283,c_203]) ).
cnf(c_284,negated_conjecture,
( in(sK5,sK0)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_957]) ).
cnf(c_958,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_284,c_198]) ).
cnf(c_285,negated_conjecture,
( in(sK5,sK0)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_958]) ).
cnf(c_959,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0)
| ~ car(sK3) ),
inference(resolve,[status(thm)],[c_285,c_200]) ).
cnf(c_286,negated_conjecture,
( in(sK5,sK0)
| ~ car(sK3) ),
inference(copy,[status(thm)],[c_959]) ).
cnf(c_960,negated_conjecture,
( in(sK5,sK0)
| in(sK5,sK0) ),
inference(resolve,[status(thm)],[c_286,c_201]) ).
cnf(c_287,negated_conjecture,
in(sK5,sK0),
inference(copy,[status(thm)],[c_960]) ).
cnf(c_961,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_248,c_190]) ).
cnf(c_288,negated_conjecture,
( street(sK4)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_961]) ).
cnf(c_962,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_249,c_189]) ).
cnf(c_289,negated_conjecture,
( old(sK3)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_962]) ).
cnf(c_963,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_250,c_188]) ).
cnf(c_290,negated_conjecture,
( dirty(sK3)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_963]) ).
cnf(c_291,plain,
( ~ down(sK5,B)
| ~ barrel(sK5,A)
| ~ lonely(B)
| ~ way(B)
| ~ street(B)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_287,c_241]) ).
cnf(c_964,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_280,c_177]) ).
cnf(c_295,negated_conjecture,
( lonely(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_964]) ).
cnf(c_965,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_295,c_132]) ).
cnf(c_299,negated_conjecture,
( lonely(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_965]) ).
cnf(c_966,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_299,c_72]) ).
cnf(c_303,negated_conjecture,
( lonely(sK4)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_966]) ).
cnf(c_967,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_303,c_57]) ).
cnf(c_307,negated_conjecture,
( lonely(sK4)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_967]) ).
cnf(c_968,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_307,c_162]) ).
cnf(c_311,negated_conjecture,
( lonely(sK4)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_968]) ).
cnf(c_969,negated_conjecture,
( down(sK5,sK6)
| down(sK5,sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_257,c_194]) ).
cnf(c_312,negated_conjecture,
( down(sK5,sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_969]) ).
cnf(c_970,negated_conjecture,
( barrel(sK5,sK7)
| barrel(sK5,sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_258,c_179]) ).
cnf(c_313,negated_conjecture,
( barrel(sK5,sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_970]) ).
cnf(c_971,negated_conjecture,
( old(sK7)
| old(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_259,c_164]) ).
cnf(c_314,negated_conjecture,
( old(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_971]) ).
cnf(c_316,plain,
( car(sK3)
| ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_291,c_186]) ).
cnf(c_972,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_311,c_87]) ).
cnf(c_324,negated_conjecture,
( lonely(sK4)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_972]) ).
cnf(c_973,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_324,c_12]) ).
cnf(c_328,negated_conjecture,
( lonely(sK4)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_973]) ).
cnf(c_974,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_328,c_42]) ).
cnf(c_332,negated_conjecture,
( lonely(sK4)
| ~ dirty(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_974]) ).
cnf(c_975,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_332,c_147]) ).
cnf(c_336,negated_conjecture,
( lonely(sK4)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_975]) ).
cnf(c_976,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ car(sK7)
| ~ chevy(sK7) ),
inference(resolve,[status(thm)],[c_336,c_27]) ).
cnf(c_340,negated_conjecture,
( lonely(sK4)
| ~ car(sK7)
| ~ chevy(sK7) ),
inference(copy,[status(thm)],[c_976]) ).
cnf(c_977,negated_conjecture,
( lonely(sK4)
| lonely(sK4)
| ~ car(sK7) ),
inference(resolve,[status(thm)],[c_340,c_102]) ).
cnf(c_344,negated_conjecture,
( lonely(sK4)
| ~ car(sK7) ),
inference(copy,[status(thm)],[c_977]) ).
cnf(c_978,negated_conjecture,
( dirty(sK7)
| dirty(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_260,c_149]) ).
cnf(c_345,negated_conjecture,
( dirty(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_978]) ).
cnf(c_979,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_261,c_134]) ).
cnf(c_346,negated_conjecture,
( white(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_979]) ).
cnf(c_980,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_262,c_119]) ).
cnf(c_347,negated_conjecture,
( car(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_980]) ).
cnf(c_981,negated_conjecture,
( lonely(sK4)
| lonely(sK4) ),
inference(resolve,[status(thm)],[c_344,c_117]) ).
cnf(c_351,negated_conjecture,
lonely(sK4),
inference(copy,[status(thm)],[c_981]) ).
cnf(c_352,negated_conjecture,
( car(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_347]) ).
cnf(c_353,negated_conjecture,
( white(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_346]) ).
cnf(c_354,negated_conjecture,
( dirty(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_345]) ).
cnf(c_355,negated_conjecture,
( old(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_314]) ).
cnf(c_356,negated_conjecture,
( barrel(sK5,sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_313]) ).
cnf(c_357,negated_conjecture,
( down(sK5,sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_312]) ).
cnf(c_982,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_352,c_118]) ).
cnf(c_363,negated_conjecture,
( car(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_982]) ).
cnf(c_983,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_363,c_112]) ).
cnf(c_369,negated_conjecture,
( car(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_983]) ).
cnf(c_984,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_369,c_116]) ).
cnf(c_375,negated_conjecture,
( car(sK7)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_984]) ).
cnf(c_985,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_375,c_115]) ).
cnf(c_381,negated_conjecture,
( car(sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_985]) ).
cnf(c_986,negated_conjecture,
( chevy(sK7)
| chevy(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_263,c_104]) ).
cnf(c_987,negated_conjecture,
( chevy(sK7)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_986]) ).
cnf(c_382,negated_conjecture,
( chevy(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_987]) ).
cnf(c_988,negated_conjecture,
( lonely(sK6)
| lonely(sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_264,c_89]) ).
cnf(c_989,negated_conjecture,
( lonely(sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_988]) ).
cnf(c_383,negated_conjecture,
( lonely(sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_989]) ).
cnf(c_990,negated_conjecture,
( way(sK6)
| way(sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_265,c_74]) ).
cnf(c_991,negated_conjecture,
( way(sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_990]) ).
cnf(c_384,negated_conjecture,
( way(sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_991]) ).
cnf(c_992,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_381,c_114]) ).
cnf(c_390,negated_conjecture,
( car(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_992]) ).
cnf(c_993,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_390,c_107]) ).
cnf(c_396,negated_conjecture,
( car(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_993]) ).
cnf(c_994,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_396,c_109]) ).
cnf(c_402,negated_conjecture,
( car(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_994]) ).
cnf(c_995,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_402,c_113]) ).
cnf(c_408,negated_conjecture,
( car(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_995]) ).
cnf(c_996,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_408,c_108]) ).
cnf(c_414,negated_conjecture,
( car(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_996]) ).
cnf(c_997,negated_conjecture,
( car(sK7)
| car(sK7)
| ~ car(sK3) ),
inference(resolve,[status(thm)],[c_414,c_110]) ).
cnf(c_420,negated_conjecture,
( car(sK7)
| ~ car(sK3) ),
inference(copy,[status(thm)],[c_997]) ).
cnf(c_998,negated_conjecture,
( street(sK6)
| street(sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_266,c_59]) ).
cnf(c_999,negated_conjecture,
( street(sK6)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_998]) ).
cnf(c_421,negated_conjecture,
( street(sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_999]) ).
cnf(c_1000,negated_conjecture,
( event(sK5)
| event(sK5)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_267,c_44]) ).
cnf(c_1001,negated_conjecture,
( event(sK5)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1000]) ).
cnf(c_422,negated_conjecture,
( event(sK5)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_1001]) ).
cnf(c_1002,negated_conjecture,
( city(sK0)
| city(sK0)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_268,c_29]) ).
cnf(c_1003,negated_conjecture,
( city(sK0)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1002]) ).
cnf(c_423,negated_conjecture,
( city(sK0)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_1003]) ).
cnf(c_1004,negated_conjecture,
( car(sK7)
| car(sK7) ),
inference(resolve,[status(thm)],[c_420,c_111]) ).
cnf(c_429,negated_conjecture,
car(sK7),
inference(copy,[status(thm)],[c_1004]) ).
cnf(c_1005,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_353,c_133]) ).
cnf(c_434,negated_conjecture,
( white(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1005]) ).
cnf(c_1006,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_434,c_127]) ).
cnf(c_439,negated_conjecture,
( white(sK7)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1006]) ).
cnf(c_1007,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_439,c_131]) ).
cnf(c_444,negated_conjecture,
( white(sK7)
| ~ street(sK4)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1007]) ).
cnf(c_1008,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_444,c_130]) ).
cnf(c_449,negated_conjecture,
( white(sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1008]) ).
cnf(c_1009,negated_conjecture,
( hollywood(sK0)
| hollywood(sK0)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_269,c_14]) ).
cnf(c_1010,negated_conjecture,
( hollywood(sK0)
| ~ barrel(sK2,A)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1009]) ).
cnf(c_450,negated_conjecture,
( hollywood(sK0)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ street(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_351,c_1010]) ).
cnf(c_1011,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_449,c_129]) ).
cnf(c_457,negated_conjecture,
( white(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1011]) ).
cnf(c_1012,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_457,c_122]) ).
cnf(c_462,negated_conjecture,
( white(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1012]) ).
cnf(c_1013,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_462,c_124]) ).
cnf(c_467,negated_conjecture,
( white(sK7)
| ~ dirty(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1013]) ).
cnf(c_1014,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_467,c_128]) ).
cnf(c_472,negated_conjecture,
( white(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1014]) ).
cnf(c_1015,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_472,c_123]) ).
cnf(c_477,negated_conjecture,
( white(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1015]) ).
cnf(c_1016,negated_conjecture,
( white(sK7)
| white(sK7)
| ~ car(sK3) ),
inference(resolve,[status(thm)],[c_477,c_125]) ).
cnf(c_482,negated_conjecture,
( white(sK7)
| ~ car(sK3) ),
inference(copy,[status(thm)],[c_1016]) ).
cnf(c_1017,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_279,c_178]) ).
cnf(c_1018,negated_conjecture,
( barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1017]) ).
cnf(c_483,negated_conjecture,
( barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_429,c_1018]) ).
cnf(c_1019,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_281,c_176]) ).
cnf(c_1020,negated_conjecture,
( way(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1019]) ).
cnf(c_484,negated_conjecture,
( way(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_429,c_1020]) ).
cnf(c_1021,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_288,c_175]) ).
cnf(c_1022,negated_conjecture,
( street(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1021]) ).
cnf(c_485,negated_conjecture,
( street(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_429,c_1022]) ).
cnf(c_1023,negated_conjecture,
( white(sK7)
| white(sK7) ),
inference(resolve,[status(thm)],[c_482,c_126]) ).
cnf(c_490,negated_conjecture,
white(sK7),
inference(copy,[status(thm)],[c_1023]) ).
cnf(c_491,negated_conjecture,
( street(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_490,c_485]) ).
cnf(c_492,negated_conjecture,
( way(sK4)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_490,c_484]) ).
cnf(c_493,negated_conjecture,
( barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_490,c_483]) ).
cnf(c_1024,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_491,c_70]) ).
cnf(c_500,negated_conjecture,
( street(sK4)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1024]) ).
cnf(c_1025,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_500,c_55]) ).
cnf(c_505,negated_conjecture,
( street(sK4)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1025]) ).
cnf(c_1026,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_505,c_160]) ).
cnf(c_510,negated_conjecture,
( street(sK4)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1026]) ).
cnf(c_1027,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_510,c_85]) ).
cnf(c_515,negated_conjecture,
( street(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1027]) ).
cnf(c_1028,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_289,c_174]) ).
cnf(c_1029,negated_conjecture,
( old(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1028]) ).
cnf(c_1030,negated_conjecture,
( old(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_429,c_1029]) ).
cnf(c_516,negated_conjecture,
( old(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_490,c_1030]) ).
cnf(c_1031,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_290,c_173]) ).
cnf(c_1032,negated_conjecture,
( dirty(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1031]) ).
cnf(c_1033,negated_conjecture,
( dirty(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_429,c_1032]) ).
cnf(c_517,negated_conjecture,
( dirty(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_490,c_1033]) ).
cnf(c_1034,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_515,c_10]) ).
cnf(c_523,negated_conjecture,
( street(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1034]) ).
cnf(c_1035,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_523,c_40]) ).
cnf(c_528,negated_conjecture,
( street(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1035]) ).
cnf(c_1036,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_528,c_145]) ).
cnf(c_533,negated_conjecture,
( street(sK4)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1036]) ).
cnf(c_1037,negated_conjecture,
( street(sK4)
| street(sK4)
| ~ chevy(sK7) ),
inference(resolve,[status(thm)],[c_533,c_25]) ).
cnf(c_538,negated_conjecture,
( street(sK4)
| ~ chevy(sK7) ),
inference(copy,[status(thm)],[c_1037]) ).
cnf(c_1038,negated_conjecture,
( street(sK4)
| street(sK4) ),
inference(resolve,[status(thm)],[c_538,c_100]) ).
cnf(c_543,negated_conjecture,
street(sK4),
inference(copy,[status(thm)],[c_1038]) ).
cnf(c_544,negated_conjecture,
( hollywood(sK0)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_450]) ).
cnf(c_545,negated_conjecture,
( city(sK0)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_423]) ).
cnf(c_546,negated_conjecture,
( event(sK5)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_422]) ).
cnf(c_547,negated_conjecture,
( street(sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_421]) ).
cnf(c_548,negated_conjecture,
( way(sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_384]) ).
cnf(c_549,negated_conjecture,
( lonely(sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_383]) ).
cnf(c_550,negated_conjecture,
( chevy(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_382]) ).
cnf(c_551,negated_conjecture,
( down(sK5,sK6)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_357]) ).
cnf(c_552,negated_conjecture,
( barrel(sK5,sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_356]) ).
cnf(c_553,negated_conjecture,
( old(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_355]) ).
cnf(c_554,negated_conjecture,
( dirty(sK7)
| ~ barrel(sK2,A)
| ~ way(sK4)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_543,c_354]) ).
cnf(c_1039,negated_conjecture,
( car(sK3)
| car(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_316,c_171]) ).
cnf(c_1040,negated_conjecture,
( car(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1039]) ).
cnf(c_1041,negated_conjecture,
( car(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_429,c_1040]) ).
cnf(c_555,negated_conjecture,
( car(sK3)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_490,c_1041]) ).
cnf(c_1042,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_492,c_71]) ).
cnf(c_561,negated_conjecture,
( way(sK4)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1042]) ).
cnf(c_1043,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_561,c_56]) ).
cnf(c_565,negated_conjecture,
( way(sK4)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1043]) ).
cnf(c_1044,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_565,c_161]) ).
cnf(c_569,negated_conjecture,
( way(sK4)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1044]) ).
cnf(c_1045,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_569,c_86]) ).
cnf(c_573,negated_conjecture,
( way(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1045]) ).
cnf(c_1046,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_573,c_11]) ).
cnf(c_577,negated_conjecture,
( way(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1046]) ).
cnf(c_1047,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_577,c_41]) ).
cnf(c_581,negated_conjecture,
( way(sK4)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1047]) ).
cnf(c_1048,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_493,c_73]) ).
cnf(c_586,negated_conjecture,
( barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1048]) ).
cnf(c_1049,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_581,c_146]) ).
cnf(c_590,negated_conjecture,
( way(sK4)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1049]) ).
cnf(c_1050,negated_conjecture,
( way(sK4)
| way(sK4)
| ~ chevy(sK7) ),
inference(resolve,[status(thm)],[c_590,c_26]) ).
cnf(c_594,negated_conjecture,
( way(sK4)
| ~ chevy(sK7) ),
inference(copy,[status(thm)],[c_1050]) ).
cnf(c_1051,negated_conjecture,
( way(sK4)
| way(sK4) ),
inference(resolve,[status(thm)],[c_594,c_101]) ).
cnf(c_598,negated_conjecture,
way(sK4),
inference(copy,[status(thm)],[c_1051]) ).
cnf(c_599,negated_conjecture,
( dirty(sK7)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_554]) ).
cnf(c_600,negated_conjecture,
( old(sK7)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_553]) ).
cnf(c_601,negated_conjecture,
( barrel(sK5,sK7)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_552]) ).
cnf(c_602,negated_conjecture,
( down(sK5,sK6)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_551]) ).
cnf(c_603,negated_conjecture,
( chevy(sK7)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_550]) ).
cnf(c_604,negated_conjecture,
( lonely(sK6)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_549]) ).
cnf(c_605,negated_conjecture,
( way(sK6)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_548]) ).
cnf(c_606,negated_conjecture,
( street(sK6)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_547]) ).
cnf(c_607,negated_conjecture,
( event(sK5)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_546]) ).
cnf(c_608,negated_conjecture,
( city(sK0)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_545]) ).
cnf(c_609,negated_conjecture,
( hollywood(sK0)
| ~ barrel(sK2,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_598,c_544]) ).
cnf(c_1052,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_586,c_58]) ).
cnf(c_612,negated_conjecture,
( barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1052]) ).
cnf(c_1053,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_612,c_163]) ).
cnf(c_615,negated_conjecture,
( barrel(sK2,sK3)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1053]) ).
cnf(c_1054,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_516,c_69]) ).
cnf(c_619,negated_conjecture,
( old(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1054]) ).
cnf(c_1055,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_615,c_88]) ).
cnf(c_622,negated_conjecture,
( barrel(sK2,sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1055]) ).
cnf(c_1056,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_622,c_13]) ).
cnf(c_625,negated_conjecture,
( barrel(sK2,sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1056]) ).
cnf(c_1057,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_625,c_43]) ).
cnf(c_628,negated_conjecture,
( barrel(sK2,sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1057]) ).
cnf(c_1058,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_628,c_148]) ).
cnf(c_631,negated_conjecture,
( barrel(sK2,sK3)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1058]) ).
cnf(c_1059,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3)
| ~ chevy(sK7) ),
inference(resolve,[status(thm)],[c_631,c_28]) ).
cnf(c_634,negated_conjecture,
( barrel(sK2,sK3)
| ~ chevy(sK7) ),
inference(copy,[status(thm)],[c_1059]) ).
cnf(c_1060,negated_conjecture,
( barrel(sK2,sK3)
| barrel(sK2,sK3) ),
inference(resolve,[status(thm)],[c_634,c_103]) ).
cnf(c_637,negated_conjecture,
barrel(sK2,sK3),
inference(copy,[status(thm)],[c_1060]) ).
cnf(c_1061,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_517,c_68]) ).
cnf(c_638,negated_conjecture,
( dirty(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1061]) ).
cnf(c_1062,negated_conjecture,
( car(sK3)
| car(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_555,c_66]) ).
cnf(c_640,negated_conjecture,
( car(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1062]) ).
cnf(c_1063,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_619,c_54]) ).
cnf(c_643,negated_conjecture,
( old(sK3)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1063]) ).
cnf(c_1064,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_643,c_159]) ).
cnf(c_646,negated_conjecture,
( old(sK3)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1064]) ).
cnf(c_1065,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_646,c_84]) ).
cnf(c_649,negated_conjecture,
( old(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1065]) ).
cnf(c_1066,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_649,c_9]) ).
cnf(c_652,negated_conjecture,
( old(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1066]) ).
cnf(c_1067,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_652,c_39]) ).
cnf(c_655,negated_conjecture,
( old(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1067]) ).
cnf(c_1068,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_655,c_144]) ).
cnf(c_661,negated_conjecture,
( old(sK3)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1068]) ).
cnf(c_1069,negated_conjecture,
( old(sK3)
| old(sK3)
| ~ chevy(sK7) ),
inference(resolve,[status(thm)],[c_661,c_24]) ).
cnf(c_664,negated_conjecture,
( old(sK3)
| ~ chevy(sK7) ),
inference(copy,[status(thm)],[c_1069]) ).
cnf(c_1070,negated_conjecture,
( old(sK3)
| old(sK3) ),
inference(resolve,[status(thm)],[c_664,c_99]) ).
cnf(c_667,negated_conjecture,
old(sK3),
inference(copy,[status(thm)],[c_1070]) ).
cnf(c_1071,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_638,c_53]) ).
cnf(c_670,negated_conjecture,
( dirty(sK3)
| ~ lonely(sK6)
| ~ old(sK7)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1071]) ).
cnf(c_1072,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_670,c_158]) ).
cnf(c_673,negated_conjecture,
( dirty(sK3)
| ~ lonely(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1072]) ).
cnf(c_1073,plain,
( dirty(sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_599,c_637]) ).
cnf(c_675,plain,
( dirty(sK7)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1073]) ).
cnf(c_1074,plain,
( old(sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_600,c_637]) ).
cnf(c_676,plain,
( old(sK7)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1074]) ).
cnf(c_1075,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_673,c_83]) ).
cnf(c_679,negated_conjecture,
( dirty(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1075]) ).
cnf(c_1076,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_679,c_8]) ).
cnf(c_682,negated_conjecture,
( dirty(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1076]) ).
cnf(c_1077,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_682,c_38]) ).
cnf(c_685,negated_conjecture,
( dirty(sK3)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1077]) ).
cnf(c_1078,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_685,c_143]) ).
cnf(c_688,negated_conjecture,
( dirty(sK3)
| ~ chevy(sK7)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1078]) ).
cnf(c_1079,negated_conjecture,
( dirty(sK3)
| dirty(sK3)
| ~ chevy(sK7) ),
inference(resolve,[status(thm)],[c_688,c_23]) ).
cnf(c_691,negated_conjecture,
( dirty(sK3)
| ~ chevy(sK7) ),
inference(copy,[status(thm)],[c_1079]) ).
cnf(c_1080,negated_conjecture,
( dirty(sK3)
| dirty(sK3) ),
inference(resolve,[status(thm)],[c_691,c_98]) ).
cnf(c_694,negated_conjecture,
dirty(sK3),
inference(copy,[status(thm)],[c_1080]) ).
cnf(c_695,plain,
( old(sK7)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_676]) ).
cnf(c_696,plain,
( dirty(sK7)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_675]) ).
cnf(c_1081,plain,
( barrel(sK5,sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_601,c_637]) ).
cnf(c_1082,plain,
( barrel(sK5,sK7)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1081]) ).
cnf(c_697,plain,
( barrel(sK5,sK7)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1082]) ).
cnf(c_1083,plain,
( down(sK5,sK6)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_602,c_637]) ).
cnf(c_1084,plain,
( down(sK5,sK6)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1083]) ).
cnf(c_698,plain,
( down(sK5,sK6)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1084]) ).
cnf(c_1085,plain,
( chevy(sK7)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_603,c_637]) ).
cnf(c_1086,plain,
( chevy(sK7)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1085]) ).
cnf(c_699,plain,
( chevy(sK7)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1086]) ).
cnf(c_1087,negated_conjecture,
( old(sK7)
| old(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_695,c_157]) ).
cnf(c_702,negated_conjecture,
( old(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1087]) ).
cnf(c_1088,negated_conjecture,
( old(sK7)
| old(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_702,c_152]) ).
cnf(c_705,negated_conjecture,
( old(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1088]) ).
cnf(c_1089,negated_conjecture,
( old(sK7)
| old(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_705,c_154]) ).
cnf(c_708,negated_conjecture,
( old(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1089]) ).
cnf(c_1090,negated_conjecture,
( old(sK7)
| old(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_708,c_153]) ).
cnf(c_711,negated_conjecture,
( old(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1090]) ).
cnf(c_1091,negated_conjecture,
( old(sK7)
| old(sK7)
| ~ car(sK3) ),
inference(resolve,[status(thm)],[c_711,c_155]) ).
cnf(c_714,negated_conjecture,
( old(sK7)
| ~ car(sK3) ),
inference(copy,[status(thm)],[c_1091]) ).
cnf(c_1092,plain,
( lonely(sK6)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_604,c_637]) ).
cnf(c_1093,plain,
( lonely(sK6)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1092]) ).
cnf(c_715,plain,
( lonely(sK6)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1093]) ).
cnf(c_1094,plain,
( way(sK6)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_605,c_637]) ).
cnf(c_1095,plain,
( way(sK6)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1094]) ).
cnf(c_716,plain,
( way(sK6)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1095]) ).
cnf(c_1096,plain,
( street(sK6)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_606,c_637]) ).
cnf(c_1097,plain,
( street(sK6)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1096]) ).
cnf(c_717,plain,
( street(sK6)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1097]) ).
cnf(c_1098,negated_conjecture,
( old(sK7)
| old(sK7) ),
inference(resolve,[status(thm)],[c_714,c_156]) ).
cnf(c_720,negated_conjecture,
old(sK7),
inference(copy,[status(thm)],[c_1098]) ).
cnf(c_725,negated_conjecture,
( car(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ dirty(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_720,c_640]) ).
cnf(c_1099,negated_conjecture,
( dirty(sK7)
| dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_696,c_142]) ).
cnf(c_731,negated_conjecture,
( dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1099]) ).
cnf(c_1100,negated_conjecture,
( dirty(sK7)
| dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_731,c_137]) ).
cnf(c_734,negated_conjecture,
( dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1100]) ).
cnf(c_1101,negated_conjecture,
( dirty(sK7)
| dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_734,c_139]) ).
cnf(c_737,negated_conjecture,
( dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1101]) ).
cnf(c_1102,negated_conjecture,
( dirty(sK7)
| dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_737,c_138]) ).
cnf(c_740,negated_conjecture,
( dirty(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1102]) ).
cnf(c_1103,plain,
( event(sK5)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_607,c_637]) ).
cnf(c_1104,plain,
( event(sK5)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1103]) ).
cnf(c_741,plain,
( event(sK5)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1104]) ).
cnf(c_1105,plain,
( city(sK0)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_608,c_637]) ).
cnf(c_1106,plain,
( city(sK0)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1105]) ).
cnf(c_742,plain,
( city(sK0)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1106]) ).
cnf(c_1107,plain,
( hollywood(sK0)
| ~ old(sK3)
| ~ dirty(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_609,c_637]) ).
cnf(c_1108,plain,
( hollywood(sK0)
| ~ old(sK3)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_694,c_1107]) ).
cnf(c_743,plain,
( hollywood(sK0)
| ~ white(sK3)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_667,c_1108]) ).
cnf(c_1109,negated_conjecture,
( dirty(sK7)
| dirty(sK7)
| ~ car(sK3) ),
inference(resolve,[status(thm)],[c_740,c_140]) ).
cnf(c_746,negated_conjecture,
( dirty(sK7)
| ~ car(sK3) ),
inference(copy,[status(thm)],[c_1109]) ).
cnf(c_1110,negated_conjecture,
( dirty(sK7)
| dirty(sK7) ),
inference(resolve,[status(thm)],[c_746,c_141]) ).
cnf(c_749,negated_conjecture,
dirty(sK7),
inference(copy,[status(thm)],[c_1110]) ).
cnf(c_753,negated_conjecture,
( car(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_749,c_725]) ).
cnf(c_1111,negated_conjecture,
( chevy(sK7)
| chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_699,c_97]) ).
cnf(c_760,negated_conjecture,
( chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1111]) ).
cnf(c_1112,negated_conjecture,
( chevy(sK7)
| chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_760,c_92]) ).
cnf(c_763,negated_conjecture,
( chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1112]) ).
cnf(c_1113,negated_conjecture,
( chevy(sK7)
| chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_763,c_94]) ).
cnf(c_766,negated_conjecture,
( chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1113]) ).
cnf(c_1114,negated_conjecture,
( barrel(sK5,sK7)
| barrel(sK5,sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_697,c_172]) ).
cnf(c_768,negated_conjecture,
( barrel(sK5,sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1114]) ).
cnf(c_1115,negated_conjecture,
( down(sK5,sK6)
| down(sK5,sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_698,c_187]) ).
cnf(c_769,negated_conjecture,
( down(sK5,sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1115]) ).
cnf(c_1116,negated_conjecture,
( lonely(sK6)
| lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_715,c_82]) ).
cnf(c_770,negated_conjecture,
( lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1116]) ).
cnf(c_1117,negated_conjecture,
( chevy(sK7)
| chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_766,c_93]) ).
cnf(c_773,negated_conjecture,
( chevy(sK7)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1117]) ).
cnf(c_1118,negated_conjecture,
( chevy(sK7)
| chevy(sK7)
| ~ car(sK3) ),
inference(resolve,[status(thm)],[c_773,c_95]) ).
cnf(c_776,negated_conjecture,
( chevy(sK7)
| ~ car(sK3) ),
inference(copy,[status(thm)],[c_1118]) ).
cnf(c_1119,negated_conjecture,
( chevy(sK7)
| chevy(sK7) ),
inference(resolve,[status(thm)],[c_776,c_96]) ).
cnf(c_779,negated_conjecture,
chevy(sK7),
inference(copy,[status(thm)],[c_1119]) ).
cnf(c_784,negated_conjecture,
( car(sK3)
| ~ lonely(sK6)
| ~ street(sK6)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_779,c_753]) ).
cnf(c_1120,negated_conjecture,
( lonely(sK6)
| lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_770,c_77]) ).
cnf(c_790,negated_conjecture,
( lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1120]) ).
cnf(c_1121,negated_conjecture,
( lonely(sK6)
| lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_790,c_79]) ).
cnf(c_793,negated_conjecture,
( lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1121]) ).
cnf(c_1122,negated_conjecture,
( way(sK6)
| way(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_716,c_67]) ).
cnf(c_794,negated_conjecture,
( way(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1122]) ).
cnf(c_1123,negated_conjecture,
( street(sK6)
| street(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_717,c_52]) ).
cnf(c_795,negated_conjecture,
( street(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1123]) ).
cnf(c_1124,negated_conjecture,
( event(sK5)
| event(sK5)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_741,c_37]) ).
cnf(c_796,negated_conjecture,
( event(sK5)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1124]) ).
cnf(c_1125,negated_conjecture,
( lonely(sK6)
| lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_793,c_78]) ).
cnf(c_799,negated_conjecture,
( lonely(sK6)
| ~ car(sK3)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1125]) ).
cnf(c_1126,negated_conjecture,
( lonely(sK6)
| lonely(sK6)
| ~ car(sK3) ),
inference(resolve,[status(thm)],[c_799,c_80]) ).
cnf(c_802,negated_conjecture,
( lonely(sK6)
| ~ car(sK3) ),
inference(copy,[status(thm)],[c_1126]) ).
cnf(c_1127,negated_conjecture,
( lonely(sK6)
| lonely(sK6) ),
inference(resolve,[status(thm)],[c_802,c_81]) ).
cnf(c_805,negated_conjecture,
lonely(sK6),
inference(copy,[status(thm)],[c_1127]) ).
cnf(c_809,negated_conjecture,
( car(sK3)
| ~ street(sK6)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_805,c_784]) ).
cnf(c_1128,negated_conjecture,
( city(sK0)
| city(sK0)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_742,c_22]) ).
cnf(c_820,negated_conjecture,
( city(sK0)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1128]) ).
cnf(c_1129,negated_conjecture,
( hollywood(sK0)
| hollywood(sK0)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_743,c_7]) ).
cnf(c_821,negated_conjecture,
( hollywood(sK0)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(copy,[status(thm)],[c_1129]) ).
cnf(c_1130,negated_conjecture,
( barrel(sK5,sK7)
| barrel(sK5,sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_768,c_167]) ).
cnf(c_823,negated_conjecture,
( barrel(sK5,sK7)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1130]) ).
cnf(c_1131,negated_conjecture,
( car(sK3)
| car(sK3)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_809,c_51]) ).
cnf(c_832,negated_conjecture,
( car(sK3)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(copy,[status(thm)],[c_1131]) ).
cnf(c_1132,negated_conjecture,
( car(sK3)
| car(sK3)
| ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_832,c_6]) ).
cnf(c_835,negated_conjecture,
( car(sK3)
| ~ event(sK5)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1132]) ).
cnf(c_1133,negated_conjecture,
( car(sK3)
| car(sK3)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_835,c_36]) ).
cnf(c_838,negated_conjecture,
( car(sK3)
| ~ city(sK0) ),
inference(copy,[status(thm)],[c_1133]) ).
cnf(c_1134,negated_conjecture,
( down(sK5,sK6)
| down(sK5,sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_769,c_182]) ).
cnf(c_839,negated_conjecture,
( down(sK5,sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1134]) ).
cnf(c_1135,negated_conjecture,
( way(sK6)
| way(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_794,c_62]) ).
cnf(c_840,negated_conjecture,
( way(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1135]) ).
cnf(c_1136,negated_conjecture,
( street(sK6)
| street(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_795,c_47]) ).
cnf(c_841,negated_conjecture,
( street(sK6)
| ~ car(sK3)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1136]) ).
cnf(c_1137,negated_conjecture,
( car(sK3)
| car(sK3) ),
inference(resolve,[status(thm)],[c_838,c_21]) ).
cnf(c_844,negated_conjecture,
car(sK3),
inference(copy,[status(thm)],[c_1137]) ).
cnf(c_845,negated_conjecture,
( street(sK6)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_844,c_841]) ).
cnf(c_846,negated_conjecture,
( way(sK6)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_844,c_840]) ).
cnf(c_847,negated_conjecture,
( down(sK5,sK6)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_844,c_839]) ).
cnf(c_848,negated_conjecture,
( barrel(sK5,sK7)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_844,c_823]) ).
cnf(c_849,negated_conjecture,
( hollywood(sK0)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_844,c_821]) ).
cnf(c_850,negated_conjecture,
( city(sK0)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_844,c_820]) ).
cnf(c_851,negated_conjecture,
( event(sK5)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1)
| ~ hollywood(sK1) ),
inference(resolve,[status(thm)],[c_844,c_796]) ).
cnf(c_1138,negated_conjecture,
( street(sK6)
| street(sK6)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_845,c_49]) ).
cnf(c_855,negated_conjecture,
( street(sK6)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1138]) ).
cnf(c_1139,negated_conjecture,
( street(sK6)
| street(sK6)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_855,c_48]) ).
cnf(c_859,negated_conjecture,
( street(sK6)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1139]) ).
cnf(c_1140,negated_conjecture,
( street(sK6)
| street(sK6) ),
inference(resolve,[status(thm)],[c_859,c_50]) ).
cnf(c_863,negated_conjecture,
street(sK6),
inference(copy,[status(thm)],[c_1140]) ).
cnf(c_1141,negated_conjecture,
( way(sK6)
| way(sK6)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_846,c_64]) ).
cnf(c_872,negated_conjecture,
( way(sK6)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1141]) ).
cnf(c_1142,negated_conjecture,
( down(sK5,sK6)
| down(sK5,sK6)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_847,c_184]) ).
cnf(c_873,negated_conjecture,
( down(sK5,sK6)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1142]) ).
cnf(c_1143,negated_conjecture,
( barrel(sK5,sK7)
| barrel(sK5,sK7)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_848,c_169]) ).
cnf(c_874,negated_conjecture,
( barrel(sK5,sK7)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1143]) ).
cnf(c_1144,negated_conjecture,
( way(sK6)
| way(sK6)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_872,c_63]) ).
cnf(c_877,negated_conjecture,
( way(sK6)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1144]) ).
cnf(c_1145,negated_conjecture,
( way(sK6)
| way(sK6) ),
inference(resolve,[status(thm)],[c_877,c_65]) ).
cnf(c_880,negated_conjecture,
way(sK6),
inference(copy,[status(thm)],[c_1145]) ).
cnf(c_1146,negated_conjecture,
( down(sK5,sK6)
| down(sK5,sK6)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_873,c_183]) ).
cnf(c_881,negated_conjecture,
( down(sK5,sK6)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1146]) ).
cnf(c_1147,negated_conjecture,
( down(sK5,sK6)
| down(sK5,sK6) ),
inference(resolve,[status(thm)],[c_881,c_185]) ).
cnf(c_882,negated_conjecture,
down(sK5,sK6),
inference(copy,[status(thm)],[c_1147]) ).
cnf(c_1148,plain,
( ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ street(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_882,c_291]) ).
cnf(c_1149,plain,
( ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ way(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_863,c_1148]) ).
cnf(c_1150,plain,
( ~ barrel(sK5,A)
| ~ lonely(sK6)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_880,c_1149]) ).
cnf(c_883,plain,
( ~ barrel(sK5,A)
| ~ old(A)
| ~ dirty(A)
| ~ white(A)
| ~ car(A)
| ~ chevy(A)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_805,c_1150]) ).
cnf(c_1151,negated_conjecture,
( hollywood(sK0)
| hollywood(sK0)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_849,c_2]) ).
cnf(c_886,negated_conjecture,
( hollywood(sK0)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1151]) ).
cnf(c_1152,negated_conjecture,
( city(sK0)
| city(sK0)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_850,c_17]) ).
cnf(c_888,negated_conjecture,
( city(sK0)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1152]) ).
cnf(c_1153,negated_conjecture,
( event(sK5)
| event(sK5)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_851,c_32]) ).
cnf(c_889,negated_conjecture,
( event(sK5)
| ~ chevy(sK3)
| ~ event(sK2)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1153]) ).
cnf(c_1154,negated_conjecture,
( barrel(sK5,sK7)
| barrel(sK5,sK7)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_874,c_168]) ).
cnf(c_890,negated_conjecture,
( barrel(sK5,sK7)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1154]) ).
cnf(c_1155,negated_conjecture,
( barrel(sK5,sK7)
| barrel(sK5,sK7) ),
inference(resolve,[status(thm)],[c_890,c_170]) ).
cnf(c_891,negated_conjecture,
barrel(sK5,sK7),
inference(copy,[status(thm)],[c_1155]) ).
cnf(c_1156,plain,
( ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ chevy(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_891,c_883]) ).
cnf(c_1157,plain,
( ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_779,c_1156]) ).
cnf(c_1158,plain,
( ~ old(sK7)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_429,c_1157]) ).
cnf(c_1159,plain,
( ~ old(sK7)
| ~ dirty(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_490,c_1158]) ).
cnf(c_1160,plain,
( ~ old(sK7)
| ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_749,c_1159]) ).
cnf(c_892,plain,
( ~ event(sK5)
| ~ city(sK0)
| ~ hollywood(sK0) ),
inference(resolve,[status(thm)],[c_720,c_1160]) ).
cnf(c_1161,negated_conjecture,
( hollywood(sK0)
| hollywood(sK0)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_886,c_4]) ).
cnf(c_895,negated_conjecture,
( hollywood(sK0)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1161]) ).
cnf(c_1162,negated_conjecture,
( hollywood(sK0)
| hollywood(sK0)
| ~ chevy(sK3) ),
inference(resolve,[status(thm)],[c_895,c_3]) ).
cnf(c_904,negated_conjecture,
( hollywood(sK0)
| ~ chevy(sK3) ),
inference(copy,[status(thm)],[c_1162]) ).
cnf(c_1163,negated_conjecture,
( city(sK0)
| city(sK0)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_888,c_19]) ).
cnf(c_906,negated_conjecture,
( city(sK0)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1163]) ).
cnf(c_1164,negated_conjecture,
( event(sK5)
| event(sK5)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_889,c_34]) ).
cnf(c_907,negated_conjecture,
( event(sK5)
| ~ chevy(sK3)
| ~ city(sK1) ),
inference(copy,[status(thm)],[c_1164]) ).
cnf(c_1165,negated_conjecture,
( hollywood(sK0)
| hollywood(sK0) ),
inference(resolve,[status(thm)],[c_904,c_5]) ).
cnf(c_911,negated_conjecture,
hollywood(sK0),
inference(copy,[status(thm)],[c_1165]) ).
cnf(c_912,plain,
( ~ event(sK5)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_911,c_892]) ).
cnf(c_916,plain,
( chevy(sK3)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_912,c_35]) ).
cnf(c_918,plain,
( city(sK1)
| ~ city(sK0) ),
inference(resolve,[status(thm)],[c_912,c_33]) ).
cnf(c_1166,negated_conjecture,
( chevy(sK3)
| chevy(sK3) ),
inference(resolve,[status(thm)],[c_916,c_20]) ).
cnf(c_921,negated_conjecture,
chevy(sK3),
inference(copy,[status(thm)],[c_1166]) ).
cnf(c_922,negated_conjecture,
( event(sK5)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_921,c_907]) ).
cnf(c_923,negated_conjecture,
( city(sK0)
| ~ city(sK1) ),
inference(resolve,[status(thm)],[c_921,c_906]) ).
cnf(c_1167,negated_conjecture,
( city(sK1)
| city(sK1) ),
inference(resolve,[status(thm)],[c_918,c_18]) ).
cnf(c_928,negated_conjecture,
city(sK1),
inference(copy,[status(thm)],[c_1167]) ).
cnf(c_930,negated_conjecture,
city(sK0),
inference(resolve,[status(thm)],[c_928,c_923]) ).
cnf(c_931,negated_conjecture,
event(sK5),
inference(resolve,[status(thm)],[c_928,c_922]) ).
cnf(c_1168,plain,
~ event(sK5),
inference(resolve,[status(thm)],[c_930,c_912]) ).
cnf(c_933,plain,
$false,
inference(resolve,[status(thm)],[c_931,c_1168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP001+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 00:24:12 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 2625493 was started by sandbox2 on n015,
% 0.08/0.35 % Sat Sep 26 00:24:12 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.39
% 0.12/0.39 % From the command line: assign(max_seconds, 300).
% 0.54/0.48
% 0.54/0.48 % SZS status Theorem for theBenchmark
% 0.54/0.48
% 0.54/0.48 % Proof 1 at 0.05 (+ 0.02) seconds.
% 0.54/0.48 % Length of proof is 467.
% 0.54/0.48 % Level of proof is 71.
% 0.54/0.48 % Maximum clause weight is 67.000.
% 0.54/0.48 % Given clauses 441.
% 0.54/0.48
% 0.54/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------