↑ Up

E-SAT---3.5.1.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : E-SAT---3.5.1
% Problem  : NLP199+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n015.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 01:38:02 PM UTC 2026

% Result   : CounterSatisfiable 8.31s 2.07s
% Output   : Saturation 8.31s
% Verified : 
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_6ERROR: Could not build tree for root c_0_8ERROR: MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(c_0_7,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_8,plain,
    ( epred2_0
    | behind(esk21_0,esk32_0,esk24_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_9,plain,
    ( epred2_0
    | actual_world(esk21_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_10,plain,
    ( epred2_0
    | frontseat(esk21_0,esk24_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_11,plain,
    ( epred2_0
    | wheel(esk21_0,esk24_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_13,plain,
    ( epred2_0
    | down(esk21_0,esk28_0,esk27_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_14,plain,
    ( epred2_0
    | city(esk21_0,esk27_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_15,plain,
    ( epred2_0
    | street(esk21_0,esk27_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_16,plain,
    ( epred2_0
    | lonely(esk21_0,esk27_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_17,plain,
    ( epred2_0
    | event(esk21_0,esk28_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_18,plain,
    ( epred2_0
    | present(esk21_0,esk28_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_19,plain,
    ( epred2_0
    | barrel(esk21_0,esk28_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_20,plain,
    ( epred2_0
    | in(esk21_0,esk28_0,esk27_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_21,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_23,plain,
    ( epred2_0
    | two(esk21_0,esk29_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_24,plain,
    ( epred2_0
    | group(esk21_0,esk29_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_27,plain,
    ( epred2_0
    | placename(esk21_0,esk26_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_28,plain,
    ( epred2_0
    | of(esk21_0,esk26_0,esk27_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_29,plain,
    ( epred2_0
    | hollywood_placename(esk21_0,esk26_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_32,plain,
    ( epred2_0
    | old(esk21_0,esk25_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_33,plain,
    ( epred2_0
    | chevy(esk21_0,esk25_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_34,plain,
    ( epred2_0
    | white(esk21_0,esk25_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_35,plain,
    ( epred2_0
    | dirty(esk21_0,esk25_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_36,plain,
    ( epred2_0
    | agent(esk21_0,esk28_0,esk25_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_38,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | epred1_0
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_40,plain,
    ( epred2_0
    | forename(esk21_0,esk23_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_41,plain,
    ( epred2_0
    | jules_forename(esk21_0,esk23_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_45,plain,
    ( epred2_0
    | man(esk21_0,esk22_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_46,plain,
    ( epred2_0
    | of(esk21_0,esk23_0,esk22_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_48,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | epred1_0
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_51,plain,
    ( epred2_0
    | be(esk21_0,esk31_0,esk22_0,esk32_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_52,plain,
    ( epred2_0
    | state(esk21_0,esk31_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_57,plain,
    ( epred2_0
    | group(esk21_0,esk30_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_61,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | ~ member(esk21_0,X2,esk29_0)
    | epred2_0
    | patient(esk21_0,esk35_2(X1,X2),X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_64,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | ~ member(esk21_0,X2,esk29_0)
    | epred2_0
    | event(esk21_0,esk35_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_65,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | ~ member(esk21_0,X2,esk29_0)
    | epred2_0
    | agent(esk21_0,esk35_2(X1,X2),X2) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_66,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | ~ member(esk21_0,X2,esk29_0)
    | epred2_0
    | present(esk21_0,esk35_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_67,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | ~ member(esk21_0,X2,esk29_0)
    | epred2_0
    | nonreflexive(esk21_0,esk35_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_68,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | ~ member(esk21_0,X2,esk29_0)
    | epred2_0
    | wear(esk21_0,esk35_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_80,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_89,plain,
    ( ~ member(esk21_0,X1,esk29_0)
    | epred2_0
    | be(esk21_0,esk33_1(X1),X1,esk34_1(X1)) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_91,plain,
    ( ~ member(esk21_0,X1,esk29_0)
    | epred2_0
    | in(esk21_0,esk34_1(X1),esk24_0) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_92,plain,
    ( ~ member(esk21_0,X1,esk29_0)
    | epred2_0
    | state(esk21_0,esk33_1(X1)) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_108,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred1_0
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_116,plain,
    ( ~ member(esk21_0,X1,esk29_0)
    | epred2_0
    | young(esk21_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_118,plain,
    ( ~ member(esk21_0,X1,esk29_0)
    | epred2_0
    | fellow(esk21_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_119,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_123,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_131,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_138,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_144,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_154,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred1_0
    | member(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_162,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | epred2_0
    | cheap(esk21_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_164,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | epred2_0
    | coat(esk21_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_165,plain,
    ( ~ member(esk21_0,X1,esk30_0)
    | epred2_0
    | black(esk21_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_166,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_171,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_179,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_186,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_192,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_202,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_210,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_215,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_225,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_226,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_235,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0
    | member(X1,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_241,plain,
    ( epred1_0
    | behind(esk1_0,esk12_0,esk12_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_242,plain,
    ( epred1_0
    | actual_world(esk1_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_243,plain,
    ( epred1_0
    | wheel(esk1_0,esk12_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_246,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,X5)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ city(esk1_0,X5)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ street(esk1_0,X5)
    | ~ lonely(esk1_0,X5)
    | ~ event(esk1_0,X6)
    | ~ agent(esk1_0,X6,X3)
    | ~ present(esk1_0,X6)
    | ~ barrel(esk1_0,X6)
    | ~ down(esk1_0,X6,X5)
    | ~ in(esk1_0,X6,X5)
    | ~ in(esk1_0,X11,esk12_0)
    | ~ state(esk1_0,X9)
    | ~ state(esk1_0,X10)
    | ~ be(esk1_0,X9,X1,esk12_0)
    | ~ be(esk1_0,X10,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X11)
    | ~ two(esk1_0,X7)
    | ~ group(esk1_0,X7)
    | ~ group(esk1_0,X8)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X8)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_241]),c_0_242]),c_0_243]),
    [final] ).

cnf(c_0_247,plain,
    ( epred1_0
    | down(esk1_0,esk8_0,esk7_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_248,plain,
    ( epred1_0
    | city(esk1_0,esk7_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_249,plain,
    ( epred1_0
    | street(esk1_0,esk7_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_250,plain,
    ( epred1_0
    | lonely(esk1_0,esk7_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_251,plain,
    ( epred1_0
    | event(esk1_0,esk8_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_252,plain,
    ( epred1_0
    | present(esk1_0,esk8_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_253,plain,
    ( epred1_0
    | barrel(esk1_0,esk8_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_254,plain,
    ( epred1_0
    | in(esk1_0,esk8_0,esk7_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_255,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,X5)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ city(esk1_0,X5)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ street(esk1_0,X5)
    | ~ lonely(esk1_0,X5)
    | ~ event(esk1_0,X6)
    | ~ agent(esk1_0,X6,X3)
    | ~ present(esk1_0,X6)
    | ~ barrel(esk1_0,X6)
    | ~ down(esk1_0,X6,X5)
    | ~ in(esk1_0,X6,X5)
    | ~ in(esk1_0,X11,esk12_0)
    | ~ state(esk1_0,X9)
    | ~ state(esk1_0,X10)
    | ~ be(esk1_0,X9,X1,esk12_0)
    | ~ be(esk1_0,X10,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X11)
    | ~ two(esk1_0,X7)
    | ~ group(esk1_0,X7)
    | ~ group(esk1_0,X8)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X8)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X8)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_241]),c_0_242]),c_0_243]),
    [final] ).

cnf(c_0_256,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,X5)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ city(esk1_0,X5)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ street(esk1_0,X5)
    | ~ lonely(esk1_0,X5)
    | ~ event(esk1_0,X6)
    | ~ agent(esk1_0,X6,X3)
    | ~ present(esk1_0,X6)
    | ~ barrel(esk1_0,X6)
    | ~ down(esk1_0,X6,X5)
    | ~ in(esk1_0,X6,X5)
    | ~ state(esk1_0,X9)
    | ~ be(esk1_0,X9,X1,esk12_0)
    | ~ two(esk1_0,X7)
    | ~ group(esk1_0,X7)
    | ~ group(esk1_0,X8)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X8)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_7,c_0_241]),c_0_242]),c_0_243]),
    [final] ).

cnf(c_0_257,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,X5)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ city(esk1_0,X5)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ street(esk1_0,X5)
    | ~ lonely(esk1_0,X5)
    | ~ event(esk1_0,X6)
    | ~ agent(esk1_0,X6,X3)
    | ~ present(esk1_0,X6)
    | ~ barrel(esk1_0,X6)
    | ~ down(esk1_0,X6,X5)
    | ~ in(esk1_0,X6,X5)
    | ~ state(esk1_0,X9)
    | ~ be(esk1_0,X9,X1,esk12_0)
    | ~ two(esk1_0,X7)
    | ~ group(esk1_0,X7)
    | ~ group(esk1_0,X8)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X7)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X8)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,X5,X6,X7,X8,X9,esk12_0),X8)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_21,c_0_241]),c_0_242]),c_0_243]),
    [final] ).

cnf(c_0_265,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ in(esk1_0,X9,esk12_0)
    | ~ state(esk1_0,X7)
    | ~ state(esk1_0,X8)
    | ~ be(esk1_0,X7,X1,esk12_0)
    | ~ be(esk1_0,X8,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X9)
    | ~ two(esk1_0,X5)
    | ~ group(esk1_0,X5)
    | ~ group(esk1_0,X6)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X6)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_246,c_0_247]),c_0_248]),c_0_249]),c_0_250]),c_0_251]),c_0_252]),c_0_253]),c_0_254]),
    [final] ).

cnf(c_0_266,plain,
    ( epred1_0
    | two(esk1_0,esk9_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_267,plain,
    ( epred1_0
    | group(esk1_0,esk9_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_268,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ in(esk1_0,X9,esk12_0)
    | ~ state(esk1_0,X7)
    | ~ state(esk1_0,X8)
    | ~ be(esk1_0,X7,X1,esk12_0)
    | ~ be(esk1_0,X8,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X9)
    | ~ two(esk1_0,X5)
    | ~ group(esk1_0,X5)
    | ~ group(esk1_0,X6)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X6)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X6)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_255,c_0_247]),c_0_248]),c_0_249]),c_0_250]),c_0_251]),c_0_252]),c_0_253]),c_0_254]),
    [final] ).

cnf(c_0_269,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ state(esk1_0,X7)
    | ~ be(esk1_0,X7,X1,esk12_0)
    | ~ two(esk1_0,X5)
    | ~ group(esk1_0,X5)
    | ~ group(esk1_0,X6)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X6)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_256,c_0_247]),c_0_248]),c_0_249]),c_0_250]),c_0_251]),c_0_252]),c_0_253]),c_0_254]),
    [final] ).

cnf(c_0_270,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ state(esk1_0,X7)
    | ~ be(esk1_0,X7,X1,esk12_0)
    | ~ two(esk1_0,X5)
    | ~ group(esk1_0,X5)
    | ~ group(esk1_0,X6)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X6)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X6)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,X5,X6,X7,esk12_0),X5)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_257,c_0_247]),c_0_248]),c_0_249]),c_0_250]),c_0_251]),c_0_252]),c_0_253]),c_0_254]),
    [final] ).

