%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP163+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 : Tue Sep 29 12:07:42 PM UTC 2026
% Result : CounterSatisfiable 9.06s 2.32s
% Output : Saturation 10.70s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u203,negated_conjecture,
~ sP12 ).
cnf(u165,negated_conjecture,
sP10(sK47) ).
cnf(u169,negated_conjecture,
actual_world(sK47) ).
cnf(u173,negated_conjecture,
( ~ actual_world(X0)
| member(X0,sK46(X0,X8),X8)
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| member(X0,sK45(X0,X7),X7)
| ~ group(X0,X7)
| ~ two(X0,X7)
| member(X0,sK44(X0,X2,X7),X7)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u177,negated_conjecture,
( ~ cheap(X0,sK46(X0,X8))
| ~ actual_world(X0)
| ~ black(X0,sK46(X0,X8))
| ~ coat(X0,sK46(X0,X8))
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| member(X0,sK45(X0,X7),X7)
| ~ group(X0,X7)
| ~ two(X0,X7)
| member(X0,sK44(X0,X2,X7),X7)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u181,negated_conjecture,
( ~ young(X0,sK45(X0,X7))
| member(X0,sK46(X0,X8),X8)
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| ~ actual_world(X0)
| ~ fellow(X0,sK45(X0,X7))
| ~ group(X0,X7)
| ~ two(X0,X7)
| member(X0,sK44(X0,X2,X7),X7)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u185,negated_conjecture,
( ~ cheap(X0,sK46(X0,X8))
| ~ actual_world(X0)
| ~ black(X0,sK46(X0,X8))
| ~ coat(X0,sK46(X0,X8))
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| ~ young(X0,sK45(X0,X7))
| ~ fellow(X0,sK45(X0,X7))
| ~ group(X0,X7)
| ~ two(X0,X7)
| member(X0,sK44(X0,X2,X7),X7)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u189,negated_conjecture,
( ~ state(X0,X10)
| member(X0,sK46(X0,X8),X8)
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| member(X0,sK45(X0,X7),X7)
| ~ group(X0,X7)
| ~ two(X0,X7)
| ~ in(X0,X11,X2)
| ~ be(X0,X10,sK44(X0,X2,X7),X11)
| ~ actual_world(X0)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u193,negated_conjecture,
( ~ cheap(X0,sK46(X0,X8))
| ~ actual_world(X0)
| ~ black(X0,sK46(X0,X8))
| ~ coat(X0,sK46(X0,X8))
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| member(X0,sK45(X0,X7),X7)
| ~ group(X0,X7)
| ~ two(X0,X7)
| ~ in(X0,X11,X2)
| ~ be(X0,X10,sK44(X0,X2,X7),X11)
| ~ state(X0,X10)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u197,negated_conjecture,
( ~ young(X0,sK45(X0,X7))
| member(X0,sK46(X0,X8),X8)
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| ~ actual_world(X0)
| ~ fellow(X0,sK45(X0,X7))
| ~ group(X0,X7)
| ~ two(X0,X7)
| ~ in(X0,X11,X2)
| ~ be(X0,X10,sK44(X0,X2,X7),X11)
| ~ state(X0,X10)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u201,negated_conjecture,
( ~ cheap(X0,sK46(X0,X8))
| ~ actual_world(X0)
| ~ black(X0,sK46(X0,X8))
| ~ coat(X0,sK46(X0,X8))
| ~ group(X0,X8)
| sP11(X0,X1,X8)
| ~ young(X0,sK45(X0,X7))
| ~ fellow(X0,sK45(X0,X7))
| ~ group(X0,X7)
| ~ two(X0,X7)
| ~ in(X0,X11,X2)
| ~ be(X0,X10,sK44(X0,X2,X7),X11)
| ~ state(X0,X10)
| ~ in(X0,X6,X2)
| ~ down(X0,X6,X5)
| ~ barrel(X0,X6)
| ~ present(X0,X6)
| ~ agent(X0,X6,X4)
| ~ event(X0,X6)
| ~ lonely(X0,X5)
| ~ street(X0,X5)
| ~ old(X0,X4)
| ~ dirty(X0,X4)
| ~ white(X0,X4)
| ~ chevy(X0,X4)
| ~ placename(X0,X3)
| ~ hollywood_placename(X0,X3)
| ~ city(X0,X2)
| ~ of(X0,X3,X2)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u206,axiom,
sP4(sK16) ).
cnf(u1935,axiom,
~ actual_world(sK16) ).
cnf(u214,axiom,
( ~ actual_world(X0)
| member(X0,sK15(X0,X9),X9)
| ~ group(X0,X9)
| sP5(X0,X1,X9)
| member(X0,sK14(X0,X8),X8)
| ~ group(X0,X8)
| ~ two(X0,X8)
| member(X0,sK13(X0,X2,X8),X8)
| ~ in(X0,X7,X3)
| ~ down(X0,X7,X6)
| ~ barrel(X0,X7)
| ~ present(X0,X7)
| ~ agent(X0,X7,X5)
| ~ event(X0,X7)
| ~ lonely(X0,X6)
| ~ street(X0,X6)
| ~ old(X0,X5)
| ~ dirty(X0,X5)
| ~ white(X0,X5)
| ~ chevy(X0,X5)
| ~ placename(X0,X4)
| ~ hollywood_placename(X0,X4)
| ~ city(X0,X3)
| ~ of(X0,X4,X3)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u218,axiom,
( ~ cheap(X0,sK15(X0,X9))
| ~ actual_world(X0)
| ~ black(X0,sK15(X0,X9))
| ~ coat(X0,sK15(X0,X9))
| ~ group(X0,X9)
| sP5(X0,X1,X9)
| member(X0,sK14(X0,X8),X8)
| ~ group(X0,X8)
| ~ two(X0,X8)
| member(X0,sK13(X0,X2,X8),X8)
| ~ in(X0,X7,X3)
| ~ down(X0,X7,X6)
| ~ barrel(X0,X7)
| ~ present(X0,X7)
| ~ agent(X0,X7,X5)
| ~ event(X0,X7)
| ~ lonely(X0,X6)
| ~ street(X0,X6)
| ~ old(X0,X5)
| ~ dirty(X0,X5)
| ~ white(X0,X5)
| ~ chevy(X0,X5)
| ~ placename(X0,X4)
| ~ hollywood_placename(X0,X4)
| ~ city(X0,X3)
| ~ of(X0,X4,X3)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u222,axiom,
( ~ young(X0,sK14(X0,X8))
| member(X0,sK15(X0,X9),X9)
| ~ group(X0,X9)
| sP5(X0,X1,X9)
| ~ actual_world(X0)
| ~ fellow(X0,sK14(X0,X8))
| ~ group(X0,X8)
| ~ two(X0,X8)
| member(X0,sK13(X0,X2,X8),X8)
| ~ in(X0,X7,X3)
| ~ down(X0,X7,X6)
| ~ barrel(X0,X7)
| ~ present(X0,X7)
| ~ agent(X0,X7,X5)
| ~ event(X0,X7)
| ~ lonely(X0,X6)
| ~ street(X0,X6)
| ~ old(X0,X5)
| ~ dirty(X0,X5)
| ~ white(X0,X5)
| ~ chevy(X0,X5)
| ~ placename(X0,X4)
| ~ hollywood_placename(X0,X4)
| ~ city(X0,X3)
| ~ of(X0,X4,X3)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u226,axiom,
( ~ cheap(X0,sK15(X0,X9))
| ~ actual_world(X0)
| ~ black(X0,sK15(X0,X9))
| ~ coat(X0,sK15(X0,X9))
| ~ group(X0,X9)
| sP5(X0,X1,X9)
| ~ young(X0,sK14(X0,X8))
| ~ fellow(X0,sK14(X0,X8))
| ~ group(X0,X8)
| ~ two(X0,X8)
| member(X0,sK13(X0,X2,X8),X8)
| ~ in(X0,X7,X3)
| ~ down(X0,X7,X6)
| ~ barrel(X0,X7)
| ~ present(X0,X7)
| ~ agent(X0,X7,X5)
| ~ event(X0,X7)
| ~ lonely(X0,X6)
| ~ street(X0,X6)
| ~ old(X0,X5)
| ~ dirty(X0,X5)
| ~ white(X0,X5)
| ~ chevy(X0,X5)
| ~ placename(X0,X4)
| ~ hollywood_placename(X0,X4)
| ~ city(X0,X3)
| ~ of(X0,X4,X3)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u230,axiom,
( ~ be(X0,X11,sK13(X0,X2,X8),X12)
| member(X0,sK15(X0,X9),X9)
| ~ group(X0,X9)
| sP5(X0,X1,X9)
| member(X0,sK14(X0,X8),X8)
| ~ group(X0,X8)
| ~ two(X0,X8)
| ~ in(X0,X12,X2)
| ~ actual_world(X0)
| ~ state(X0,X11)
| ~ in(X0,X7,X3)
| ~ down(X0,X7,X6)
| ~ barrel(X0,X7)
| ~ present(X0,X7)
| ~ agent(X0,X7,X5)
| ~ event(X0,X7)
| ~ lonely(X0,X6)
| ~ street(X0,X6)
| ~ old(X0,X5)
| ~ dirty(X0,X5)
| ~ white(X0,X5)
| ~ chevy(X0,X5)
| ~ placename(X0,X4)
| ~ hollywood_placename(X0,X4)
| ~ city(X0,X3)
| ~ of(X0,X4,X3)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u234,axiom,
( ~ cheap(X0,sK15(X0,X9))
| ~ actual_world(X0)
| ~ black(X0,sK15(X0,X9))
| ~ coat(X0,sK15(X0,X9))
| ~ group(X0,X9)
| sP5(X0,X1,X9)
| member(X0,sK14(X0,X8),X8)
| ~ group(X0,X8)
| ~ two(X0,X8)
| ~ in(X0,X12,X2)
| ~ be(X0,X11,sK13(X0,X2,X8),X12)
| ~ state(X0,X11)
| ~ in(X0,X7,X3)
| ~ down(X0,X7,X6)
| ~ barrel(X0,X7)
| ~ present(X0,X7)
| ~ agent(X0,X7,X5)
| ~ event(X0,X7)
| ~ lonely(X0,X6)
| ~ street(X0,X6)
| ~ old(X0,X5)
| ~ dirty(X0,X5)
| ~ white(X0,X5)
| ~ chevy(X0,X5)
| ~ placename(X0,X4)
| ~ hollywood_placename(X0,X4)
| ~ city(X0,X3)
| ~ of(X0,X4,X3)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u238,axiom,
( ~ young(X0,sK14(X0,X8))
| member(X0,sK15(X0,X9),X9)
| ~ group(X0,X9)
| sP5(X0,X1,X9)
| ~ actual_world(X0)
| ~ fellow(X0,sK14(X0,X8))
| ~ group(X0,X8)
| ~ two(X0,X8)
| ~ in(X0,X12,X2)
| ~ be(X0,X11,sK13(X0,X2,X8),X12)
| ~ state(X0,X11)
| ~ in(X0,X7,X3)
| ~ down(X0,X7,X6)
| ~ barrel(X0,X7)
| ~ present(X0,X7)
| ~ agent(X0,X7,X5)
| ~ event(X0,X7)
| ~ lonely(X0,X6)
| ~ street(X0,X6)
| ~ old(X0,X5)
| ~ dirty(X0,X5)
| ~ white(X0,X5)
| ~ chevy(X0,X5)
| ~ placename(X0,X4)
| ~ hollywood_placename(X0,X4)
| ~ city(X0,X3)
| ~ of(X0,X4,X3)
| ~ frontseat(X0,X2)
| ~ group(X0,X1) ) ).
cnf(u265,negated_conjecture,
( ~ two(sK47,X2)
| ~ frontseat(sK47,X3)
| ~ city(sK47,X3)
| ~ placename(sK47,X7)
| ~ of(sK47,X7,X3)
| ~ hollywood_placename(sK47,X7)
| ~ chevy(sK47,X6)
| ~ white(sK47,X6)
| ~ dirty(sK47,X6)
| ~ old(sK47,X6)
| ~ street(sK47,X5)
| ~ lonely(sK47,X5)
| ~ event(sK47,X4)
| ~ agent(sK47,X4,X6)
| ~ present(sK47,X4)
| ~ barrel(sK47,X4)
| ~ down(sK47,X4,X5)
| ~ in(sK47,X4,X3)
| member(sK47,sK44(sK47,X3,X2),X2)
| member(sK47,sK45(sK47,X2),X2)
| ~ group(sK47,X2) ) ).
cnf(u268,negated_conjecture,
( ~ group(sK47,X0)
| ~ group(sK47,X1)
| sP11(sK47,X1,X0)
| member(sK47,sK46(sK47,X0),X0) ) ).
cnf(u276,negated_conjecture,
member(sK47,sK45(sK47,sK26(sK47)),sK26(sK47)) ).
cnf(u279,negated_conjecture,
( ~ barrel(sK47,X4)
| member(sK47,sK44(sK47,X0,sK26(sK47)),sK26(sK47))
| ~ chevy(sK47,X2)
| ~ in(sK47,X4,X0)
| ~ down(sK47,X4,X3)
| ~ frontseat(sK47,X0)
| ~ present(sK47,X4)
| ~ event(sK47,X4)
| ~ agent(sK47,X4,X2)
| ~ street(sK47,X3)
| ~ lonely(sK47,X3)
| ~ old(sK47,X2)
| ~ dirty(sK47,X2)
| ~ white(sK47,X2)
| ~ hollywood_placename(sK47,X1)
| ~ placename(sK47,X1)
| ~ of(sK47,X1,X0)
| ~ city(sK47,X0) ) ).
cnf(u294,negated_conjecture,
member(sK47,sK46(sK47,sK19(sK47)),sK19(sK47)) ).
cnf(u301,negated_conjecture,
member(sK47,sK46(sK47,sK27(sK47)),sK27(sK47)) ).
cnf(u308,negated_conjecture,
member(sK47,sK46(sK47,sK26(sK47)),sK26(sK47)) ).
cnf(u337,negated_conjecture,
( ~ in(sK47,sK25(sK47),X0)
| ~ city(sK47,X0)
| ~ hollywood_placename(sK47,X3)
| ~ of(sK47,X3,X0)
| ~ placename(sK47,X3)
| ~ frontseat(sK47,X0)
| member(sK47,sK44(sK47,X0,sK26(sK47)),sK26(sK47)) ) ).
cnf(u404,negated_conjecture,
( ~ young(sK47,sK45(sK47,X1))
| ~ frontseat(sK47,X3)
| ~ city(sK47,X3)
| ~ placename(sK47,X8)
| ~ of(sK47,X8,X3)
| ~ hollywood_placename(sK47,X8)
| ~ chevy(sK47,X7)
| ~ white(sK47,X7)
| ~ dirty(sK47,X7)
| ~ old(sK47,X7)
| ~ street(sK47,X6)
| ~ lonely(sK47,X6)
| ~ event(sK47,X5)
| ~ agent(sK47,X5,X7)
| ~ present(sK47,X5)
| ~ barrel(sK47,X5)
| ~ down(sK47,X5,X6)
| ~ in(sK47,X5,X3)
| ~ state(sK47,X4)
| ~ be(sK47,X4,sK44(sK47,X3,X1),X2)
| ~ in(sK47,X2,X3)
| ~ two(sK47,X1)
| ~ group(sK47,X1)
| ~ fellow(sK47,sK45(sK47,X1)) ) ).
cnf(u411,negated_conjecture,
( ~ be(sK47,X4,sK44(sK47,X3,X1),X2)
| ~ frontseat(sK47,X3)
| ~ city(sK47,X3)
| ~ placename(sK47,X8)
| ~ of(sK47,X8,X3)
| ~ hollywood_placename(sK47,X8)
| ~ chevy(sK47,X7)
| ~ white(sK47,X7)
| ~ dirty(sK47,X7)
| ~ old(sK47,X7)
| ~ street(sK47,X6)
| ~ lonely(sK47,X6)
| ~ event(sK47,X5)
| ~ agent(sK47,X5,X7)
| ~ present(sK47,X5)
| ~ barrel(sK47,X5)
| ~ down(sK47,X5,X6)
| ~ in(sK47,X5,X3)
| ~ state(sK47,X4)
| member(sK47,sK45(sK47,X1),X1)
| ~ in(sK47,X2,X3)
| ~ two(sK47,X1)
| ~ group(sK47,X1) ) ).
cnf(u416,negated_conjecture,
( ~ young(sK47,sK45(sK47,X1))
| ~ frontseat(sK47,X2)
| ~ city(sK47,X2)
| ~ placename(sK47,X6)
| ~ of(sK47,X6,X2)
| ~ hollywood_placename(sK47,X6)
| ~ chevy(sK47,X5)
| ~ white(sK47,X5)
| ~ dirty(sK47,X5)
| ~ old(sK47,X5)
| ~ street(sK47,X4)
| ~ lonely(sK47,X4)
| ~ event(sK47,X3)
| ~ agent(sK47,X3,X5)
| ~ present(sK47,X3)
| ~ barrel(sK47,X3)
| ~ down(sK47,X3,X4)
| ~ in(sK47,X3,X2)
| member(sK47,sK44(sK47,X2,X1),X1)
| ~ two(sK47,X1)
| ~ group(sK47,X1)
| ~ fellow(sK47,sK45(sK47,X1)) ) ).
cnf(u536,negated_conjecture,
( ~ group(sK16,X0)
| ~ group(sK16,X1)
| sP11(sK16,X1,X0)
| member(sK16,sK46(sK16,X0),X0) ) ).
cnf(u585,negated_conjecture,
~ sP10(sK16) ).
cnf(u612,negated_conjecture,
( sP11(sK16,X0,sK39(sK16))
| ~ group(sK16,X0) ) ).
cnf(u616,negated_conjecture,
member(sK16,sK46(sK16,sK40(sK16)),sK40(sK16)) ).
cnf(u623,negated_conjecture,
member(sK16,sK46(sK16,sK33(sK16)),sK33(sK16)) ).
cnf(u654,negated_conjecture,
( ~ state(sK16,X4)
| ~ frontseat(sK16,X3)
| ~ city(sK16,X3)
| ~ placename(sK16,X8)
| ~ of(sK16,X8,X3)
| ~ hollywood_placename(sK16,X8)
| ~ chevy(sK16,X7)
| ~ white(sK16,X7)
| ~ dirty(sK16,X7)
| ~ old(sK16,X7)
| ~ street(sK16,X6)
| ~ lonely(sK16,X6)
| ~ event(sK16,X5)
| ~ agent(sK16,X5,X7)
| ~ present(sK16,X5)
| ~ barrel(sK16,X5)
| ~ down(sK16,X5,X6)
| ~ in(sK16,X5,X3)
| ~ in(sK16,X2,X3)
| ~ be(sK16,X4,sK44(sK16,X3,sK39(sK16)),X2) ) ).
cnf(u754,axiom,
( ~ group(sK16,X0)
| ~ group(sK16,X1)
| sP5(sK16,X1,X0)
| member(sK16,sK15(sK16,X0),X0) ) ).
cnf(u760,axiom,
( ~ two(sK16,X2)
| ~ frontseat(sK16,X3)
| member(sK16,sK13(sK16,X3,X2),X2)
| member(sK16,sK14(sK16,X2),X2)
| ~ group(sK16,X2) ) ).
cnf(u767,negated_conjecture,
( ~ two(sK47,X2)
| ~ frontseat(sK47,X3)
| member(sK47,sK13(sK47,X3,X2),X2)
| member(sK47,sK14(sK47,X2),X2)
| ~ group(sK47,X2) ) ).
cnf(u770,negated_conjecture,
( ~ group(sK47,X0)
| ~ group(sK47,X1)
| sP5(sK47,X1,X0)
| member(sK47,sK15(sK47,X0),X0) ) ).
cnf(u780,negated_conjecture,
member(sK47,sK15(sK47,sK19(sK47)),sK19(sK47)) ).
cnf(u787,negated_conjecture,
member(sK47,sK15(sK47,sK27(sK47)),sK27(sK47)) ).
cnf(u797,negated_conjecture,
( sP5(sK47,X0,sK26(sK47))
| ~ group(sK47,X0) ) ).
cnf(u884,axiom,
( ~ frontseat(sK16,X0)
| member(sK16,sK13(sK16,X0,sK39(sK16)),sK39(sK16)) ) ).
cnf(u918,axiom,
( sP5(sK16,X0,sK39(sK16))
| ~ group(sK16,X0) ) ).
cnf(u922,axiom,
member(sK16,sK15(sK16,sK40(sK16)),sK40(sK16)) ).
cnf(u932,axiom,
( sP5(sK16,X0,sK33(sK16))
| ~ group(sK16,X0) ) ).
cnf(u971,axiom,
( ~ fellow(sK16,sK14(sK16,X1))
| ~ frontseat(sK16,X3)
| ~ state(sK16,X4)
| ~ be(sK16,X4,sK13(sK16,X3,X1),X2)
| ~ in(sK16,X2,X3)
| ~ two(sK16,X1)
| ~ group(sK16,X1)
| ~ young(sK16,sK14(sK16,X1)) ) ).
cnf(u979,axiom,
( ~ fellow(sK16,sK14(sK16,X1))
| ~ frontseat(sK16,X2)
| member(sK16,sK13(sK16,X2,X1),X1)
| ~ two(sK16,X1)
| ~ group(sK16,X1)
| ~ young(sK16,sK14(sK16,X1)) ) ).
cnf(u1174,negated_conjecture,
( ~ be(sK47,X4,sK13(sK47,X3,X1),X2)
| ~ frontseat(sK47,X3)
| ~ state(sK47,X4)
| member(sK47,sK14(sK47,X1),X1)
| ~ in(sK47,X2,X3)
| ~ two(sK47,X1)
| ~ group(sK47,X1) ) ).
cnf(u1178,negated_conjecture,
( ~ young(sK47,sK14(sK47,X1))
| ~ frontseat(sK47,X2)
| member(sK47,sK13(sK47,X2,X1),X1)
| ~ two(sK47,X1)
| ~ group(sK47,X1)
| ~ fellow(sK47,sK14(sK47,X1)) ) ).
cnf(u1184,negated_conjecture,
member(sK47,sK14(sK47,sK26(sK47)),sK26(sK47)) ).
cnf(u1187,negated_conjecture,
( ~ frontseat(sK47,X0)
| member(sK47,sK13(sK47,X0,sK26(sK47)),sK26(sK47)) ) ).
cnf(u1310,axiom,
( ~ wear(sK16,sK43(sK16,sK31(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ member(sK16,X0,sK33(sK16))
| ~ nonreflexive(sK16,sK43(sK16,sK31(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ present(sK16,sK43(sK16,sK31(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ event(sK16,sK43(sK16,sK31(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ agent(sK16,sK43(sK16,sK31(sK16,sK40(sK16),sK40(sK16)),X0),sK32(sK16,sK40(sK16),sK40(sK16))) ) ).
cnf(u1319,axiom,
( ~ wear(sK16,sK43(sK16,sK31(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ member(sK16,X0,sK33(sK16))
| ~ nonreflexive(sK16,sK43(sK16,sK31(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ present(sK16,sK43(sK16,sK31(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ event(sK16,sK43(sK16,sK31(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ agent(sK16,sK43(sK16,sK31(sK16,sK39(sK16),sK40(sK16)),X0),sK32(sK16,sK39(sK16),sK40(sK16))) ) ).
cnf(u1385,axiom,
~ member(sK16,sK31(sK16,sK40(sK16),sK40(sK16)),sK40(sK16)) ).
cnf(u1392,axiom,
~ member(sK16,sK31(sK16,sK39(sK16),sK40(sK16)),sK40(sK16)) ).
cnf(u1676,negated_conjecture,
( ~ wear(sK16,sK43(sK16,sK17(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ member(sK16,X0,sK33(sK16))
| ~ nonreflexive(sK16,sK43(sK16,sK17(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ present(sK16,sK43(sK16,sK17(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ event(sK16,sK43(sK16,sK17(sK16,sK40(sK16),sK40(sK16)),X0))
| ~ agent(sK16,sK43(sK16,sK17(sK16,sK40(sK16),sK40(sK16)),X0),sK18(sK16,sK40(sK16),sK40(sK16))) ) ).
cnf(u1689,negated_conjecture,
( ~ wear(sK16,sK43(sK16,sK17(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ member(sK16,X0,sK33(sK16))
| ~ nonreflexive(sK16,sK43(sK16,sK17(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ present(sK16,sK43(sK16,sK17(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ event(sK16,sK43(sK16,sK17(sK16,sK39(sK16),sK40(sK16)),X0))
| ~ agent(sK16,sK43(sK16,sK17(sK16,sK39(sK16),sK40(sK16)),X0),sK18(sK16,sK39(sK16),sK40(sK16))) ) ).
cnf(u1731,negated_conjecture,
~ member(sK16,sK17(sK16,sK40(sK16),sK40(sK16)),sK40(sK16)) ).
cnf(u1738,negated_conjecture,
~ member(sK16,sK17(sK16,sK39(sK16),sK40(sK16)),sK40(sK16)) ).
cnf(u1771,negated_conjecture,
( ~ young(sK16,sK45(sK16,X1))
| ~ frontseat(sK16,X3)
| ~ city(sK16,X3)
| ~ placename(sK16,X8)
| ~ of(sK16,X8,X3)
| ~ hollywood_placename(sK16,X8)
| ~ chevy(sK16,X7)
| ~ white(sK16,X7)
| ~ dirty(sK16,X7)
| ~ old(sK16,X7)
| ~ street(sK16,X6)
| ~ lonely(sK16,X6)
| ~ event(sK16,X5)
| ~ agent(sK16,X5,X7)
| ~ present(sK16,X5)
| ~ barrel(sK16,X5)
| ~ down(sK16,X5,X6)
| ~ in(sK16,X5,X3)
| ~ state(sK16,X4)
| ~ be(sK16,X4,sK44(sK16,X3,X1),X2)
| ~ in(sK16,X2,X3)
| ~ two(sK16,X1)
| ~ group(sK16,X1)
| ~ fellow(sK16,sK45(sK16,X1)) ) ).
cnf(u1775,negated_conjecture,
( ~ two(sK16,X1)
| ~ frontseat(sK16,X3)
| ~ city(sK16,X3)
| ~ placename(sK16,X8)
| ~ of(sK16,X8,X3)
| ~ hollywood_placename(sK16,X8)
| ~ chevy(sK16,X7)
| ~ white(sK16,X7)
| ~ dirty(sK16,X7)
| ~ old(sK16,X7)
| ~ street(sK16,X6)
| ~ lonely(sK16,X6)
| ~ event(sK16,X5)
| ~ agent(sK16,X5,X7)
| ~ present(sK16,X5)
| ~ barrel(sK16,X5)
| ~ down(sK16,X5,X6)
| ~ in(sK16,X5,X3)
| ~ state(sK16,X4)
| ~ be(sK16,X4,sK44(sK16,X3,X1),X2)
| ~ in(sK16,X2,X3)
| member(sK16,sK45(sK16,X1),X1)
| ~ group(sK16,X1) ) ).
cnf(u1779,negated_conjecture,
( ~ young(sK16,sK45(sK16,X1))
| ~ frontseat(sK16,X2)
| ~ city(sK16,X2)
| ~ placename(sK16,X6)
| ~ of(sK16,X6,X2)
| ~ hollywood_placename(sK16,X6)
| ~ chevy(sK16,X5)
| ~ white(sK16,X5)
| ~ dirty(sK16,X5)
| ~ old(sK16,X5)
| ~ street(sK16,X4)
| ~ lonely(sK16,X4)
| ~ event(sK16,X3)
| ~ agent(sK16,X3,X5)
| ~ present(sK16,X3)
| ~ barrel(sK16,X3)
| ~ down(sK16,X3,X4)
| ~ in(sK16,X3,X2)
| member(sK16,sK44(sK16,X2,X1),X1)
| ~ two(sK16,X1)
| ~ group(sK16,X1)
| ~ fellow(sK16,sK45(sK16,X1)) ) ).
cnf(u1812,negated_conjecture,
( ~ be(sK47,X5,sK44(sK47,X0,sK26(sK47)),X6)
| ~ in(sK47,X6,X0)
| ~ frontseat(sK47,X0)
| ~ state(sK47,X5)
| ~ chevy(sK47,X2)
| ~ in(sK47,X4,X0)
| ~ down(sK47,X4,X3)
| ~ barrel(sK47,X4)
| ~ present(sK47,X4)
| ~ event(sK47,X4)
| ~ agent(sK47,X4,X2)
| ~ street(sK47,X3)
| ~ lonely(sK47,X3)
| ~ old(sK47,X2)
| ~ dirty(sK47,X2)
| ~ white(sK47,X2)
| ~ hollywood_placename(sK47,X1)
| ~ placename(sK47,X1)
| ~ of(sK47,X1,X0)
| ~ city(sK47,X0) ) ).
cnf(u1889,negated_conjecture,
~ frontseat(sK47,sK21(sK47)) ).
cnf(u1909,negated_conjecture,
( ~ in(sK16,sK38(sK16),X0)
| ~ member(sK16,X5,sK39(sK16))
| ~ be(sK16,sK41(sK16,sK34(sK16),X5),sK44(sK16,X0,sK39(sK16)),X4)
| ~ in(sK16,X4,X0)
| ~ city(sK16,X0)
| ~ frontseat(sK16,X0)
| ~ hollywood_placename(sK16,X1)
| ~ placename(sK16,X1)
| ~ of(sK16,X1,X0) ) ).
cnf(u1916,negated_conjecture,
( ~ be(sK16,sK41(sK16,sK34(sK16),X0),sK44(sK16,sK34(sK16),sK39(sK16)),X1)
| ~ in(sK16,X1,sK34(sK16))
| ~ member(sK16,X0,sK39(sK16)) ) ).
cnf(u248,negated_conjecture,
barrel(sK47,sK25(sK47)) ).
cnf(u550,axiom,
event(sK16,sK38(sK16)) ).
cnf(u1294,negated_conjecture,
( agent(sK47,sK30(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u1567,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK18(sK16,sK33(sK16),sK39(sK16))),sK18(sK16,sK33(sK16),sK39(sK16)),sK29(sK16,X0,sK18(sK16,sK33(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK33(sK16)) ) ).
cnf(u556,axiom,
chevy(sK16,sK36(sK16)) ).
cnf(u260,negated_conjecture,
city(sK47,sK21(sK47)) ).
cnf(u1566,negated_conjecture,
( ~ sP6(sK16,X1,sK33(sK16))
| agent(sK16,sK30(sK16,sK18(sK16,sK33(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u805,negated_conjecture,
cheap(sK47,sK15(sK47,sK27(sK47))) ).
cnf(u1572,negated_conjecture,
cheap(sK16,sK18(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u803,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK15(sK47,sK19(sK47))),sK15(sK47,sK19(sK47)),sK29(sK47,X0,sK15(sK47,sK19(sK47))))
| ~ sP8(sK47,X0,sK19(sK47)) ) ).
cnf(u149,axiom,
( ~ sP0(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| event(X0,sK43(X0,X3,X4)) ) ).
cnf(u1570,negated_conjecture,
black(sK16,sK18(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u1587,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK18(sK16,sK39(sK16),sK39(sK16)))) ) ).
cnf(u1576,negated_conjecture,
( ~ sP6(sK16,X1,sK40(sK16))
| present(sK16,sK30(sK16,sK18(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u538,axiom,
sP1(sK16,sK40(sK16)) ).
cnf(u824,negated_conjecture,
young(sK47,sK32(sK47,sK26(sK47),sK26(sK47))) ).
cnf(u544,axiom,
sP2(sK16,sK34(sK16),sK39(sK16)) ).
cnf(u561,axiom,
frontseat(sK16,sK34(sK16)) ).
cnf(u1077,axiom,
( ~ sP8(sK16,X1,sK33(sK16))
| in(sK16,sK29(sK16,X1,sK31(sK16,X0,sK33(sK16))),X1)
| ~ group(sK16,X0) ) ).
cnf(u575,axiom,
( ~ member(sK16,X0,sK39(sK16))
| fellow(sK16,X0) ) ).
cnf(u946,axiom,
( ~ group(sK16,X0)
| member(sK16,sK32(sK16,X0,sK33(sK16)),X0) ) ).
cnf(u1058,axiom,
( patient(sK16,sK43(sK16,sK32(sK16,sK40(sK16),sK39(sK16)),X0),sK32(sK16,sK40(sK16),sK39(sK16)))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u373,negated_conjecture,
( ~ member(sK47,X0,sK26(sK47))
| fellow(sK47,X0) ) ).
cnf(u1081,axiom,
( be(sK16,sK28(sK16,X1,sK31(sK16,X0,sK33(sK16))),sK31(sK16,X0,sK33(sK16)),sK29(sK16,X1,sK31(sK16,X0,sK33(sK16))))
| ~ group(sK16,X0)
| ~ sP8(sK16,X1,sK33(sK16)) ) ).
cnf(u822,negated_conjecture,
member(sK47,sK32(sK47,sK26(sK47),sK26(sK47)),sK26(sK47)) ).
cnf(u828,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK32(sK47,sK26(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u78,axiom,
( ~ sP10(X0)
| barrel(X0,sK25(X0)) ) ).
cnf(u368,negated_conjecture,
( nonreflexive(sK47,sK30(sK47,X1,X0))
| ~ member(sK47,X1,sK27(sK47))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u1879,axiom,
( be(sK16,sK28(sK16,X0,sK15(sK16,sK40(sK16))),sK15(sK16,sK40(sK16)),sK29(sK16,X0,sK15(sK16,sK40(sK16))))
| ~ sP8(sK16,X0,sK40(sK16)) ) ).
cnf(u833,negated_conjecture,
coat(sK47,sK32(sK47,sK27(sK47),sK26(sK47))) ).
cnf(u76,axiom,
( ~ sP10(X0)
| in(X0,sK25(X0),sK21(X0)) ) ).
cnf(u1987,negated_conjecture,
( ~ sP8(sK47,X0,sK27(sK47))
| state(sK47,sK28(sK47,X0,sK15(sK47,sK27(sK47)))) ) ).
cnf(u1749,negated_conjecture,
( ~ sP6(sK16,X1,sK40(sK16))
| event(sK16,sK30(sK16,sK46(sK16,sK40(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1750,negated_conjecture,
( ~ sP6(sK16,X1,sK40(sK16))
| present(sK16,sK30(sK16,sK46(sK16,sK40(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1993,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK14(sK47,sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u91,axiom,
( ~ sP10(X0)
| of(X0,sK22(X0),sK21(X0)) ) ).
cnf(u346,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| event(sK47,sK30(sK47,sK46(sK47,sK19(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u66,axiom,
( ~ sP11(X0,X1,X2)
| member(X0,sK17(X0,X1,X2),X2) ) ).
cnf(u862,negated_conjecture,
young(sK47,sK31(sK47,sK26(sK47),sK26(sK47))) ).
cnf(u1477,negated_conjecture,
( ~ sP6(sK16,X1,sK33(sK16))
| agent(sK16,sK30(sK16,sK46(sK16,sK33(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u89,axiom,
( ~ sP10(X0)
| hollywood_placename(X0,sK22(X0)) ) ).
cnf(u868,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK31(sK47,sK26(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1134,axiom,
( be(sK16,sK28(sK16,X0,sK31(sK16,sK33(sK16),sK39(sK16))),sK31(sK16,sK33(sK16),sK39(sK16)),sK29(sK16,X0,sK31(sK16,sK33(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u1878,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| agent(sK16,sK30(sK16,sK15(sK16,sK40(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u873,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK31(sK47,sK27(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u116,axiom,
( ~ sP4(X0)
| two(X0,sK39(X0)) ) ).
cnf(u990,axiom,
( ~ sP8(sK16,X0,sK33(sK16))
| in(sK16,sK29(sK16,X0,sK32(sK16,sK33(sK16),sK33(sK16))),X0) ) ).
cnf(u95,axiom,
( ~ sP9(X0,X1)
| ~ member(X0,X2,X1)
| fellow(X0,X2) ) ).
cnf(u1132,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK31(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u363,negated_conjecture,
( agent(sK47,sK30(sK47,sK46(sK47,sK27(sK47)),X0),X0)
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u350,negated_conjecture,
( ~ sP8(sK47,X0,sK19(sK47))
| state(sK47,sK28(sK47,X0,sK46(sK47,sK19(sK47)))) ) ).
cnf(u106,axiom,
( ~ member(X0,X3,X2)
| ~ member(X0,X4,X1)
| agent(X0,sK30(X0,X3,X4),X4)
| ~ sP6(X0,X1,X2) ) ).
cnf(u1001,axiom,
( ~ sP8(sK16,X0,sK40(sK16))
| in(sK16,sK29(sK16,X0,sK32(sK16,sK40(sK16),sK33(sK16))),X0) ) ).
cnf(u1147,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK31(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u2012,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK13(sK47,sK20(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1517,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK45(sK47,sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1136,axiom,
fellow(sK16,sK31(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u1639,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK17(sK16,sK40(sK16),sK39(sK16))),sK17(sK16,sK40(sK16),sK39(sK16)),sK29(sK16,X0,sK17(sK16,sK40(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u2010,negated_conjecture,
young(sK47,sK13(sK47,sK20(sK47),sK26(sK47))) ).
cnf(u361,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK46(sK47,sK26(sK47))),sK46(sK47,sK26(sK47)),sK29(sK47,X0,sK46(sK47,sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u256,negated_conjecture,
white(sK47,sK23(sK47)) ).
cnf(u104,axiom,
( ~ member(X0,X3,X2)
| ~ member(X0,X4,X1)
| present(X0,sK30(X0,X3,X4))
| ~ sP6(X0,X1,X2) ) ).
cnf(u1753,negated_conjecture,
( ~ sP8(sK16,X0,sK40(sK16))
| state(sK16,sK28(sK16,X0,sK46(sK16,sK40(sK16)))) ) ).
cnf(u875,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK31(sK47,sK27(sK47),sK26(sK47))),sK31(sK47,sK27(sK47),sK26(sK47)),sK29(sK47,X0,sK31(sK47,sK27(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1794,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| be(sK16,sK28(sK16,X0,sK13(sK16,sK34(sK16),sK39(sK16))),sK13(sK16,sK34(sK16),sK39(sK16)),sK29(sK16,X0,sK13(sK16,sK34(sK16),sK39(sK16)))) ) ).
cnf(u984,axiom,
member(sK16,sK32(sK16,sK33(sK16),sK33(sK16)),sK33(sK16)) ).
cnf(u1642,negated_conjecture,
young(sK16,sK17(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u2016,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK13(sK47,sK20(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1005,axiom,
( be(sK16,sK28(sK16,X0,sK32(sK16,sK40(sK16),sK33(sK16))),sK32(sK16,sK40(sK16),sK33(sK16)),sK29(sK16,X0,sK32(sK16,sK40(sK16),sK33(sK16))))
| ~ sP8(sK16,X0,sK40(sK16)) ) ).
cnf(u1648,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK17(sK16,sK39(sK16),sK39(sK16)))) ) ).
cnf(u1003,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| present(sK16,sK30(sK16,sK32(sK16,sK40(sK16),sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1146,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK31(sK16,sK39(sK16),sK39(sK16))),X0) ) ).
cnf(u135,axiom,
( ~ sP4(X0)
| group(X0,sK33(X0)) ) ).
cnf(u540,axiom,
sP0(sK16,sK33(sK16),sK40(sK16)) ).
cnf(u937,axiom,
cheap(sK16,sK15(sK16,sK40(sK16))) ).
cnf(u1573,negated_conjecture,
( agent(sK16,sK43(sK16,sK18(sK16,sK40(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u133,axiom,
( ~ sP4(X0)
| of(X0,sK35(X0),sK34(X0)) ) ).
cnf(u1571,negated_conjecture,
coat(sK16,sK18(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u144,axiom,
( ~ sP0(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| wear(X0,sK43(X0,X3,X4)) ) ).
cnf(u802,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| agent(sK47,sK30(sK47,sK15(sK47,sK19(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1577,negated_conjecture,
( ~ sP6(sK16,X1,sK40(sK16))
| agent(sK16,sK30(sK16,sK18(sK16,sK40(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u545,axiom,
in(sK16,sK38(sK16),sK34(sK16)) ).
cnf(u829,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK32(sK47,sK26(sK47),sK26(sK47))),sK32(sK47,sK26(sK47),sK26(sK47)),sK29(sK47,X0,sK32(sK47,sK26(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1061,axiom,
cheap(sK16,sK32(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u559,axiom,
city(sK16,sK34(sK16)) ).
cnf(u148,axiom,
( ~ sP0(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| agent(X0,sK43(X0,X3,X4),X4) ) ).
cnf(u806,negated_conjecture,
black(sK47,sK15(sK47,sK27(sK47))) ).
cnf(u1189,negated_conjecture,
fellow(sK47,sK14(sK47,sK26(sK47))) ).
cnf(u562,axiom,
group(sK16,sK33(sK16)) ).
cnf(u1078,axiom,
( ~ sP6(sK16,X2,sK33(sK16))
| ~ member(sK16,X1,X2)
| event(sK16,sK30(sK16,sK31(sK16,X0,sK33(sK16)),X1))
| ~ group(sK16,X0) ) ).
cnf(u568,axiom,
( wear(sK16,sK43(sK16,X1,X0))
| ~ member(sK16,X1,sK40(sK16))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1071,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK32(sK16,sK39(sK16),sK39(sK16))),X0) ) ).
cnf(u831,negated_conjecture,
cheap(sK47,sK32(sK47,sK27(sK47),sK26(sK47))) ).
cnf(u1082,axiom,
( ~ sP8(sK16,X1,sK33(sK16))
| state(sK16,sK28(sK16,X1,sK31(sK16,X0,sK33(sK16))))
| ~ group(sK16,X0) ) ).
cnf(u945,axiom,
( member(sK16,sK31(sK16,X0,sK33(sK16)),sK33(sK16))
| ~ group(sK16,X0) ) ).
cnf(u1080,axiom,
( ~ sP6(sK16,X2,sK33(sK16))
| ~ member(sK16,X1,X2)
| agent(sK16,sK30(sK16,sK31(sK16,X0,sK33(sK16)),X1),X1)
| ~ group(sK16,X0) ) ).
cnf(u75,axiom,
( sP8(X0,sK20(X0),sK26(X0))
| ~ sP10(X0) ) ).
cnf(u1009,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK32(sK16,sK39(sK16),sK33(sK16))),X0) ) ).
cnf(u846,negated_conjecture,
( ~ sP8(sK47,X0,sK19(sK47))
| state(sK47,sK28(sK47,X0,sK32(sK47,sK19(sK47),sK26(sK47)))) ) ).
cnf(u73,axiom,
( group(X0,sK26(X0))
| ~ sP10(X0) ) ).
cnf(u852,negated_conjecture,
member(sK47,sK31(sK47,sK26(sK47),sK26(sK47)),sK26(sK47)) ).
cnf(u857,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK31(sK47,sK19(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u100,axiom,
( ~ sP7(X0,X1)
| ~ member(X0,X2,X1)
| black(X0,X2) ) ).
cnf(u1868,negated_conjecture,
( ~ barrel(sK16,X4)
| ~ city(sK16,X0)
| ~ placename(sK16,X1)
| ~ of(sK16,X1,X0)
| ~ hollywood_placename(sK16,X1)
| ~ chevy(sK16,X2)
| ~ white(sK16,X2)
| ~ dirty(sK16,X2)
| ~ old(sK16,X2)
| ~ street(sK16,X3)
| ~ lonely(sK16,X3)
| ~ event(sK16,X4)
| ~ agent(sK16,X4,X2)
| ~ present(sK16,X4)
| ~ frontseat(sK16,X0)
| ~ down(sK16,X4,X3)
| ~ in(sK16,X4,X0)
| ~ in(sK16,X5,X0)
| ~ be(sK16,sK41(sK16,sK34(sK16),X6),sK44(sK16,X0,sK39(sK16)),X5)
| ~ member(sK16,X6,sK39(sK16)) ) ).
cnf(u871,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK31(sK47,sK27(sK47),sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u79,axiom,
( ~ sP10(X0)
| present(X0,sK25(X0)) ) ).
cnf(u347,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| present(sK47,sK30(sK47,sK46(sK47,sK19(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1990,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK14(sK47,sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u90,axiom,
( ~ sP10(X0)
| city(X0,sK21(X0)) ) ).
cnf(u985,axiom,
member(sK16,sK32(sK16,sK40(sK16),sK33(sK16)),sK40(sK16)) ).
cnf(u1131,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK31(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u999,axiom,
cheap(sK16,sK32(sK16,sK40(sK16),sK33(sK16))) ).
cnf(u1994,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK14(sK47,sK26(sK47))),sK14(sK47,sK26(sK47)),sK29(sK47,X0,sK14(sK47,sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u345,negated_conjecture,
( ~ sP8(sK47,X0,sK19(sK47))
| in(sK47,sK29(sK47,X0,sK46(sK47,sK19(sK47))),X0) ) ).
cnf(u861,negated_conjecture,
fellow(sK47,sK31(sK47,sK26(sK47),sK26(sK47))) ).
cnf(u88,axiom,
( ~ sP10(X0)
| placename(X0,sK22(X0)) ) ).
cnf(u859,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK31(sK47,sK19(sK47),sK26(sK47))),sK31(sK47,sK19(sK47),sK26(sK47)),sK29(sK47,X0,sK31(sK47,sK19(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1645,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK17(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u119,axiom,
( ~ sP4(X0)
| down(X0,sK38(X0),sK37(X0)) ) ).
cnf(u1751,negated_conjecture,
( ~ sP6(sK16,X1,sK40(sK16))
| agent(sK16,sK30(sK16,sK46(sK16,sK40(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u1643,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK17(sK16,sK39(sK16),sK39(sK16))),X0) ) ).
cnf(u374,negated_conjecture,
fellow(sK47,sK46(sK47,sK26(sK47))) ).
cnf(u874,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK31(sK47,sK27(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1649,negated_conjecture,
fellow(sK16,sK17(sK16,sK33(sK16),sK39(sK16))) ).
cnf(u1747,negated_conjecture,
( agent(sK16,sK43(sK16,sK46(sK16,sK40(sK16)),X0),X0)
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u117,axiom,
( ~ sP4(X0)
| sP2(X0,sK34(X0),sK39(X0)) ) ).
cnf(u247,negated_conjecture,
down(sK47,sK25(sK47),sK24(sK47)) ).
cnf(u257,negated_conjecture,
chevy(sK47,sK23(sK47)) ).
cnf(u372,axiom,
( ~ sP10(X0)
| fellow(X0,X1)
| ~ member(X0,X1,sK26(X0)) ) ).
cnf(u1002,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| event(sK16,sK30(sK16,sK32(sK16,sK40(sK16),sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1557,negated_conjecture,
member(sK16,sK18(sK16,sK33(sK16),sK39(sK16)),sK33(sK16)) ).
cnf(u1518,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK45(sK47,sK26(sK47))),sK45(sK47,sK26(sK47)),sK29(sK47,X0,sK45(sK47,sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u245,negated_conjecture,
two(sK47,sK26(sK47)) ).
cnf(u1008,axiom,
young(sK16,sK32(sK16,sK39(sK16),sK33(sK16))) ).
cnf(u1791,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK13(sK16,sK34(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u385,negated_conjecture,
cheap(sK47,sK46(sK47,sK27(sK47))) ).
cnf(u1137,axiom,
young(sK16,sK31(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u1790,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK13(sK16,sK34(sK16),sK39(sK16))),X0) ) ).
cnf(u128,axiom,
( ~ sP4(X0)
| white(X0,sK36(X0)) ) ).
cnf(u1793,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK13(sK16,sK34(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u261,negated_conjecture,
of(sK47,sK22(sK47),sK21(sK47)) ).
cnf(u1574,negated_conjecture,
( ~ sP8(sK16,X0,sK40(sK16))
| in(sK16,sK29(sK16,X0,sK18(sK16,sK40(sK16),sK39(sK16))),X0) ) ).
cnf(u134,axiom,
( ~ sP4(X0)
| frontseat(X0,sK34(X0)) ) ).
cnf(u543,axiom,
two(sK16,sK39(sK16)) ).
cnf(u1580,negated_conjecture,
fellow(sK16,sK18(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u2000,negated_conjecture,
( event(sK47,sK30(sK47,sK15(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u132,axiom,
( ~ sP4(X0)
| city(X0,sK34(X0)) ) ).
cnf(u546,axiom,
down(sK16,sK38(sK16),sK37(sK16)) ).
cnf(u147,axiom,
( ~ sP0(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| patient(X0,sK43(X0,X3,X4),X3) ) ).
cnf(u1062,axiom,
( agent(sK16,sK43(sK16,sK32(sK16,sK40(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u552,axiom,
street(sK16,sK37(sK16)) ).
cnf(u569,axiom,
( event(sK16,sK43(sK16,X1,X0))
| ~ member(sK16,X1,sK40(sK16))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1055,axiom,
( ~ sP6(sK16,X1,sK33(sK16))
| agent(sK16,sK30(sK16,sK32(sK16,sK33(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u801,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| present(sK47,sK30(sK47,sK15(sK47,sK19(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u815,negated_conjecture,
( ~ group(sK47,X0)
| member(sK47,sK31(sK47,X0,sK26(sK47)),sK26(sK47)) ) ).
cnf(u1066,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| agent(sK16,sK30(sK16,sK32(sK16,sK40(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u145,axiom,
( ~ sP0(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| nonreflexive(X0,sK43(X0,X3,X4)) ) ).
cnf(u1190,negated_conjecture,
young(sK47,sK14(sK47,sK26(sK47))) ).
cnf(u1075,axiom,
( be(sK16,sK28(sK16,X0,sK32(sK16,sK39(sK16),sK39(sK16))),sK32(sK16,sK39(sK16),sK39(sK16)),sK29(sK16,X0,sK32(sK16,sK39(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u830,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK32(sK47,sK26(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1064,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| event(sK16,sK30(sK16,sK32(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u573,axiom,
( ~ member(sK16,X0,sK40(sK16))
| black(sK16,X0) ) ).
cnf(u571,axiom,
( ~ member(sK16,X1,sK40(sK16))
| ~ member(sK16,X0,sK33(sK16))
| agent(sK16,sK43(sK16,X1,X0),X0) ) ).
cnf(u836,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| event(sK47,sK30(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u841,negated_conjecture,
( ~ sP8(sK47,X0,sK19(sK47))
| in(sK47,sK29(sK47,X0,sK32(sK47,sK19(sK47),sK26(sK47))),X0) ) ).
cnf(u84,axiom,
( ~ sP10(X0)
| old(X0,sK23(X0)) ) ).
cnf(u855,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK31(sK47,sK19(sK47),sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u74,axiom,
( ~ sP10(X0)
| two(X0,sK26(X0)) ) ).
cnf(u352,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| event(sK47,sK30(sK47,sK46(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u845,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK32(sK47,sK19(sK47),sK26(sK47))),sK32(sK47,sK19(sK47),sK26(sK47)),sK29(sK47,X0,sK32(sK47,sK19(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK19(sK47)) ) ).
cnf(u72,axiom,
( sP9(X0,sK26(X0))
| ~ sP10(X0) ) ).
cnf(u843,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| present(sK47,sK30(sK47,sK32(sK47,sK19(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1629,negated_conjecture,
member(sK16,sK17(sK16,sK39(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u103,axiom,
( ~ sP6(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| nonreflexive(X0,sK30(X0,X3,X4)) ) ).
cnf(u1140,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK31(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1627,negated_conjecture,
member(sK16,sK17(sK16,sK33(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u358,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK46(sK47,sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u858,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK31(sK47,sK19(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1633,negated_conjecture,
fellow(sK16,sK17(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u101,axiom,
( ~ sP7(X0,X1)
| ~ member(X0,X2,X1)
| coat(X0,X2) ) ).
cnf(u864,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK31(sK47,sK26(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1647,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK17(sK16,sK39(sK16),sK39(sK16))),sK17(sK16,sK39(sK16),sK39(sK16)),sK29(sK16,X0,sK17(sK16,sK39(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u369,axiom,
( ~ sP10(X0)
| young(X0,X1)
| ~ member(X0,X1,sK26(X0)) ) ).
cnf(u356,negated_conjecture,
( ~ sP8(sK47,X0,sK27(sK47))
| state(sK47,sK28(sK47,X0,sK46(sK47,sK27(sK47)))) ) ).
cnf(u1646,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK17(sK16,sK39(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u112,axiom,
( ~ sP4(X0)
| group(X0,sK40(X0)) ) ).
cnf(u1744,negated_conjecture,
black(sK16,sK46(sK16,sK40(sK16))) ).
cnf(u986,axiom,
member(sK16,sK32(sK16,sK39(sK16),sK33(sK16)),sK39(sK16)) ).
cnf(u1652,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK17(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1515,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK45(sK47,sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u992,axiom,
( ~ sP6(sK16,X1,sK33(sK16))
| present(sK16,sK30(sK16,sK32(sK16,sK33(sK16),sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u375,negated_conjecture,
( ~ member(sK47,X1,sK27(sK47))
| ~ member(sK47,X0,sK19(sK47))
| patient(sK47,sK30(sK47,X1,X0),X1) ) ).
cnf(u1650,negated_conjecture,
young(sK16,sK17(sK16,sK33(sK16),sK39(sK16))) ).
cnf(u118,axiom,
( ~ sP4(X0)
| in(X0,sK38(X0),sK34(X0)) ) ).
cnf(u1013,axiom,
( be(sK16,sK28(sK16,X0,sK32(sK16,sK39(sK16),sK33(sK16))),sK32(sK16,sK39(sK16),sK33(sK16)),sK29(sK16,X0,sK32(sK16,sK39(sK16),sK33(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u1656,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK17(sK16,sK33(sK16),sK39(sK16)))) ) ).
cnf(u1011,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK32(sK16,sK39(sK16),sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1148,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK31(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u246,negated_conjecture,
in(sK47,sK25(sK47),sK21(sK47)) ).
cnf(u1564,negated_conjecture,
( ~ sP6(sK16,X1,sK33(sK16))
| event(sK16,sK30(sK16,sK18(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1138,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK31(sK16,sK40(sK16),sK39(sK16))),X0) ) ).
cnf(u141,axiom,
( ~ sP1(X0,X1)
| ~ member(X0,X2,X1)
| cheap(X0,X2) ) ).
cnf(u1984,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| present(sK47,sK30(sK47,sK15(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u258,negated_conjecture,
placename(sK47,sK22(sK47)) ).
cnf(u244,negated_conjecture,
sP6(sK47,sK19(sK47),sK27(sK47)) ).
cnf(u2014,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK13(sK47,sK20(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u131,axiom,
( ~ sP4(X0)
| hollywood_placename(X0,sK35(X0)) ) ).
cnf(u1046,axiom,
member(sK16,sK32(sK16,sK33(sK16),sK39(sK16)),sK33(sK16)) ).
cnf(u553,axiom,
old(sK16,sK36(sK16)) ).
cnf(u1069,axiom,
fellow(sK16,sK32(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u799,negated_conjecture,
( ~ sP8(sK47,X0,sK19(sK47))
| in(sK47,sK29(sK47,X0,sK15(sK47,sK19(sK47))),X0) ) ).
cnf(u129,axiom,
( ~ sP4(X0)
| chevy(X0,sK36(X0)) ) ).
cnf(u384,negated_conjecture,
( ~ member(sK47,X0,sK27(sK47))
| cheap(sK47,X0) ) ).
cnf(u1059,axiom,
black(sK16,sK32(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u1328,negated_conjecture,
( present(sK47,sK30(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u1048,axiom,
member(sK16,sK32(sK16,sK39(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u820,negated_conjecture,
member(sK47,sK32(sK47,sK19(sK47),sK26(sK47)),sK19(sK47)) ).
cnf(u557,axiom,
placename(sK16,sK35(sK16)) ).
cnf(u1079,axiom,
( ~ sP6(sK16,X2,sK33(sK16))
| ~ member(sK16,X1,X2)
| present(sK16,sK30(sK16,sK31(sK16,X0,sK33(sK16)),X1))
| ~ group(sK16,X0) ) ).
cnf(u825,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK32(sK47,sK26(sK47),sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u146,axiom,
( ~ sP0(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| present(X0,sK43(X0,X3,X4)) ) ).
cnf(u555,axiom,
white(sK16,sK36(sK16)) ).
cnf(u948,axiom,
( ~ group(sK16,X0)
| member(sK16,sK32(sK16,X0,sK39(sK16)),X0) ) ).
cnf(u574,axiom,
( ~ member(sK16,X0,sK40(sK16))
| coat(sK16,X0) ) ).
cnf(u839,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK32(sK47,sK27(sK47),sK26(sK47))),sK32(sK47,sK27(sK47),sK26(sK47)),sK29(sK47,X0,sK32(sK47,sK27(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK27(sK47)) ) ).
cnf(u827,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK32(sK47,sK26(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u936,axiom,
coat(sK16,sK15(sK16,sK40(sK16))) ).
cnf(u1476,negated_conjecture,
( ~ sP6(sK16,X1,sK33(sK16))
| present(sK16,sK30(sK16,sK46(sK16,sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1870,axiom,
( patient(sK16,sK43(sK16,sK15(sK16,sK40(sK16)),X0),sK15(sK16,sK40(sK16)))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1876,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| event(sK16,sK30(sK16,sK15(sK16,sK40(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u87,axiom,
( ~ sP10(X0)
| chevy(X0,sK23(X0)) ) ).
cnf(u1874,axiom,
( agent(sK16,sK43(sK16,sK15(sK16,sK40(sK16)),X0),X0)
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1124,axiom,
member(sK16,sK31(sK16,sK39(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u1880,axiom,
( ~ sP8(sK16,X0,sK40(sK16))
| state(sK16,sK28(sK16,X0,sK15(sK16,sK40(sK16)))) ) ).
cnf(u1479,negated_conjecture,
( ~ sP8(sK16,X0,sK33(sK16))
| state(sK16,sK28(sK16,X0,sK46(sK16,sK33(sK16)))) ) ).
cnf(u842,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| event(sK47,sK30(sK47,sK32(sK47,sK19(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u85,axiom,
( ~ sP10(X0)
| dirty(X0,sK23(X0)) ) ).
cnf(u353,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| present(sK47,sK30(sK47,sK46(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u869,negated_conjecture,
fellow(sK47,sK31(sK47,sK27(sK47),sK26(sK47))) ).
cnf(u96,axiom,
( ~ member(X0,X3,X2)
| in(X0,sK29(X0,X1,X3),X1)
| ~ sP8(X0,X1,X2) ) ).
cnf(u1745,negated_conjecture,
coat(sK16,sK46(sK16,sK40(sK16))) ).
cnf(u1636,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK17(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u867,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK31(sK47,sK26(sK47),sK26(sK47))),sK31(sK47,sK26(sK47),sK26(sK47)),sK29(sK47,X0,sK31(sK47,sK26(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1653,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK17(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u359,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK46(sK47,sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1634,negated_conjecture,
young(sK16,sK17(sK16,sK40(sK16),sK39(sK16))) ).
cnf(u1991,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK14(sK47,sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1651,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK17(sK16,sK33(sK16),sK39(sK16))),X0) ) ).
cnf(u102,axiom,
( ~ sP6(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| wear(X0,sK30(X0,X3,X4)) ) ).
cnf(u997,axiom,
black(sK16,sK32(sK16,sK40(sK16),sK33(sK16))) ).
cnf(u1640,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK17(sK16,sK40(sK16),sK39(sK16)))) ) ).
cnf(u1519,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK45(sK47,sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u995,axiom,
( ~ sP8(sK16,X0,sK33(sK16))
| state(sK16,sK28(sK16,X0,sK32(sK16,sK33(sK16),sK33(sK16)))) ) ).
cnf(u125,axiom,
( ~ sP4(X0)
| street(X0,sK37(X0)) ) ).
cnf(u357,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK46(sK47,sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u380,axiom,
( ~ sP10(X0)
| black(X0,X1)
| ~ member(X0,X1,sK27(X0)) ) ).
cnf(u2011,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK13(sK47,sK20(sK47),sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1141,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK31(sK16,sK40(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u1010,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK32(sK16,sK39(sK16),sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1122,axiom,
member(sK16,sK31(sK16,sK33(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u2017,negated_conjecture,
( present(sK47,sK30(sK47,sK15(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u115,axiom,
( ~ sP4(X0)
| group(X0,sK39(X0)) ) ).
cnf(u253,negated_conjecture,
street(sK47,sK24(sK47)) ).
cnf(u2013,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK13(sK47,sK20(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u370,negated_conjecture,
( ~ member(sK47,X0,sK26(sK47))
| young(sK47,X0) ) ).
cnf(u1145,axiom,
young(sK16,sK31(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u1795,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK13(sK16,sK34(sK16),sK39(sK16)))) ) ).
cnf(u1400,axiom,
fellow(sK16,sK13(sK16,sK34(sK16),sK39(sK16))) ).
cnf(u113,axiom,
( ~ sP4(X0)
| sP0(X0,sK33(X0),sK40(X0)) ) ).
cnf(u1151,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK31(sK16,sK39(sK16),sK39(sK16)))) ) ).
cnf(u142,axiom,
( ~ sP1(X0,X1)
| ~ member(X0,X2,X1)
| black(X0,X2) ) ).
cnf(u1053,axiom,
( ~ sP6(sK16,X1,sK33(sK16))
| event(sK16,sK30(sK16,sK32(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1014,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK32(sK16,sK39(sK16),sK33(sK16)))) ) ).
cnf(u259,negated_conjecture,
hollywood_placename(sK47,sK22(sK47)) ).
cnf(u1057,axiom,
( ~ sP8(sK16,X0,sK33(sK16))
| state(sK16,sK28(sK16,X0,sK32(sK16,sK33(sK16),sK39(sK16)))) ) ).
cnf(u140,axiom,
( ~ sP2(X0,X1,X2)
| ~ member(X0,X3,X2)
| state(X0,sK41(X0,X1,X3)) ) ).
cnf(u804,negated_conjecture,
( ~ sP8(sK47,X0,sK19(sK47))
| state(sK47,sK28(sK47,X0,sK15(sK47,sK19(sK47)))) ) ).
cnf(u1070,axiom,
young(sK16,sK32(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u541,axiom,
sP3(sK16,sK39(sK16)) ).
cnf(u1063,axiom,
( ~ sP8(sK16,X0,sK40(sK16))
| in(sK16,sK29(sK16,X0,sK32(sK16,sK40(sK16),sK39(sK16))),X0) ) ).
cnf(u130,axiom,
( ~ sP4(X0)
| placename(X0,sK35(X0)) ) ).
cnf(u539,axiom,
group(sK16,sK40(sK16)) ).
cnf(u823,negated_conjecture,
fellow(sK47,sK32(sK47,sK26(sK47),sK26(sK47))) ).
cnf(u1068,axiom,
( ~ sP8(sK16,X0,sK40(sK16))
| state(sK16,sK28(sK16,X0,sK32(sK16,sK40(sK16),sK39(sK16)))) ) ).
cnf(u558,axiom,
hollywood_placename(sK16,sK35(sK16)) ).
cnf(u1072,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK32(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1575,negated_conjecture,
( ~ sP6(sK16,X1,sK40(sK16))
| event(sK16,sK30(sK16,sK18(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u564,axiom,
( be(sK16,sK41(sK16,sK34(sK16),X0),X0,sK42(sK16,sK34(sK16),X0))
| ~ member(sK16,X0,sK39(sK16)) ) ).
cnf(u996,axiom,
( patient(sK16,sK43(sK16,sK32(sK16,sK40(sK16),sK33(sK16)),X0),sK32(sK16,sK40(sK16),sK33(sK16)))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1578,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK18(sK16,sK40(sK16),sK39(sK16))),sK18(sK16,sK40(sK16),sK39(sK16)),sK29(sK16,X0,sK18(sK16,sK40(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK40(sK16)) ) ).
cnf(u1982,negated_conjecture,
( ~ sP8(sK47,X0,sK27(sK47))
| in(sK47,sK29(sK47,X0,sK15(sK47,sK27(sK47))),X0) ) ).
cnf(u1584,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK18(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u826,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK32(sK47,sK26(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u71,axiom,
( ~ sP10(X0)
| sP6(X0,sK19(X0),sK27(X0)) ) ).
cnf(u69,axiom,
( sP7(X0,sK27(X0))
| ~ sP10(X0) ) ).
cnf(u832,negated_conjecture,
black(sK47,sK32(sK47,sK27(sK47),sK26(sK47))) ).
cnf(u1986,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK15(sK47,sK27(sK47))),sK15(sK47,sK27(sK47)),sK29(sK47,X0,sK15(sK47,sK27(sK47))))
| ~ sP8(sK47,X0,sK27(sK47)) ) ).
cnf(u853,negated_conjecture,
fellow(sK47,sK31(sK47,sK19(sK47),sK26(sK47))) ).
cnf(u80,axiom,
( ~ sP10(X0)
| agent(X0,sK25(X0),sK23(X0)) ) ).
cnf(u851,negated_conjecture,
member(sK47,sK31(sK47,sK27(sK47),sK26(sK47)),sK26(sK47)) ).
cnf(u1065,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| present(sK16,sK30(sK16,sK32(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1558,negated_conjecture,
member(sK16,sK18(sK16,sK40(sK16),sK39(sK16)),sK40(sK16)) ).
cnf(u1743,negated_conjecture,
( patient(sK16,sK43(sK16,sK46(sK16,sK40(sK16)),X0),sK46(sK16,sK40(sK16)))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1635,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK17(sK16,sK40(sK16),sK39(sK16))),X0) ) ).
cnf(u86,axiom,
( ~ sP10(X0)
| white(X0,sK23(X0)) ) ).
cnf(u866,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK31(sK47,sK26(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1474,negated_conjecture,
( ~ sP8(sK16,X0,sK33(sK16))
| in(sK16,sK29(sK16,X0,sK46(sK16,sK33(sK16))),X0) ) ).
cnf(u1748,negated_conjecture,
( ~ sP8(sK16,X0,sK40(sK16))
| in(sK16,sK29(sK16,X0,sK46(sK16,sK40(sK16))),X0) ) ).
cnf(u109,axiom,
( ~ sP5(X0,X1,X2)
| member(X0,sK32(X0,X1,X2),X1) ) ).
cnf(u872,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK31(sK47,sK27(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1746,negated_conjecture,
cheap(sK16,sK46(sK16,sK40(sK16))) ).
cnf(u364,negated_conjecture,
( event(sK47,sK30(sK47,sK46(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u1654,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK17(sK16,sK33(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u1995,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK14(sK47,sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1752,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK46(sK16,sK40(sK16))),sK46(sK16,sK40(sK16)),sK29(sK16,X0,sK46(sK16,sK40(sK16))))
| ~ sP8(sK16,X0,sK40(sK16)) ) ).
cnf(u994,axiom,
( be(sK16,sK28(sK16,X0,sK32(sK16,sK33(sK16),sK33(sK16))),sK32(sK16,sK33(sK16),sK33(sK16)),sK29(sK16,X0,sK32(sK16,sK33(sK16),sK33(sK16))))
| ~ sP8(sK16,X0,sK33(sK16)) ) ).
cnf(u99,axiom,
( ~ sP7(X0,X1)
| ~ member(X0,X2,X1)
| cheap(X0,X2) ) ).
cnf(u383,axiom,
( ~ sP10(X0)
| cheap(X0,X1)
| ~ member(X0,X1,sK27(X0)) ) ).
cnf(u2015,negated_conjecture,
( ~ sP8(sK47,X0,sK26(sK47))
| be(sK47,sK28(sK47,X0,sK13(sK47,sK20(sK47),sK26(sK47))),sK13(sK47,sK20(sK47),sK26(sK47)),sK29(sK47,X0,sK13(sK47,sK20(sK47),sK26(sK47)))) ) ).
cnf(u354,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| agent(sK47,sK30(sK47,sK46(sK47,sK27(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1129,axiom,
young(sK16,sK31(sK16,sK33(sK16),sK39(sK16))) ).
cnf(u126,axiom,
( ~ sP4(X0)
| old(X0,sK36(X0)) ) ).
cnf(u870,negated_conjecture,
young(sK47,sK31(sK47,sK27(sK47),sK26(sK47))) ).
cnf(u1514,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK45(sK47,sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u97,axiom,
( ~ member(X0,X3,X2)
| be(X0,sK28(X0,X1,X3),X3,sK29(X0,X1,X3))
| ~ sP8(X0,X1,X2) ) ).
cnf(u876,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK31(sK47,sK27(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u1142,axiom,
( be(sK16,sK28(sK16,X0,sK31(sK16,sK40(sK16),sK39(sK16))),sK31(sK16,sK40(sK16),sK39(sK16)),sK29(sK16,X0,sK31(sK16,sK40(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u381,negated_conjecture,
( ~ member(sK47,X0,sK27(sK47))
| black(sK47,X0) ) ).
cnf(u1135,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK31(sK16,sK33(sK16),sK39(sK16)))) ) ).
cnf(u124,axiom,
( ~ sP4(X0)
| lonely(X0,sK37(X0)) ) ).
cnf(u254,negated_conjecture,
old(sK47,sK23(sK47)) ).
cnf(u998,axiom,
coat(sK16,sK32(sK16,sK40(sK16),sK33(sK16))) ).
cnf(u1397,axiom,
member(sK16,sK13(sK16,sK34(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u1512,negated_conjecture,
fellow(sK47,sK45(sK47,sK26(sK47))) ).
cnf(u1004,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| agent(sK16,sK30(sK16,sK32(sK16,sK40(sK16),sK33(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u371,negated_conjecture,
young(sK47,sK46(sK47,sK26(sK47))) ).
cnf(u114,axiom,
( ~ sP4(X0)
| sP3(X0,sK39(X0)) ) ).
cnf(u1401,axiom,
young(sK16,sK13(sK16,sK34(sK16),sK39(sK16))) ).
cnf(u252,negated_conjecture,
lonely(sK47,sK24(sK47)) ).
cnf(u1144,axiom,
fellow(sK16,sK31(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u139,axiom,
( ~ sP2(X0,X1,X2)
| ~ member(X0,X3,X2)
| be(X0,sK41(X0,X1,X3),X3,sK42(X0,X1,X3)) ) ).
cnf(u1054,axiom,
( ~ sP6(sK16,X1,sK33(sK16))
| present(sK16,sK30(sK16,sK32(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1047,axiom,
member(sK16,sK32(sK16,sK40(sK16),sK39(sK16)),sK40(sK16)) ).
cnf(u807,negated_conjecture,
coat(sK47,sK15(sK47,sK27(sK47))) ).
cnf(u137,axiom,
( ~ sP3(X0,X1)
| ~ member(X0,X2,X1)
| fellow(X0,X2) ) ).
cnf(u1052,axiom,
( ~ sP8(sK16,X0,sK33(sK16))
| in(sK16,sK29(sK16,X0,sK32(sK16,sK33(sK16),sK39(sK16))),X0) ) ).
cnf(u1067,axiom,
( be(sK16,sK28(sK16,X0,sK32(sK16,sK40(sK16),sK39(sK16))),sK32(sK16,sK40(sK16),sK39(sK16)),sK29(sK16,X0,sK32(sK16,sK40(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK40(sK16)) ) ).
cnf(u542,axiom,
group(sK16,sK39(sK16)) ).
cnf(u1056,axiom,
( be(sK16,sK28(sK16,X0,sK32(sK16,sK33(sK16),sK39(sK16))),sK32(sK16,sK33(sK16),sK39(sK16)),sK29(sK16,X0,sK32(sK16,sK33(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK33(sK16)) ) ).
cnf(u935,axiom,
black(sK16,sK15(sK16,sK40(sK16))) ).
cnf(u143,axiom,
( ~ sP1(X0,X1)
| ~ member(X0,X2,X1)
| coat(X0,X2) ) ).
cnf(u548,axiom,
present(sK16,sK38(sK16)) ).
cnf(u565,axiom,
( state(sK16,sK41(sK16,sK34(sK16),X0))
| ~ member(sK16,X0,sK39(sK16)) ) ).
cnf(u563,axiom,
( in(sK16,sK42(sK16,sK34(sK16),X0),sK34(sK16))
| ~ member(sK16,X0,sK39(sK16)) ) ).
cnf(u1581,negated_conjecture,
young(sK16,sK18(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u1579,negated_conjecture,
( ~ sP8(sK16,X0,sK40(sK16))
| state(sK16,sK28(sK16,X0,sK18(sK16,sK40(sK16),sK39(sK16)))) ) ).
cnf(u1568,negated_conjecture,
( ~ sP8(sK16,X0,sK33(sK16))
| state(sK16,sK28(sK16,X0,sK18(sK16,sK33(sK16),sK39(sK16)))) ) ).
cnf(u1585,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK18(sK16,sK39(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u816,negated_conjecture,
( ~ group(sK47,X0)
| member(sK47,sK32(sK47,X0,sK26(sK47)),X0) ) ).
cnf(u567,axiom,
( nonreflexive(sK16,sK43(sK16,X1,X0))
| ~ member(sK16,X1,sK40(sK16))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u837,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| present(sK47,sK30(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u570,axiom,
( present(sK16,sK43(sK16,X1,X0))
| ~ member(sK16,X1,sK40(sK16))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u835,negated_conjecture,
( ~ sP8(sK47,X0,sK27(sK47))
| in(sK47,sK29(sK47,X0,sK32(sK47,sK27(sK47),sK26(sK47))),X0) ) ).
cnf(u1981,negated_conjecture,
( patient(sK47,sK30(sK47,sK15(sK47,sK27(sK47)),X0),sK15(sK47,sK27(sK47)))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u70,axiom,
( group(X0,sK27(X0))
| ~ sP10(X0) ) ).
cnf(u850,negated_conjecture,
member(sK47,sK31(sK47,sK19(sK47),sK26(sK47)),sK26(sK47)) ).
cnf(u93,axiom,
( group(X0,sK19(X0))
| ~ sP10(X0) ) ).
cnf(u856,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| event(sK47,sK30(sK47,sK31(sK47,sK19(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u576,axiom,
( ~ member(sK16,X0,sK39(sK16))
| young(sK16,X0) ) ).
cnf(u348,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| agent(sK47,sK30(sK47,sK46(sK47,sK19(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1638,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK17(sK16,sK40(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u68,axiom,
( ~ patient(X0,X5,sK17(X0,X1,X2))
| ~ agent(X0,X5,sK18(X0,X1,X2))
| ~ event(X0,X5)
| ~ present(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ wear(X0,X5)
| ~ sP11(X0,X1,X2) ) ).
cnf(u1644,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK17(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1985,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| agent(sK47,sK30(sK47,sK15(sK47,sK27(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u83,axiom,
( ~ sP10(X0)
| street(X0,sK24(X0)) ) ).
cnf(u367,negated_conjecture,
( wear(sK47,sK30(sK47,X1,X0))
| ~ member(sK47,X1,sK27(sK47))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u1999,negated_conjecture,
( agent(sK47,sK30(sK47,sK15(sK47,sK27(sK47)),X0),X0)
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u110,axiom,
( ~ patient(X0,X5,sK31(X0,X1,X2))
| ~ agent(X0,X5,sK32(X0,X1,X2))
| ~ event(X0,X5)
| ~ present(X0,X5)
| ~ nonreflexive(X0,X5)
| ~ wear(X0,X5)
| ~ sP5(X0,X1,X2) ) ).
cnf(u854,negated_conjecture,
young(sK47,sK31(sK47,sK19(sK47),sK26(sK47))) ).
cnf(u81,axiom,
( ~ sP10(X0)
| event(X0,sK25(X0)) ) ).
cnf(u860,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK31(sK47,sK19(sK47),sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u365,negated_conjecture,
( present(sK47,sK30(sK47,sK46(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u865,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK31(sK47,sK26(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u108,axiom,
( ~ sP5(X0,X1,X2)
| member(X0,sK31(X0,X1,X2),X2) ) ).
cnf(u1149,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK31(sK16,sK39(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u1496,negated_conjecture,
( ~ group(sK16,X0)
| member(sK16,sK17(sK16,X0,sK39(sK16)),sK39(sK16)) ) ).
cnf(u1130,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK31(sK16,sK33(sK16),sK39(sK16))),X0) ) ).
cnf(u2021,negated_conjecture,
be(sK47,sK28(sK47,sK20(sK47),sK13(sK47,sK20(sK47),sK26(sK47))),sK13(sK47,sK20(sK47),sK26(sK47)),sK29(sK47,sK20(sK47),sK13(sK47,sK20(sK47),sK26(sK47)))) ).
cnf(u123,axiom,
( ~ sP4(X0)
| event(X0,sK38(X0)) ) ).
cnf(u355,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK46(sK47,sK27(sK47))),sK46(sK47,sK27(sK47)),sK29(sK47,X0,sK46(sK47,sK27(sK47))))
| ~ sP8(sK47,X0,sK27(sK47)) ) ).
cnf(u378,negated_conjecture,
( ~ member(sK47,X0,sK27(sK47))
| coat(sK47,X0) ) ).
cnf(u98,axiom,
( ~ member(X0,X3,X2)
| state(X0,sK28(X0,X1,X3))
| ~ sP8(X0,X1,X2) ) ).
cnf(u993,axiom,
( ~ sP6(sK16,X1,sK33(sK16))
| agent(sK16,sK30(sK16,sK32(sK16,sK33(sK16),sK33(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u1139,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK31(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1128,axiom,
fellow(sK16,sK31(sK16,sK33(sK16),sK39(sK16))) ).
cnf(u1007,axiom,
fellow(sK16,sK32(sK16,sK39(sK16),sK33(sK16))) ).
cnf(u121,axiom,
( ~ sP4(X0)
| present(X0,sK38(X0)) ) ).
cnf(u251,negated_conjecture,
event(sK47,sK25(sK47)) ).
cnf(u376,negated_conjecture,
( patient(sK47,sK30(sK47,sK46(sK47,sK27(sK47)),X0),sK46(sK47,sK27(sK47)))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u2008,negated_conjecture,
member(sK47,sK13(sK47,sK20(sK47),sK26(sK47)),sK26(sK47)) ).
cnf(u1513,negated_conjecture,
young(sK47,sK45(sK47,sK26(sK47))) ).
cnf(u127,axiom,
( ~ sP4(X0)
| dirty(X0,sK36(X0)) ) ).
cnf(u249,negated_conjecture,
present(sK47,sK25(sK47)) ).
cnf(u1637,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK17(sK16,sK40(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u382,negated_conjecture,
black(sK47,sK46(sK47,sK27(sK47))) ).
cnf(u1792,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK13(sK16,sK34(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u255,negated_conjecture,
dirty(sK47,sK23(sK47)) ).
cnf(u549,axiom,
agent(sK16,sK38(sK16),sK36(sK16)) ).
cnf(u1920,negated_conjecture,
~ member(sK16,sK44(sK16,sK34(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u138,axiom,
( ~ sP2(X0,X1,X2)
| ~ member(X0,X3,X2)
| in(X0,sK42(X0,X1,X3),X1) ) ).
cnf(u547,axiom,
barrel(sK16,sK38(sK16)) ).
cnf(u1565,negated_conjecture,
( ~ sP6(sK16,X1,sK33(sK16))
| present(sK16,sK30(sK16,sK18(sK16,sK33(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1076,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK32(sK16,sK39(sK16),sK39(sK16)))) ) ).
cnf(u1563,negated_conjecture,
( ~ sP8(sK16,X0,sK33(sK16))
| in(sK16,sK29(sK16,X0,sK18(sK16,sK33(sK16),sK39(sK16))),X0) ) ).
cnf(u136,axiom,
( ~ sP3(X0,X1)
| ~ member(X0,X2,X1)
| young(X0,X2) ) ).
cnf(u1569,negated_conjecture,
( patient(sK16,sK43(sK16,sK18(sK16,sK40(sK16),sK39(sK16)),X0),sK18(sK16,sK40(sK16),sK39(sK16)))
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1323,negated_conjecture,
( event(sK47,sK30(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),X0))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u566,axiom,
( ~ member(sK16,X1,sK40(sK16))
| ~ member(sK16,X0,sK33(sK16))
| patient(sK16,sK43(sK16,X1,X0),X1) ) ).
cnf(u800,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| event(sK47,sK30(sK47,sK15(sK47,sK19(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1583,negated_conjecture,
( ~ sP6(sK16,X1,sK39(sK16))
| event(sK16,sK30(sK16,sK18(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u572,axiom,
( ~ member(sK16,X0,sK40(sK16))
| cheap(sK16,X0) ) ).
cnf(u1582,negated_conjecture,
( ~ sP8(sK16,X0,sK39(sK16))
| in(sK16,sK29(sK16,X0,sK18(sK16,sK39(sK16),sK39(sK16))),X0) ) ).
cnf(u821,negated_conjecture,
member(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),sK27(sK47)) ).
cnf(u551,axiom,
lonely(sK16,sK37(sK16)) ).
cnf(u1586,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK18(sK16,sK39(sK16),sK39(sK16))),sK18(sK16,sK39(sK16),sK39(sK16)),sK29(sK16,X0,sK18(sK16,sK39(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u554,axiom,
dirty(sK16,sK36(sK16)) ).
cnf(u947,axiom,
( ~ group(sK16,X0)
| member(sK16,sK31(sK16,X0,sK39(sK16)),sK39(sK16)) ) ).
cnf(u560,axiom,
of(sK16,sK35(sK16),sK34(sK16)) ).
cnf(u834,negated_conjecture,
( patient(sK47,sK30(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),X0),sK32(sK47,sK27(sK47),sK26(sK47)))
| ~ member(sK47,X0,sK19(sK47)) ) ).
cnf(u1074,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK32(sK16,sK39(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u77,axiom,
( ~ sP10(X0)
| down(X0,sK25(X0),sK24(X0)) ) ).
cnf(u840,negated_conjecture,
( ~ sP8(sK47,X0,sK27(sK47))
| state(sK47,sK28(sK47,X0,sK32(sK47,sK27(sK47),sK26(sK47)))) ) ).
cnf(u1983,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| event(sK47,sK30(sK47,sK15(sK47,sK27(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1073,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| present(sK16,sK30(sK16,sK32(sK16,sK39(sK16),sK39(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u1628,negated_conjecture,
member(sK16,sK17(sK16,sK40(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u1475,negated_conjecture,
( ~ sP6(sK16,X1,sK33(sK16))
| event(sK16,sK30(sK16,sK46(sK16,sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u67,axiom,
( ~ sP11(X0,X1,X2)
| member(X0,sK18(X0,X1,X2),X1) ) ).
cnf(u1478,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK46(sK16,sK33(sK16))),sK46(sK16,sK33(sK16)),sK29(sK16,X0,sK46(sK16,sK33(sK16))))
| ~ sP8(sK16,X0,sK33(sK16)) ) ).
cnf(u1877,axiom,
( ~ sP6(sK16,X1,sK40(sK16))
| present(sK16,sK30(sK16,sK15(sK16,sK40(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u351,negated_conjecture,
( ~ sP8(sK47,X0,sK27(sK47))
| in(sK47,sK29(sK47,X0,sK46(sK47,sK27(sK47))),X0) ) ).
cnf(u1875,axiom,
( ~ sP8(sK16,X0,sK40(sK16))
| in(sK16,sK29(sK16,X0,sK15(sK16,sK40(sK16))),X0) ) ).
cnf(u94,axiom,
( ~ sP9(X0,X1)
| ~ member(X0,X2,X1)
| young(X0,X2) ) ).
cnf(u838,negated_conjecture,
( ~ sP6(sK47,X1,sK27(sK47))
| agent(sK47,sK30(sK47,sK32(sK47,sK27(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u844,negated_conjecture,
( ~ sP6(sK47,X1,sK19(sK47))
| agent(sK47,sK30(sK47,sK32(sK47,sK19(sK47),sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u349,negated_conjecture,
( be(sK47,sK28(sK47,X0,sK46(sK47,sK19(sK47))),sK46(sK47,sK19(sK47)),sK29(sK47,X0,sK46(sK47,sK19(sK47))))
| ~ sP8(sK47,X0,sK19(sK47)) ) ).
cnf(u92,axiom,
( frontseat(X0,sK20(X0))
| ~ sP10(X0) ) ).
cnf(u1133,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK31(sK16,sK33(sK16),sK39(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u863,negated_conjecture,
( in(sK47,sK29(sK47,X0,sK31(sK47,sK26(sK47),sK26(sK47))),X0)
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u2009,negated_conjecture,
fellow(sK47,sK13(sK47,sK20(sK47),sK26(sK47))) ).
cnf(u107,axiom,
( ~ member(X0,X3,X2)
| ~ member(X0,X4,X1)
| event(X0,sK30(X0,X3,X4))
| ~ sP6(X0,X1,X2) ) ).
cnf(u362,negated_conjecture,
( state(sK47,sK28(sK47,X0,sK46(sK47,sK26(sK47))))
| ~ sP8(sK47,X0,sK26(sK47)) ) ).
cnf(u82,axiom,
( ~ sP10(X0)
| lonely(X0,sK24(X0)) ) ).
cnf(u1123,axiom,
member(sK16,sK31(sK16,sK40(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u991,axiom,
( ~ sP6(sK16,X1,sK33(sK16))
| event(sK16,sK30(sK16,sK32(sK16,sK33(sK16),sK33(sK16)),X0))
| ~ member(sK16,X0,X1) ) ).
cnf(u105,axiom,
( ~ sP6(X0,X1,X2)
| ~ member(X0,X4,X1)
| ~ member(X0,X3,X2)
| patient(X0,sK30(X0,X3,X4),X3) ) ).
cnf(u1516,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK45(sK47,sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1150,axiom,
( be(sK16,sK28(sK16,X0,sK31(sK16,sK39(sK16),sK39(sK16))),sK31(sK16,sK39(sK16),sK39(sK16)),sK29(sK16,X0,sK31(sK16,sK39(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u360,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| agent(sK47,sK30(sK47,sK46(sK47,sK26(sK47)),X0),X0)
| ~ member(sK47,X0,X1) ) ).
cnf(u1143,axiom,
( ~ sP8(sK16,X0,sK39(sK16))
| state(sK16,sK28(sK16,X0,sK31(sK16,sK40(sK16),sK39(sK16)))) ) ).
cnf(u1992,negated_conjecture,
( ~ sP6(sK47,X1,sK26(sK47))
| present(sK47,sK30(sK47,sK14(sK47,sK26(sK47)),X0))
| ~ member(sK47,X0,X1) ) ).
cnf(u1559,negated_conjecture,
member(sK16,sK18(sK16,sK39(sK16),sK39(sK16)),sK39(sK16)) ).
cnf(u1497,negated_conjecture,
( ~ group(sK16,X0)
| member(sK16,sK18(sK16,X0,sK39(sK16)),X0) ) ).
cnf(u1006,axiom,
( ~ sP8(sK16,X0,sK40(sK16))
| state(sK16,sK28(sK16,X0,sK32(sK16,sK40(sK16),sK33(sK16)))) ) ).
cnf(u111,axiom,
( ~ sP4(X0)
| sP1(X0,sK40(X0)) ) ).
cnf(u1012,axiom,
( ~ sP6(sK16,X1,sK39(sK16))
| agent(sK16,sK30(sK16,sK32(sK16,sK39(sK16),sK33(sK16)),X0),X0)
| ~ member(sK16,X0,X1) ) ).
cnf(u379,negated_conjecture,
coat(sK47,sK46(sK47,sK27(sK47))) ).
cnf(u122,axiom,
( ~ sP4(X0)
| agent(X0,sK38(X0),sK36(X0)) ) ).
cnf(u1641,negated_conjecture,
fellow(sK16,sK17(sK16,sK39(sK16),sK39(sK16))) ).
cnf(u1655,negated_conjecture,
( be(sK16,sK28(sK16,X0,sK17(sK16,sK33(sK16),sK39(sK16))),sK17(sK16,sK33(sK16),sK39(sK16)),sK29(sK16,X0,sK17(sK16,sK33(sK16),sK39(sK16))))
| ~ sP8(sK16,X0,sK39(sK16)) ) ).
cnf(u377,axiom,
( ~ sP10(X0)
| coat(X0,X1)
| ~ member(X0,X1,sK27(X0)) ) ).
cnf(u120,axiom,
( ~ sP4(X0)
| barrel(X0,sK38(X0)) ) ).
cnf(u250,negated_conjecture,
agent(sK47,sK25(sK47),sK23(sK47)) ).
cnf(u1000,axiom,
( agent(sK16,sK43(sK16,sK32(sK16,sK40(sK16),sK33(sK16)),X0),X0)
| ~ member(sK16,X0,sK33(sK16)) ) ).
cnf(u1060,axiom,
coat(sK16,sK32(sK16,sK40(sK16),sK39(sK16))) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP163+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n002.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 18:16:21 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.06/2.32 % (3792611)Detected formulas, will run a generic FOF schedule.
% 9.06/2.32 % (3792620)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=147151587:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.06/2.32 % (3792618)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=166040171:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.06/2.32 % (3792616)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2557044938:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.06/2.32 % (3792617)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3581560974:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.06/2.32 % (3792619)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=444100966:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.06/2.32 % (3792620)Instruction limit reached!
% 9.06/2.32 % (3792620)------------------------------
% 9.06/2.32 % (3792620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792620)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792620)Termination reason: Instruction limit
% 9.06/2.32 % (3792620)Termination phase: Saturation
% 9.06/2.32 % (3792620)Time elapsed: 0.029 s
% 9.06/2.32 % (3792620)Peak memory usage: 89 MB
% 9.06/2.32 % (3792620)Instructions burned: 124 (million)
% 9.06/2.32 % (3792621)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2526812516:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.06/2.32 % (3792619)Refutation not found, incomplete strategy
% 9.06/2.32 % (3792619)------------------------------
% 9.06/2.32 % (3792619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792619)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792619)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.32 % (3792619)Time elapsed: 0.019 s
% 9.06/2.32 % (3792619)Peak memory usage: 88 MB
% 9.06/2.32 % (3792619)Instructions burned: 35 (million)
% 9.06/2.32 % (3792622)dis-21_1_sil=8000:lcm=predicate:random_seed=167069556:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.06/2.32 % (3792621)Refutation not found, incomplete strategy
% 9.06/2.32 % (3792621)------------------------------
% 9.06/2.32 % (3792621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792621)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792621)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.32 % (3792621)Time elapsed: 0.052 s
% 9.06/2.32 % (3792621)Peak memory usage: 90 MB
% 9.06/2.32 % (3792621)Instructions burned: 89 (million)
% 9.06/2.32 % (3792622)Instruction limit reached!
% 9.06/2.32 % (3792622)------------------------------
% 9.06/2.32 % (3792622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792622)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792622)Termination reason: Instruction limit
% 9.06/2.32 % (3792622)Termination phase: Saturation
% 9.06/2.32 % (3792622)Time elapsed: 0.064 s
% 9.06/2.32 % (3792622)Peak memory usage: 89 MB
% 9.06/2.32 % (3792622)Instructions burned: 130 (million)
% 9.06/2.32 % (3792628)lrs+10_1_sil=8000:sp=occurrence:random_seed=1987718770:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 9.06/2.32 % (3792628)Instruction limit reached!
% 9.06/2.32 % (3792628)------------------------------
% 9.06/2.32 % (3792628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792628)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792628)Termination reason: Instruction limit
% 9.06/2.32 % (3792628)Termination phase: Saturation
% 9.06/2.32 % (3792628)Time elapsed: 0.069 s
% 9.06/2.32 % (3792628)Peak memory usage: 91 MB
% 9.06/2.32 % (3792628)Instructions burned: 290 (million)
% 9.06/2.32 % (3792619)------------------------------
% 9.06/2.32 % (3792619)------------------------------
% 9.06/2.32 % (3792631)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2099964112:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.06/2.32 % (3792631)Refutation not found, incomplete strategy
% 9.06/2.32 % (3792631)------------------------------
% 9.06/2.32 % (3792631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792631)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792631)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.32 % (3792631)Time elapsed: 0.008 s
% 9.06/2.32 % (3792631)Peak memory usage: 89 MB
% 9.06/2.32 % (3792631)Instructions burned: 12 (million)
% 9.06/2.32 % (3792621)------------------------------
% 9.06/2.32 % (3792621)------------------------------
% 9.06/2.32 % (3792633)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2454961339:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 9.06/2.32 % (3792633)Refutation not found, incomplete strategy
% 9.06/2.32 % (3792633)------------------------------
% 9.06/2.32 % (3792633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792633)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792633)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.32 % (3792633)Time elapsed: 0.027 s
% 9.06/2.32 % (3792633)Peak memory usage: 89 MB
% 9.06/2.32 % (3792633)Instructions burned: 84 (million)
% 9.06/2.32 % (3792635)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=483872426:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.06/2.32 % (3792635)Refutation not found, incomplete strategy
% 9.06/2.32 % (3792635)------------------------------
% 9.06/2.32 % (3792635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792635)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792635)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.32 % (3792635)Time elapsed: 0.008 s
% 9.06/2.32 % (3792635)Peak memory usage: 89 MB
% 9.06/2.32 % (3792635)Instructions burned: 11 (million)
% 9.06/2.32 % (3792636)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3522111216:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.06/2.32 % (3792636)Refutation not found, incomplete strategy
% 9.06/2.32 % (3792636)------------------------------
% 9.06/2.32 % (3792636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792636)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792636)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.32 % (3792636)Time elapsed: 0.003 s
% 9.06/2.32 % (3792636)Peak memory usage: 88 MB
% 9.06/2.32 % (3792636)Instructions burned: 4 (million)
% 9.06/2.32 % (3792633)------------------------------
% 9.06/2.32 % (3792633)------------------------------
% 9.06/2.32 % (3792631)------------------------------
% 9.06/2.32 % (3792631)------------------------------
% 9.06/2.32 % (3792640)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2083730608:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 9.06/2.32 % (3792641)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1294648875:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 9.06/2.32 % (3792635)------------------------------
% 9.06/2.32 % (3792635)------------------------------
% 9.06/2.32 % (3792636)------------------------------
% 9.06/2.32 % (3792636)------------------------------
% 9.06/2.32 % (3792641)Instruction limit reached!
% 9.06/2.32 % (3792641)------------------------------
% 9.06/2.32 % (3792641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792641)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792641)Termination reason: Instruction limit
% 9.06/2.32 % (3792641)Termination phase: Saturation
% 9.06/2.32 % (3792641)Time elapsed: 0.056 s
% 9.06/2.32 % (3792641)Peak memory usage: 90 MB
% 9.06/2.32 % (3792641)Instructions burned: 114 (million)
% 9.06/2.32 % (3792644)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2103722742:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 9.06/2.32 % (3792645)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=450887806:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 9.06/2.32 % (3792646)lrs+10_1_sil=8000:sp=occurrence:random_seed=216506223:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 9.06/2.32 % (3792644)Instruction limit reached!
% 9.06/2.32 % (3792644)------------------------------
% 9.06/2.32 % (3792644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792644)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792644)Termination reason: Instruction limit
% 9.06/2.32 % (3792644)Termination phase: Saturation
% 9.06/2.32 % (3792644)Time elapsed: 0.065 s
% 9.06/2.32 % (3792644)Peak memory usage: 88 MB
% 9.06/2.32 % (3792644)Instructions burned: 127 (million)
% 9.06/2.32 % (3792645)Instruction limit reached!
% 9.06/2.32 % (3792645)------------------------------
% 9.06/2.32 % (3792645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792645)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792645)Termination reason: Instruction limit
% 9.06/2.32 % (3792645)Termination phase: Property scanning
% 9.06/2.32 % (3792645)Time elapsed: 0.042 s
% 9.06/2.32 % (3792645)Peak memory usage: 87 MB
% 9.06/2.32 % (3792645)Instructions burned: 115 (million)
% 9.06/2.32 % (3792617)First to succeed.
% 9.06/2.32 % (3792617)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3792611"
% 9.06/2.32 % (3792650)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2677373501:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 9.06/2.32 % (3792650)Refutation not found, incomplete strategy
% 9.06/2.32 % (3792650)------------------------------
% 9.06/2.32 % (3792650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.06/2.32 % (3792650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.06/2.32 % (3792650)CaDiCaL version: 2.1.3
% 9.06/2.32 % (3792650)Termination reason: Refutation not found, incomplete strategy
% 9.06/2.32 % (3792650)Time elapsed: 0.004 s
% 9.06/2.32 % (3792650)Peak memory usage: 88 MB
% 9.06/2.32 % (3792650)Instructions burned: 7 (million)
% 9.06/2.32 % (3792651)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2806533844:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 9.06/2.32 % SZS status CounterSatisfiable for theBenchmark
% 9.06/2.32 % SZS output start Saturation.
% See solution above
% 10.70/2.41 % SZS output start Definitions and Model Updates.
% 10.70/2.41 % SZS output end Definitions and Model Updates.
% 10.70/2.41 % (3792617)------------------------------
% 10.70/2.41 % (3792617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.41 % (3792617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.41 % (3792617)CaDiCaL version: 2.1.3
% 10.70/2.41 % (3792617)Termination reason: Satisfiable
% 10.70/2.41 % (3792617)Time elapsed: 1.018 s
% 10.70/2.41 % (3792617)Peak memory usage: 133 MB
% 10.70/2.41 % (3792617)Instructions burned: 1499 (million)
% 10.70/2.41 % (3792617)------------------------------
% 10.70/2.41 % (3792617)------------------------------
% 10.70/2.41 % (3792611)Success in time 1.437 s
% 10.70/2.41 % Vampire exiting
%------------------------------------------------------------------------------