%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP165+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:09:10 PM UTC 2026
% Result : CounterSatisfiable 0.07s 0.39s
% Output : Saturation 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u344,negated_conjecture,
( ~ actual_world(X18)
| sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u347,negated_conjecture,
( ~ cheap(X52,sK21(X52,X61))
| ~ actual_world(X52)
| group(X52,X53)
| frontseat(X52,X54)
| ~ of(X52,X56,X55)
| ~ city(X52,X55)
| hollywood_placename(X52,X56)
| placename(X52,X56)
| ~ chevy(X52,X57)
| ~ white(X52,X57)
| ~ dirty(X52,X57)
| ~ old(X52,X57)
| ~ street(X52,X58)
| lonely(X52,X58)
| event(X52,X59)
| ~ agent(X52,X59,X57)
| ~ present(X52,X59)
| barrel(X52,X59)
| down(X52,X59,X58)
| in(X52,X59,X55)
| ~ sP26(sK24(X52,X54,X60),X60,X54,X52)
| ~ two(X52,X60)
| group(X52,X60)
| sP25(sK23(X52,X60),X60,X52)
| event(X52,X68)
| ~ agent(X52,X68,sK33(X52,X53,X61))
| patient(X52,X68,sK22(X52,X53,X61))
| ~ present(X52,X68)
| ~ nonreflexive(X52,X68)
| wear(X52,X68)
| group(X52,X61)
| coat(X52,sK21(X52,X61))
| black(X52,sK21(X52,X61)) ) ).
cnf(u352,negated_conjecture,
sP19(sK18,sK17,sK16,sK15,sK14,sK13,sK12,sK11,sK10,sK1) ).
cnf(u357,negated_conjecture,
actual_world(sK1) ).
cnf(u367,negated_conjecture,
( ~ wear(sK0,sK37(X48,X49))
| member(sK0,X48,sK9)
| member(sK0,X49,sK2) ) ).
cnf(u371,negated_conjecture,
( nonreflexive(sK0,sK37(X48,X49))
| member(sK0,X48,sK9)
| member(sK0,X49,sK2) ) ).
cnf(u375,negated_conjecture,
( present(sK0,sK37(X48,X49))
| member(sK0,X48,sK9)
| member(sK0,X49,sK2) ) ).
cnf(u379,negated_conjecture,
( ~ patient(sK0,sK37(X48,X49),X48)
| member(sK0,X48,sK9)
| member(sK0,X49,sK2) ) ).
cnf(u383,negated_conjecture,
( agent(sK0,sK37(X48,X49),X49)
| member(sK0,X48,sK9)
| member(sK0,X49,sK2) ) ).
cnf(u387,negated_conjecture,
( ~ event(sK0,sK37(X48,X49))
| member(sK0,X48,sK9)
| member(sK0,X49,sK2) ) ).
cnf(u403,negated_conjecture,
( ~ actual_world(X52)
| ~ member(X52,sK21(X52,X61),X61)
| group(X52,X53)
| frontseat(X52,X54)
| ~ of(X52,X56,X55)
| ~ city(X52,X55)
| hollywood_placename(X52,X56)
| placename(X52,X56)
| ~ chevy(X52,X57)
| ~ white(X52,X57)
| ~ dirty(X52,X57)
| ~ old(X52,X57)
| ~ street(X52,X58)
| lonely(X52,X58)
| event(X52,X59)
| ~ agent(X52,X59,X57)
| ~ present(X52,X59)
| barrel(X52,X59)
| down(X52,X59,X58)
| in(X52,X59,X55)
| ~ sP26(sK24(X52,X54,X60),X60,X54,X52)
| ~ two(X52,X60)
| group(X52,X60)
| sP25(sK23(X52,X60),X60,X52)
| ~ member(X52,sK33(X52,X53,X61),X53)
| group(X52,X61) ) ).
cnf(u409,negated_conjecture,
( ~ cheap(X52,sK21(X52,X61))
| ~ actual_world(X52)
| group(X52,X53)
| frontseat(X52,X54)
| ~ of(X52,X56,X55)
| ~ city(X52,X55)
| hollywood_placename(X52,X56)
| placename(X52,X56)
| ~ chevy(X52,X57)
| ~ white(X52,X57)
| ~ dirty(X52,X57)
| ~ old(X52,X57)
| ~ street(X52,X58)
| lonely(X52,X58)
| event(X52,X59)
| ~ agent(X52,X59,X57)
| ~ present(X52,X59)
| barrel(X52,X59)
| down(X52,X59,X58)
| in(X52,X59,X55)
| ~ sP26(sK24(X52,X54,X60),X60,X54,X52)
| ~ two(X52,X60)
| group(X52,X60)
| sP25(sK23(X52,X60),X60,X52)
| ~ member(X52,sK33(X52,X53,X61),X53)
| group(X52,X61)
| coat(X52,sK21(X52,X61))
| black(X52,sK21(X52,X61)) ) ).
cnf(u415,negated_conjecture,
( ~ in(sK0,sK32(X44),sK6)
| member(sK0,X44,sK8) ) ).
cnf(u419,negated_conjecture,
( ~ be(sK0,sK31(X44),X44,sK32(X44))
| member(sK0,X44,sK8) ) ).
cnf(u423,negated_conjecture,
( state(sK0,sK31(X44))
| member(sK0,X44,sK8) ) ).
cnf(u433,negated_conjecture,
( ~ cheap(X52,sK21(X52,X61))
| ~ actual_world(X52)
| group(X52,X53)
| frontseat(X52,X54)
| ~ of(X52,X56,X55)
| ~ city(X52,X55)
| hollywood_placename(X52,X56)
| placename(X52,X56)
| ~ chevy(X52,X57)
| ~ white(X52,X57)
| ~ dirty(X52,X57)
| ~ old(X52,X57)
| ~ street(X52,X58)
| lonely(X52,X58)
| event(X52,X59)
| ~ agent(X52,X59,X57)
| ~ present(X52,X59)
| barrel(X52,X59)
| down(X52,X59,X58)
| in(X52,X59,X55)
| ~ sP26(sK24(X52,X54,X60),X60,X54,X52)
| ~ two(X52,X60)
| group(X52,X60)
| sP25(sK23(X52,X60),X60,X52)
| ~ member(X52,sK22(X52,X53,X61),X61)
| group(X52,X61)
| coat(X52,sK21(X52,X61))
| black(X52,sK21(X52,X61)) ) ).
cnf(u439,negated_conjecture,
( member(sK0,X47,sK8)
| young(sK0,X47) ) ).
cnf(u443,negated_conjecture,
( member(sK0,X47,sK8)
| fellow(sK0,X47) ) ).
cnf(u451,negated_conjecture,
( member(sK0,X51,sK9)
| cheap(sK0,X51) ) ).
cnf(u455,negated_conjecture,
( member(sK0,X51,sK9)
| ~ black(sK0,X51) ) ).
cnf(u459,negated_conjecture,
( member(sK0,X51,sK9)
| ~ coat(sK0,X51) ) ).
cnf(u469,negated_conjecture,
( ~ actual_world(X52)
| ~ member(X52,sK21(X52,X61),X61)
| group(X52,X53)
| frontseat(X52,X54)
| ~ of(X52,X56,X55)
| ~ city(X52,X55)
| hollywood_placename(X52,X56)
| placename(X52,X56)
| ~ chevy(X52,X57)
| ~ white(X52,X57)
| ~ dirty(X52,X57)
| ~ old(X52,X57)
| ~ street(X52,X58)
| lonely(X52,X58)
| event(X52,X59)
| ~ agent(X52,X59,X57)
| ~ present(X52,X59)
| barrel(X52,X59)
| down(X52,X59,X58)
| in(X52,X59,X55)
| ~ sP26(sK24(X52,X54,X60),X60,X54,X52)
| ~ two(X52,X60)
| group(X52,X60)
| sP25(sK23(X52,X60),X60,X52)
| ~ member(X52,sK22(X52,X53,X61),X61)
| group(X52,X61) ) ).
cnf(u476,negated_conjecture,
~ group(sK0,sK9) ).
cnf(u481,negated_conjecture,
~ group(sK0,sK8) ).
cnf(u485,negated_conjecture,
~ two(sK0,sK8) ).
cnf(u491,negated_conjecture,
~ in(sK0,sK7,sK3) ).
cnf(u496,negated_conjecture,
~ down(sK0,sK7,sK6) ).
cnf(u501,negated_conjecture,
~ barrel(sK0,sK7) ).
cnf(u506,negated_conjecture,
present(sK0,sK7) ).
cnf(u511,negated_conjecture,
agent(sK0,sK7,sK5) ).
cnf(u516,negated_conjecture,
~ event(sK0,sK7) ).
cnf(u521,negated_conjecture,
~ lonely(sK0,sK6) ).
cnf(u526,negated_conjecture,
street(sK0,sK6) ).
cnf(u531,negated_conjecture,
old(sK0,sK5) ).
cnf(u536,negated_conjecture,
dirty(sK0,sK5) ).
cnf(u541,negated_conjecture,
white(sK0,sK5) ).
cnf(u546,negated_conjecture,
chevy(sK0,sK5) ).
cnf(u551,negated_conjecture,
~ placename(sK0,sK4) ).
cnf(u556,negated_conjecture,
~ hollywood_placename(sK0,sK4) ).
cnf(u561,negated_conjecture,
city(sK0,sK3) ).
cnf(u566,negated_conjecture,
of(sK0,sK4,sK3) ).
cnf(u570,negated_conjecture,
frontseat(sK0,sK6) ).
cnf(u576,negated_conjecture,
~ group(sK0,sK2) ).
cnf(u623,negated_conjecture,
actual_world(sK0) ).
cnf(u637,negated_conjecture,
( ~ two(sK0,X8)
| sP25(sK23(sK0,X8),X8,sK0)
| group(sK0,X8)
| frontseat(sK0,X2)
| ~ sP26(sK24(sK0,X2,X8),X8,X2,sK0) ) ).
cnf(u665,negated_conjecture,
( ~ sP26(sK24(sK0,X0,sK8),sK8,X0,sK0)
| frontseat(sK0,X0) ) ).
cnf(u729,negated_conjecture,
( ~ member(sK1,sK21(sK1,X0),X0)
| group(sK1,X0)
| ~ member(sK1,sK33(sK1,X1,X0),X1)
| group(sK1,X1) ) ).
cnf(u733,negated_conjecture,
( ~ member(sK1,sK21(sK1,X0),X0)
| group(sK1,X0)
| ~ member(sK1,sK22(sK1,X1,X0),X0)
| group(sK1,X1) ) ).
cnf(u769,negated_conjecture,
( ~ two(sK0,X2)
| frontseat(sK0,X3)
| ~ city(sK0,X5)
| placename(sK0,X7)
| ~ of(sK0,X7,X5)
| hollywood_placename(sK0,X7)
| ~ chevy(sK0,X6)
| ~ white(sK0,X6)
| ~ dirty(sK0,X6)
| ~ old(sK0,X6)
| ~ street(sK0,X3)
| lonely(sK0,X3)
| event(sK0,X4)
| ~ agent(sK0,X4,X6)
| ~ present(sK0,X4)
| barrel(sK0,X4)
| in(sK0,X4,X5)
| down(sK0,X4,X3)
| ~ member(sK0,sK30(sK0,X3,X2),X2)
| ~ member(sK0,sK29(sK0,X2),X2)
| group(sK0,X2) ) ).
cnf(u780,negated_conjecture,
( ~ two(sK0,X2)
| frontseat(sK0,X5)
| ~ city(sK0,X7)
| placename(sK0,X9)
| ~ of(sK0,X9,X7)
| hollywood_placename(sK0,X9)
| ~ chevy(sK0,X8)
| ~ white(sK0,X8)
| ~ dirty(sK0,X8)
| ~ old(sK0,X8)
| ~ street(sK0,X5)
| lonely(sK0,X5)
| event(sK0,X6)
| ~ agent(sK0,X6,X8)
| ~ present(sK0,X6)
| barrel(sK0,X6)
| in(sK0,X6,X7)
| down(sK0,X6,X5)
| sP38(X3,X4,sK30(sK0,X5,X2),X5,sK0)
| ~ member(sK0,sK29(sK0,X2),X2)
| group(sK0,X2) ) ).
cnf(u796,negated_conjecture,
( ~ two(sK1,X2)
| frontseat(sK1,X3)
| ~ city(sK1,X5)
| placename(sK1,X7)
| ~ of(sK1,X7,X5)
| hollywood_placename(sK1,X7)
| ~ chevy(sK1,X6)
| ~ white(sK1,X6)
| ~ dirty(sK1,X6)
| ~ old(sK1,X6)
| ~ street(sK1,X3)
| lonely(sK1,X3)
| event(sK1,X4)
| ~ agent(sK1,X4,X6)
| ~ present(sK1,X4)
| barrel(sK1,X4)
| in(sK1,X4,X5)
| down(sK1,X4,X3)
| ~ member(sK1,sK30(sK1,X3,X2),X2)
| ~ member(sK1,sK29(sK1,X2),X2)
| group(sK1,X2) ) ).
cnf(u803,negated_conjecture,
( ~ member(sK1,sK27(sK1,X0),X0)
| group(sK1,X0)
| group(sK1,X1)
| ~ member(sK1,sK36(sK1,X1,X0),X1) ) ).
cnf(u807,negated_conjecture,
( ~ two(sK1,X2)
| frontseat(sK1,X5)
| ~ city(sK1,X7)
| placename(sK1,X9)
| ~ of(sK1,X9,X7)
| hollywood_placename(sK1,X9)
| ~ chevy(sK1,X8)
| ~ white(sK1,X8)
| ~ dirty(sK1,X8)
| ~ old(sK1,X8)
| ~ street(sK1,X5)
| lonely(sK1,X5)
| event(sK1,X6)
| ~ agent(sK1,X6,X8)
| ~ present(sK1,X6)
| barrel(sK1,X6)
| in(sK1,X6,X7)
| down(sK1,X6,X5)
| sP38(X3,X4,sK30(sK1,X5,X2),X5,sK1)
| ~ member(sK1,sK29(sK1,X2),X2)
| group(sK1,X2) ) ).
cnf(u827,negated_conjecture,
~ group(sK1,sK17) ).
cnf(u837,negated_conjecture,
~ cheap(sK1,sK27(sK1,sK18)) ).
cnf(u841,negated_conjecture,
( ~ member(sK1,sK28(sK1,X0,sK18),sK18)
| group(sK1,X0) ) ).
cnf(u844,negated_conjecture,
~ group(sK1,sK18) ).
cnf(u854,negated_conjecture,
~ lonely(sK1,sK15) ).
cnf(u869,negated_conjecture,
( ~ member(sK1,sK33(sK1,X0,sK18),X0)
| group(sK1,X0) ) ).
cnf(u876,negated_conjecture,
( ~ member(sK1,sK22(sK1,X0,sK18),sK18)
| group(sK1,X0) ) ).
cnf(u893,negated_conjecture,
~ member(sK0,sK29(sK0,sK8),sK8) ).
cnf(u978,negated_conjecture,
fellow(sK1,sK21(sK1,sK17)) ).
cnf(u986,negated_conjecture,
young(sK1,sK21(sK1,sK17)) ).
cnf(u995,negated_conjecture,
( ~ member(sK1,sK36(sK1,X0,sK17),X0)
| group(sK1,X0) ) ).
cnf(u1025,negated_conjecture,
member(sK1,sK29(sK1,sK17),sK17) ).
cnf(u1029,negated_conjecture,
( ~ street(sK1,X0)
| ~ member(sK1,sK30(sK1,X0,sK17),sK17)
| lonely(sK1,X0)
| frontseat(sK1,X0)
| ~ city(sK1,X1)
| down(sK1,X4,X0)
| event(sK1,X4)
| ~ agent(sK1,X4,X3)
| ~ chevy(sK1,X3)
| in(sK1,X4,X1)
| barrel(sK1,X4)
| ~ present(sK1,X4)
| ~ old(sK1,X3)
| ~ dirty(sK1,X3)
| ~ white(sK1,X3)
| hollywood_placename(sK1,X2)
| placename(sK1,X2)
| ~ of(sK1,X2,X1) ) ).
cnf(u1035,negated_conjecture,
( ~ street(sK1,X0)
| sP38(X5,X6,sK30(sK1,X0,sK17),X0,sK1)
| lonely(sK1,X0)
| frontseat(sK1,X0)
| ~ city(sK1,X1)
| down(sK1,X4,X0)
| event(sK1,X4)
| ~ agent(sK1,X4,X3)
| ~ chevy(sK1,X3)
| in(sK1,X4,X1)
| barrel(sK1,X4)
| ~ present(sK1,X4)
| ~ old(sK1,X3)
| ~ dirty(sK1,X3)
| ~ white(sK1,X3)
| hollywood_placename(sK1,X2)
| placename(sK1,X2)
| ~ of(sK1,X2,X1) ) ).
cnf(u1052,negated_conjecture,
~ fellow(sK1,sK29(sK1,sK17)) ).
cnf(u1081,negated_conjecture,
cheap(sK1,sK36(sK1,sK18,sK17)) ).
cnf(u1104,negated_conjecture,
( ~ member(sK1,sK36(sK1,X0,sK18),X0)
| group(sK1,X0) ) ).
cnf(u1146,negated_conjecture,
frontseat(sK1,sK15) ).
cnf(u1150,negated_conjecture,
~ member(sK1,sK30(sK1,sK15,sK17),sK17) ).
cnf(u1193,negated_conjecture,
~ sP25(sK30(sK1,sK15,sK17),X0,sK1) ).
cnf(u1196,negated_conjecture,
fellow(sK1,sK30(sK1,sK15,sK17)) ).
cnf(u295,negated_conjecture,
( ~ young(X18,sK29(X18,X25))
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ member(X18,sK27(X18,X26),X26)
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u339,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ young(X18,sK29(X18,X25))
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u884,negated_conjecture,
( ~ sP19(X4,X3,X5,X6,X7,X8,X9,sK11,X10,sK1)
| sP26(X0,X2,X1,sK1)
| member(sK1,X0,sK17)
| member(sK1,X0,X3)
| in(sK1,sK35(sK1,sK11,X0),X1) ) ).
cnf(u752,negated_conjecture,
( member(sK1,X0,sK17)
| young(sK1,X0) ) ).
cnf(u288,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ young(X18,sK29(X18,X25))
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u283,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| fellow(X0,X13)
| member(X0,X13,X8) ) ).
cnf(u1136,negated_conjecture,
( cheap(sK1,sK22(sK1,X0,sK18))
| group(sK1,X0) ) ).
cnf(u239,negated_conjecture,
( ~ group(X0,X9)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u1181,negated_conjecture,
~ sP19(X0,X1,X2,X3,X4,X5,X6,sK15,X7,sK1) ).
cnf(u754,negated_conjecture,
( ~ in(sK1,sK35(sK1,sK11,X0),sK11)
| member(sK1,X0,sK17) ) ).
cnf(u1133,negated_conjecture,
fellow(sK1,sK33(sK1,sK17,sK18)) ).
cnf(u116,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| agent(X0,X7,X5) ) ).
cnf(u336,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u287,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ young(X18,sK29(X18,X25))
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u331,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| member(X0,X15,X1)
| present(X0,sK39(X0,X14,X15))
| member(X0,X14,X9) ) ).
cnf(u123,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| chevy(X0,X5) ) ).
cnf(u744,negated_conjecture,
old(sK1,sK14) ).
cnf(u750,negated_conjecture,
( member(sK1,X0,sK18)
| cheap(sK1,X0) ) ).
cnf(u290,negated_conjecture,
( ~ young(X18,sK29(X18,X25))
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ member(X18,sK27(X18,X26),X26)
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u758,negated_conjecture,
sP20(X0,X1,X2,X3,X4,X5,X6,X7,sK0) ).
cnf(u293,negated_conjecture,
( ~ be(X0,sK34(X0,X2,X10),X10,sK35(X0,X2,X10))
| member(X0,X10,X8)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u745,negated_conjecture,
dirty(sK1,sK14) ).
cnf(u705,negated_conjecture,
( fellow(sK0,sK24(sK0,X0,sK8))
| frontseat(sK0,X0) ) ).
cnf(u1065,negated_conjecture,
fellow(sK1,sK36(sK1,sK17,sK17)) ).
cnf(u335,negated_conjecture,
( ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18)
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ member(X18,sK27(X18,X26),X26) ) ).
cnf(u630,negated_conjecture,
( sP26(X0,X2,X1,sK0)
| in(sK0,sK32(X0),X1)
| member(sK0,X0,sK8) ) ).
cnf(u231,negated_conjecture,
( ~ hollywood_placename(X0,X4)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u294,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| ~ in(X0,sK35(X0,X2,X10),X2)
| member(X0,X10,X8) ) ).
cnf(u743,negated_conjecture,
street(sK1,sK15) ).
cnf(u755,negated_conjecture,
( agent(sK1,sK39(sK1,X1,X0),X0)
| member(sK1,X0,sK10)
| member(sK1,X1,sK18) ) ).
cnf(u338,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ young(X18,sK29(X18,X25))
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u281,negated_conjecture,
( ~ black(X0,X17)
| member(X0,X17,X9)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u234,negated_conjecture,
( ~ event(X0,X7)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u341,negated_conjecture,
( ~ young(X18,sK29(X18,X25))
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ member(X18,sK27(X18,X26),X26)
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u749,negated_conjecture,
of(sK1,sK13,sK12) ).
cnf(u885,negated_conjecture,
( ~ sP19(X5,X6,X0,X7,X8,X9,X1,X10,X11,sK1)
| sP26(X3,X4,X1,sK1)
| member(sK1,X2,sK17)
| be(sK1,sK34(sK1,sK11,X2),X3,X0) ) ).
cnf(u68,negated_conjecture,
( ~ young(X52,X65)
| ~ fellow(X52,X65)
| ~ sP25(X65,X60,X52) ) ).
cnf(u627,negated_conjecture,
( be(sK0,sK31(X0),X1,X2)
| in(sK0,X2,X3)
| sP26(X1,X4,X3,sK0)
| member(sK0,X0,sK8) ) ).
cnf(u742,negated_conjecture,
agent(sK1,sK16,sK14) ).
cnf(u285,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u329,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| member(X0,X15,X1)
| agent(X0,sK39(X0,X14,X15),X15)
| member(X0,X14,X9) ) ).
cnf(u121,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| dirty(X0,X5) ) ).
cnf(u1203,negated_conjecture,
( ~ sP19(X3,X4,sK35(sK1,sK11,X0),X5,X6,X7,X1,X8,X9,sK1)
| member(sK1,X0,sK17)
| sP26(X0,X2,X1,sK1) ) ).
cnf(u1135,negated_conjecture,
cheap(sK1,sK33(sK1,sK18,sK18)) ).
cnf(u1138,negated_conjecture,
~ sP25(sK33(sK1,sK17,sK18),X0,sK1) ).
cnf(u261,negated_conjecture,
( ~ sP25(X65,X60,X52)
| ~ member(X52,X65,X60) ) ).
cnf(u333,negated_conjecture,
( ~ wear(X0,sK39(X0,X14,X15))
| member(X0,X15,X1)
| member(X0,X14,X9)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u741,negated_conjecture,
present(sK1,sK16) ).
cnf(u229,negated_conjecture,
( ~ group(X0,X1)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u292,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| state(X0,sK34(X0,X2,X10))
| member(X0,X10,X8) ) ).
cnf(u299,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u232,negated_conjecture,
( ~ placename(X0,X4)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u1134,negated_conjecture,
young(sK1,sK33(sK1,sK17,sK18)) ).
cnf(u698,negated_conjecture,
( be(sK0,sK31(X1),sK24(sK0,X0,sK8),X2)
| frontseat(sK0,X0)
| in(sK0,X2,X0)
| member(sK0,X1,sK8) ) ).
cnf(u1188,negated_conjecture,
young(sK1,sK36(sK1,sK17,sK18)) ).
cnf(u711,negated_conjecture,
( ~ sP19(X1,X2,sK32(sK24(sK0,X0,sK8)),X3,X4,X5,X0,X6,X7,sK0)
| frontseat(sK0,X0) ) ).
cnf(u302,negated_conjecture,
( ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18)
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ member(X18,sK27(X18,X26),X26) ) ).
cnf(u280,negated_conjecture,
( ~ coat(X0,X17)
| member(X0,X17,X9)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u340,negated_conjecture,
( ~ young(X18,sK29(X18,X25))
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ member(X18,sK27(X18,X26),X26)
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u236,negated_conjecture,
( ~ down(X0,X7,X6)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u127,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| of(X0,X4,X3) ) ).
cnf(u748,negated_conjecture,
city(sK1,sK12) ).
cnf(u760,negated_conjecture,
( be(sK1,sK34(sK1,sK11,X0),X1,X2)
| in(sK1,X2,X3)
| sP26(X1,X4,X3,sK1)
| member(sK1,X0,sK17) ) ).
cnf(u746,negated_conjecture,
white(sK1,sK14) ).
cnf(u925,negated_conjecture,
~ sP25(sK29(sK0,sK8),X0,sK0) ).
cnf(u1066,negated_conjecture,
young(sK1,sK36(sK1,sK17,sK17)) ).
cnf(u286,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u756,negated_conjecture,
( present(sK1,sK39(sK1,X1,X0))
| member(sK1,X0,sK10)
| member(sK1,X1,sK18) ) ).
cnf(u284,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| young(X0,X13)
| member(X0,X13,X8) ) ).
cnf(u328,negated_conjecture,
( ~ event(X0,sK39(X0,X14,X15))
| member(X0,X15,X1)
| member(X0,X14,X9)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u115,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| present(X0,X7) ) ).
cnf(u264,negated_conjecture,
( ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18)
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ member(X18,sK27(X18,X26),X26) ) ).
cnf(u699,negated_conjecture,
( ~ member(sK0,sK24(sK0,X0,sK8),sK8)
| frontseat(sK0,X0) ) ).
cnf(u759,negated_conjecture,
sP20(X0,X1,X2,X3,X4,X5,X6,X7,sK1) ).
cnf(u297,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ young(X18,sK29(X18,X25))
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u970,negated_conjecture,
( sP26(X0,X1,sK12,sK1)
| be(sK1,sK34(sK1,sK11,X2),X0,sK16)
| member(sK1,X2,sK17) ) ).
cnf(u709,negated_conjecture,
( in(sK0,sK32(sK24(sK0,X0,sK8)),X0)
| frontseat(sK0,X0) ) ).
cnf(u1139,negated_conjecture,
( cheap(sK1,sK28(sK1,X0,sK18))
| group(sK1,X0) ) ).
cnf(u332,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| member(X0,X15,X1)
| nonreflexive(X0,sK39(X0,X14,X15))
| member(X0,X14,X9) ) ).
cnf(u327,negated_conjecture,
( ~ sP38(X29,X28,X27,X23,X18)
| be(X18,X28,X27,X29)
| ~ state(X18,X28)
| in(X18,X29,X23) ) ).
cnf(u119,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| street(X0,X6) ) ).
cnf(u740,negated_conjecture,
two(sK1,sK17) ).
cnf(u916,negated_conjecture,
fellow(sK0,sK29(sK0,sK8)) ).
cnf(u263,negated_conjecture,
( ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18)
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ member(X18,sK27(X18,X26),X26) ) ).
cnf(u122,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| white(X0,X5) ) ).
cnf(u298,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ young(X18,sK29(X18,X25))
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u747,negated_conjecture,
chevy(sK1,sK14) ).
cnf(u301,negated_conjecture,
( ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18)
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ member(X18,sK27(X18,X26),X26) ) ).
cnf(u917,negated_conjecture,
young(sK0,sK29(sK0,sK8)) ).
cnf(u753,negated_conjecture,
( state(sK1,sK34(sK1,sK11,X0))
| member(sK1,X0,sK17) ) ).
cnf(u1069,negated_conjecture,
~ sP25(sK36(sK1,sK17,sK17),X0,sK1) ).
cnf(u330,negated_conjecture,
( ~ patient(X0,sK39(X0,X14,X15),X14)
| member(X0,X15,X1)
| member(X0,X14,X9)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u1020,negated_conjecture,
~ sP25(sK21(sK1,sK17),X0,sK1) ).
cnf(u282,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| cheap(X0,X17)
| member(X0,X17,X9) ) ).
cnf(u1182,negated_conjecture,
young(sK1,sK30(sK1,sK15,sK17)) ).
cnf(u235,negated_conjecture,
( ~ barrel(X0,X7)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u126,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| city(X0,X3) ) ).
cnf(u751,negated_conjecture,
( member(sK1,X0,sK17)
| fellow(sK1,X0) ) ).
cnf(u334,negated_conjecture,
( ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18)
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ member(X18,sK27(X18,X26),X26) ) ).
cnf(u289,negated_conjecture,
( ~ young(X18,sK29(X18,X25))
| group(X18,X26)
| ~ member(X18,sK28(X18,X19,X26),X26)
| ~ member(X18,sK27(X18,X26),X26)
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u230,negated_conjecture,
( ~ frontseat(X0,X2)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u972,negated_conjecture,
( sP26(X0,X1,X2,sK1)
| in(sK1,sK35(sK1,sK11,X0),X2)
| member(sK1,X0,sK17) ) ).
cnf(u757,negated_conjecture,
( nonreflexive(sK1,sK39(sK1,X1,X0))
| member(sK1,X0,sK10)
| member(sK1,X1,sK18) ) ).
cnf(u1204,negated_conjecture,
( sP26(X0,X1,sK11,sK1)
| member(sK1,X0,sK17) ) ).
cnf(u739,negated_conjecture,
~ sP19(X0,X1,X2,X3,X4,X5,X6,sK6,X7,sK0) ).
cnf(u238,negated_conjecture,
( ~ group(X0,X8)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u629,negated_conjecture,
( ~ sP19(X5,X6,X0,X7,X8,X9,X1,X10,X11,sK0)
| sP26(X3,X4,X1,sK0)
| member(sK0,X2,sK8)
| be(sK0,sK31(X2),X3,X0) ) ).
cnf(u337,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| wear(X18,X33)
| ~ nonreflexive(X18,X33)
| ~ present(X18,X33)
| patient(X18,X33,sK28(X18,X19,X26))
| ~ agent(X18,X33,sK36(X18,X19,X26))
| event(X18,X33)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| sP38(X29,X28,sK30(X18,X23,X25),X23,X18)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u233,negated_conjecture,
( ~ lonely(X0,X6)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u120,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| old(X0,X5) ) ).
cnf(u296,negated_conjecture,
( ~ young(X18,sK29(X18,X25))
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ member(X18,sK27(X18,X26),X26)
| ~ fellow(X18,sK29(X18,X25))
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u1201,negated_conjecture,
~ sP25(sK36(sK1,sK17,sK18),X0,sK1) ).
cnf(u291,negated_conjecture,
( ~ state(X52,X63)
| be(X52,X63,X62,X64)
| in(X52,X64,X54)
| sP26(X62,X60,X54,X52) ) ).
cnf(u1189,negated_conjecture,
cheap(sK1,sK36(sK1,sK18,sK18)) ).
cnf(u708,negated_conjecture,
( ~ sP25(sK24(sK0,X0,sK8),X1,sK0)
| frontseat(sK0,X0) ) ).
cnf(u111,negated_conjecture,
( ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0)
| two(X0,X8) ) ).
cnf(u706,negated_conjecture,
( young(sK0,sK24(sK0,X0,sK8))
| frontseat(sK0,X0) ) ).
cnf(u262,negated_conjecture,
( sP26(X62,X60,X54,X52)
| ~ member(X52,X62,X60) ) ).
cnf(u237,negated_conjecture,
( ~ in(X0,X7,X3)
| ~ sP19(X9,X8,X7,X6,X5,X4,X3,X2,X1,X0) ) ).
cnf(u300,negated_conjecture,
( ~ cheap(X18,sK27(X18,X26))
| black(X18,sK27(X18,X26))
| coat(X18,sK27(X18,X26))
| group(X18,X26)
| ~ member(X18,sK36(X18,X19,X26),X19)
| ~ member(X18,sK29(X18,X25),X25)
| group(X18,X25)
| ~ two(X18,X25)
| ~ member(X18,sK30(X18,X23,X25),X25)
| in(X18,X24,X20)
| down(X18,X24,X23)
| barrel(X18,X24)
| ~ present(X18,X24)
| ~ agent(X18,X24,X22)
| event(X18,X24)
| lonely(X18,X23)
| ~ street(X18,X23)
| ~ old(X18,X22)
| ~ dirty(X18,X22)
| ~ white(X18,X22)
| ~ chevy(X18,X22)
| placename(X18,X21)
| hollywood_placename(X18,X21)
| ~ city(X18,X20)
| ~ of(X18,X21,X20)
| frontseat(X18,X23)
| group(X18,X19)
| ~ sP20(X26,X25,X24,X23,X22,X21,X20,X19,X18) ) ).
cnf(u1187,negated_conjecture,
fellow(sK1,sK36(sK1,sK17,sK18)) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NLP165+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 18:14:49 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.39 % (2645123)Will run a generic schedule for satisfiability detection.
% 0.07/0.39 % (2645129)% WARNING: option uhcvi not known.
% 0.07/0.39 % (2645128)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=552120842_2999 on theBenchmark for (2999ds/0Mi)
% 0.07/0.39 % (2645134)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2283165234:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.07/0.39 % (2645130)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=507804348:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.07/0.39 % (2645131)dis+10_1_sil=32000:sp=arity:random_seed=3727404709:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.07/0.39 % (2645132)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3355786884:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.07/0.39 % (2645129)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4179533998:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.07/0.39 % (2645133)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3418290744:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.07/0.39 % TRYING [1]
% 0.07/0.39 % TRYING [2]
% 0.07/0.39 % (2645129) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2645123-2645129"...
% 0.07/0.39 % (2645129)...printing done.
% 0.07/0.39 % SZS status CounterSatisfiable for theBenchmark
% 0.07/0.39 % SZS output start Saturation.
% See solution above
% 0.07/0.39 % SZS output start Definitions and Model Updates.
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "sP26"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "black"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "coat"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "wear"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "patient"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "be"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "member"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "in"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "down"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "barrel"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "event"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "lonely"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "placename"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "hollywood_placename"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "frontseat"
% 0.07/0.39 globally flip the polarity of every occurrence of predicate "group"
% 0.07/0.39 % SZS output end Definitions and Model Updates.
% 0.07/0.39 % (2645129)------------------------------
% 0.07/0.39 % (2645129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.39 % (2645129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.39 % (2645129)CaDiCaL version: 2.1.3
% 0.07/0.39 % (2645129)Termination reason: Satisfiable
% 0.07/0.39 % (2645129)Time elapsed: 0.024 s
% 0.07/0.39 % (2645129)Peak memory usage: 13 MB
% 0.07/0.39 % (2645129)Instructions burned: 75 (million)
% 0.07/0.39 % (2645123)Success in time 0.053 s
% 0.07/0.39 % Vampire exiting
%------------------------------------------------------------------------------