cnf(c_0_272,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X4)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ wheel(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk16_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ young(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk17_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk18_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk19_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk20_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred1_0 ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_279,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ in(esk1_0,X8,esk12_0)
    | ~ state(esk1_0,X6)
    | ~ state(esk1_0,X7)
    | ~ be(esk1_0,X6,X1,esk12_0)
    | ~ be(esk1_0,X7,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X8)
    | ~ group(esk1_0,X5)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X5)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_265,c_0_266]),c_0_267]),
    [final] ).

cnf(c_0_280,plain,
    ( epred1_0
    | placename(esk1_0,esk6_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_281,plain,
    ( epred1_0
    | of(esk1_0,esk6_0,esk7_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_282,plain,
    ( epred1_0
    | hollywood_placename(esk1_0,esk6_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_283,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ in(esk1_0,X8,esk12_0)
    | ~ state(esk1_0,X6)
    | ~ state(esk1_0,X7)
    | ~ be(esk1_0,X6,X1,esk12_0)
    | ~ be(esk1_0,X7,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X8)
    | ~ group(esk1_0,X5)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X5)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X5)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_268,c_0_266]),c_0_267]),
    [final] ).

cnf(c_0_284,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ state(esk1_0,X6)
    | ~ be(esk1_0,X6,X1,esk12_0)
    | ~ group(esk1_0,X5)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X5)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_269,c_0_266]),c_0_267]),
    [final] ).

cnf(c_0_285,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ of(esk1_0,X4,esk7_0)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ hollywood_placename(esk1_0,X4)
    | ~ placename(esk1_0,X4)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ state(esk1_0,X6)
    | ~ be(esk1_0,X6,X1,esk12_0)
    | ~ group(esk1_0,X5)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X5)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),X5)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,X4,esk7_0,esk8_0,esk9_0,X5,X6,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_270,c_0_266]),c_0_267]),
    [final] ).

cnf(c_0_288,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ in(esk1_0,X7,esk12_0)
    | ~ state(esk1_0,X5)
    | ~ state(esk1_0,X6)
    | ~ be(esk1_0,X5,X1,esk12_0)
    | ~ be(esk1_0,X6,esk16_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X7)
    | ~ group(esk1_0,X4)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X4)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_279,c_0_280]),c_0_281]),c_0_282]),
    [final] ).

cnf(c_0_289,plain,
    ( epred1_0
    | old(esk1_0,esk5_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_290,plain,
    ( epred1_0
    | chevy(esk1_0,esk5_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_291,plain,
    ( epred1_0
    | white(esk1_0,esk5_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_292,plain,
    ( epred1_0
    | dirty(esk1_0,esk5_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_293,plain,
    ( epred1_0
    | agent(esk1_0,esk8_0,esk5_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_294,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ in(esk1_0,X7,esk12_0)
    | ~ state(esk1_0,X5)
    | ~ state(esk1_0,X6)
    | ~ be(esk1_0,X5,X1,esk12_0)
    | ~ be(esk1_0,X6,esk16_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X7)
    | ~ group(esk1_0,X4)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X4)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X4)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_283,c_0_280]),c_0_281]),c_0_282]),
    [final] ).

cnf(c_0_295,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ state(esk1_0,X5)
    | ~ be(esk1_0,X5,X1,esk12_0)
    | ~ group(esk1_0,X4)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X4)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_284,c_0_280]),c_0_281]),c_0_282]),
    [final] ).

cnf(c_0_296,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ chevy(esk1_0,X3)
    | ~ white(esk1_0,X3)
    | ~ dirty(esk1_0,X3)
    | ~ old(esk1_0,X3)
    | ~ agent(esk1_0,esk8_0,X3)
    | ~ state(esk1_0,X5)
    | ~ be(esk1_0,X5,X1,esk12_0)
    | ~ group(esk1_0,X4)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X4)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),X4)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,X3,esk6_0,esk7_0,esk8_0,esk9_0,X4,X5,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_285,c_0_280]),c_0_281]),c_0_282]),
    [final] ).

cnf(c_0_298,plain,
    ( epred1_0
    | epred2_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_287,c_0_237]),c_0_238]),c_0_239]),
    [final] ).

cnf(c_0_299,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred2_0
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_300,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_301,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_302,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_303,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_304,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_305,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_306,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_307,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_308,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_309,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_310,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | epred2_0
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_311,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_312,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ in(esk1_0,X6,esk12_0)
    | ~ state(esk1_0,X4)
    | ~ state(esk1_0,X5)
    | ~ be(esk1_0,X4,X1,esk12_0)
    | ~ be(esk1_0,X5,esk16_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X6)
    | ~ group(esk1_0,X3)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X3)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_288,c_0_289]),c_0_290]),c_0_291]),c_0_292]),c_0_293]),
    [final] ).

cnf(c_0_313,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_314,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_315,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_316,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_317,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ in(esk1_0,X6,esk12_0)
    | ~ state(esk1_0,X4)
    | ~ state(esk1_0,X5)
    | ~ be(esk1_0,X4,X1,esk12_0)
    | ~ be(esk1_0,X5,esk16_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X6)
    | ~ group(esk1_0,X3)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X3)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X3)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_294,c_0_289]),c_0_290]),c_0_291]),c_0_292]),c_0_293]),
    [final] ).

cnf(c_0_318,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_319,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X15,X4)
    | ~ be(X1,X14,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X15)
    | ~ state(X1,X14)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ wear(X1,X13)
    | ~ nonreflexive(X1,X13)
    | ~ present(X1,X13)
    | ~ patient(X1,X13,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ agent(X1,X13,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ event(X1,X13)
    | ~ cheap(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ black(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ coat(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0 ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_320,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ state(esk1_0,X4)
    | ~ be(esk1_0,X4,X1,esk12_0)
    | ~ group(esk1_0,X3)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X3)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | member(esk1_0,esk19_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_295,c_0_289]),c_0_290]),c_0_291]),c_0_292]),c_0_293]),
    [final] ).

cnf(c_0_321,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | epred2_0
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_322,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | epred2_0
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_323,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk39_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_324,plain,
    ( ~ of(esk1_0,X2,X1)
    | ~ man(esk1_0,X1)
    | ~ jules_forename(esk1_0,X2)
    | ~ forename(esk1_0,X2)
    | ~ frontseat(esk1_0,esk12_0)
    | ~ state(esk1_0,X4)
    | ~ be(esk1_0,X4,X1,esk12_0)
    | ~ group(esk1_0,X3)
    | member(esk1_0,esk18_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X3)
    | member(esk1_0,esk20_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),X3)
    | member(esk1_0,esk16_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | member(esk1_0,esk17_12(esk1_0,X1,X2,esk12_0,esk5_0,esk6_0,esk7_0,esk8_0,esk9_0,X3,X4,esk12_0),esk9_0)
    | epred1_0 ),
    inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_296,c_0_289]),c_0_290]),c_0_291]),c_0_292]),c_0_293]),
    [final] ).

cnf(c_0_325,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | epred2_0
    | member(X1,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X9)
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_326,plain,
    ( ~ actual_world(X1)
    | ~ behind(X1,X12,X12)
    | ~ be(X1,X11,X2,X12)
    | ~ state(X1,X11)
    | ~ wheel(X1,X12)
    | ~ group(X1,X10)
    | ~ group(X1,X9)
    | ~ two(X1,X9)
    | ~ in(X1,X8,X7)
    | ~ down(X1,X8,X7)
    | ~ barrel(X1,X8)
    | ~ present(X1,X8)
    | ~ agent(X1,X8,X5)
    | ~ event(X1,X8)
    | ~ lonely(X1,X7)
    | ~ street(X1,X7)
    | ~ placename(X1,X6)
    | ~ hollywood_placename(X1,X6)
    | ~ city(X1,X7)
    | ~ of(X1,X6,X7)
    | ~ old(X1,X5)
    | ~ dirty(X1,X5)
    | ~ white(X1,X5)
    | ~ chevy(X1,X5)
    | ~ frontseat(X1,X4)
    | ~ forename(X1,X3)
    | ~ jules_forename(X1,X3)
    | ~ man(X1,X2)
    | ~ of(X1,X3,X2)
    | ~ in(X1,X14,X4)
    | ~ be(X1,X13,esk36_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X14)
    | ~ state(X1,X13)
    | ~ young(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | ~ fellow(X1,esk37_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12))
    | epred2_0
    | member(X1,esk38_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10)
    | member(X1,esk40_12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12),X10) ),
    inference(split_conjunct,[status(thm)],[c_0_6]),
    [final] ).

cnf(c_0_327,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | ~ member(esk1_0,X2,esk9_0)
    | epred1_0
    | patient(esk1_0,esk15_2(X1,X2),X1) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_328,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | ~ member(esk1_0,X2,esk9_0)
    | epred1_0
    | agent(esk1_0,esk15_2(X1,X2),X2) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_329,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | ~ member(esk1_0,X2,esk9_0)
    | epred1_0
    | wear(esk1_0,esk15_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_330,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | ~ member(esk1_0,X2,esk9_0)
    | epred1_0
    | nonreflexive(esk1_0,esk15_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_331,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | ~ member(esk1_0,X2,esk9_0)
    | epred1_0
    | present(esk1_0,esk15_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_332,plain,
    ( ~ member(esk1_0,X1,esk9_0)
    | epred1_0
    | be(esk1_0,esk13_1(X1),X1,esk14_1(X1)) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_333,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | ~ member(esk1_0,X2,esk9_0)
    | epred1_0
    | event(esk1_0,esk15_2(X1,X2)) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_334,plain,
    ( ~ member(esk1_0,X1,esk9_0)
    | epred1_0
    | in(esk1_0,esk14_1(X1),esk4_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_335,plain,
    ( ~ member(esk1_0,X1,esk9_0)
    | epred1_0
    | state(esk1_0,esk13_1(X1)) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_336,plain,
    ( epred1_0
    | be(esk1_0,esk11_0,esk2_0,esk12_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_337,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | epred1_0
    | cheap(esk1_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_338,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | epred1_0
    | black(esk1_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_339,plain,
    ( ~ member(esk1_0,X1,esk10_0)
    | epred1_0
    | coat(esk1_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_340,plain,
    ( ~ member(esk1_0,X1,esk9_0)
    | epred1_0
    | young(esk1_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_341,plain,
    ( ~ member(esk1_0,X1,esk9_0)
    | epred1_0
    | fellow(esk1_0,X1) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_342,plain,
    ( epred1_0
    | of(esk1_0,esk3_0,esk2_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_343,plain,
    ( epred1_0
    | group(esk1_0,esk10_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_344,plain,
    ( epred1_0
    | state(esk1_0,esk11_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_345,plain,
    ( epred1_0
    | frontseat(esk1_0,esk4_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_346,plain,
    ( epred1_0
    | forename(esk1_0,esk3_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_347,plain,
    ( epred1_0
    | jules_forename(esk1_0,esk3_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_348,plain,
    ( epred1_0
    | man(esk1_0,esk2_0) ),
    inference(split_conjunct,[status(thm)],[c_0_5]),
    [final] ).

cnf(c_0_349,negated_conjecture,
    ( ~ epred2_0
    | ~ epred1_0 ),
    inference(split_conjunct,[status(thm)],[c_0_297]),
    [final] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP199+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06  % Command  : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.44  % Computer : n015.cluster.edu
% 0.17/0.44  % Model    : x86_64 x86_64
% 0.17/0.44  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44  % Memory   : 8046.5625MB
% 0.17/0.44  % OS       : Linux 6.8.0-71-generic
% 0.17/0.44  % CPULimit : 300
% 0.17/0.44  % WCLimit  : 300
% 0.17/0.44  % DateTime : Mon Sep 21 01:51:36 UTC 2026
% 0.17/0.45  % CPUTime  : 
% 0.17/0.45  Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.52  Running first-order theorem proving
% 0.26/0.52  Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.31/2.07  % Version: 3.5.1
% 8.31/2.07  % Preprocessing class: FSLSSMSSSSSNFFN.
% 8.31/2.07  % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 8.31/2.07  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 8.31/2.07  % Starting new_bool_3 with 300s (1) cores
% 8.31/2.07  % Starting new_bool_1 with 300s (1) cores
% 8.31/2.07  % Starting sh5l with 300s (1) cores
% 8.31/2.07  % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 302692 completed with status 1
% 8.31/2.07  % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 8.31/2.07  % Preprocessing class: FSLSSMSSSSSNFFN.
% 8.31/2.07  % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 8.31/2.07  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 8.31/2.07  % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 8.31/2.07  % No SInE strategy applied
% 8.31/2.07  % Search class: FGHNF-FSLM33-SFFFFFNN
% 8.31/2.07  % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 8.31/2.07  % Starting SubtermCWHack with 136s (1) cores
% 8.31/2.07  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 8.31/2.07  % Starting G-E--_107_C41_F1_PI_AE_Q4_CS_SP_PS_S4S with 136s (1) cores
% 8.31/2.07  % Starting new_bool_3 with 136s (1) cores
% 8.31/2.07  % Starting H----_042_B03_F1_AE_Q4_SP_S2S with 136s (1) cores
% 8.31/2.07  % new_bool_3 with pid 302699 completed with status 1
% 8.31/2.07  % Result found by new_bool_3
% 8.31/2.07  % Preprocessing class: FSLSSMSSSSSNFFN.
% 8.31/2.07  % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 8.31/2.07  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 8.31/2.07  % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 8.31/2.07  % No SInE strategy applied
% 8.31/2.07  % Search class: FGHNF-FSLM33-SFFFFFNN
% 8.31/2.07  % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 8.31/2.07  % Starting SubtermCWHack with 136s (1) cores
% 8.31/2.07  % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 8.31/2.07  % Starting G-E--_107_C41_F1_PI_AE_Q4_CS_SP_PS_S4S with 136s (1) cores
% 8.31/2.07  % Starting new_bool_3 with 136s (1) cores
% 8.31/2.07  % Preprocessing time       : 0.011 s
% 8.31/2.07  % Presaturation interreduction done
% 8.31/2.07  
% 8.31/2.07  % No proof found!
% 8.31/2.07  % SZS status CounterSatisfiable
% 8.31/2.07  % SZS output start Saturation
% See solution above
% 8.31/2.07  % Parsed axioms                        : 1
% 8.31/2.07  % Removed by relevancy pruning/SinE    : 0
% 8.31/2.07  % Initial clauses                      : 135
% 8.31/2.07  % Removed in clause preprocessing      : 0
% 8.31/2.07  % Initial clauses in saturation        : 135
% 8.31/2.07  % Processed clauses                    : 1375
% 8.31/2.07  % ...of these trivial                  : 0
% 8.31/2.07  % ...subsumed                          : 96
% 8.31/2.07  % ...remaining for further processing  : 1279
% 8.31/2.07  % Other redundant clauses eliminated   : 0
% 8.31/2.07  % Clauses deleted for lack of memory   : 0
% 8.31/2.07  % Backward-subsumed                    : 988
% 8.31/2.07  % Backward-rewritten                   : 0
% 8.31/2.07  % Generated clauses                    : 1471
% 8.31/2.07  % ...of the previous two non-redundant : 1470
% 8.31/2.07  % ...aggressively subsumed             : 0
% 8.31/2.07  % Contextual simplify-reflections      : 2045
% 8.31/2.07  % Paramodulations                      : 1471
% 8.31/2.07  % Factorizations                       : 0
% 8.31/2.07  % NegExts                              : 0
% 8.31/2.07  % Equation resolutions                 : 0
% 8.31/2.07  % Disequality decompositions           : 0
% 8.31/2.07  % Total rewrite steps                  : 0
% 8.31/2.07  % ...of those cached                   : 0
% 8.31/2.07  % Propositional unsat checks           : 0
% 8.31/2.07  %    Propositional check models        : 0
% 8.31/2.07  %    Propositional check unsatisfiable : 0
% 8.31/2.07  %    Propositional clauses             : 0
% 8.31/2.07  %    Propositional clauses after purity: 0
% 8.31/2.07  %    Propositional unsat core size     : 0
% 8.31/2.07  %    Propositional preprocessing time  : 0.000
% 8.31/2.07  %    Propositional encoding time       : 0.000
% 8.31/2.07  %    Propositional solver time         : 0.000
% 8.31/2.07  %    Success case prop preproc time    : 0.000
% 8.31/2.07  %    Success case prop encoding time   : 0.000
% 8.31/2.07  %    Success case prop solver time     : 0.000
% 8.31/2.07  % Current number of processed clauses  : 156
% 8.31/2.07  %    Positive orientable unit clauses  : 0
% 8.31/2.07  %    Positive unorientable unit clauses: 0
% 8.31/2.07  %    Negative unit clauses             : 0
% 8.31/2.07  %    Non-unit-clauses                  : 156
% 8.31/2.07  % Current number of unprocessed clauses: 0
% 8.31/2.07  % ...number of literals in the above   : 0
% 8.31/2.07  % Current number of archived formulas  : 0
% 8.31/2.07  % Current number of archived clauses   : 1123
% 8.31/2.07  % Clause-clause subsumption calls (NU) : 1119648
% 8.31/2.07  % Rec. Clause-clause subsumption calls : 23962
% 8.31/2.07  % Non-unit clause-clause subsumptions  : 3129
% 8.31/2.07  % Unit Clause-clause subsumption calls : 0
% 8.31/2.07  % Rewrite failures with RHS unbound    : 0
% 8.31/2.07  % BW rewrite match attempts            : 0
% 8.31/2.07  % BW rewrite match successes           : 0
% 8.31/2.07  % Condensation attempts                : 0
% 8.31/2.07  % Condensation successes               : 0
% 8.31/2.07  % Termbank termtop insertions          : 287677
% 8.31/2.07  % Search garbage collected termcells   : 3944
% 8.31/2.07  
% 8.31/2.07  % -------------------------------------------------
% 8.31/2.07  % User time                : 1.213 s
% 8.31/2.07  % System time              : 0.015 s
% 8.31/2.07  % Total time               : 1.227 s
% 8.31/2.07  % Maximum resident set size: 4456 pages
% 8.31/2.07  
% 8.31/2.07  % -------------------------------------------------
% 8.31/2.07  % User time                : 5.553 s
% 8.31/2.07  % System time              : 0.063 s
% 8.31/2.07  % Total time               : 5.616 s
% 8.31/2.07  % Maximum resident set size: 5120 pages
% 8.31/2.07  % E exiting
%------------------------------------------------------------------------------