%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP133-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:34:17 EDT 2024
% Result : Satisfiable 6.90s 7.10s
% Output : Saturation 6.90s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause17,negated_conjecture,
( ssSkC0
| ssSkP1(skc43,skc42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause38,negated_conjecture,
( ~ ssSkC0
| in(skc12,skc14,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c310,plain,
( in(skc12,skc14,skc15)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause38,clause17]) ).
cnf(clause42,negated_conjecture,
( ssSkP0(X5,X6)
| member(X6,skf14(X6,X5),X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(clause50,negated_conjecture,
( ~ member(X22,X24,X23)
| ~ ssSkP1(X23,X22)
| in(X22,skf15(X22,X21),skf15(X22,X21)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c374,plain,
( ~ ssSkP1(X91,X92)
| in(X92,skf15(X92,X93),skf15(X92,X93))
| ssSkP0(X91,X92) ),
inference(resolution,[status(thm)],[clause50,clause42]) ).
cnf(c641,plain,
( in(skc42,skf15(skc42,X369),skf15(skc42,X369))
| ssSkP0(skc43,skc42)
| in(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c374,c310]) ).
cnf(clause40,negated_conjecture,
( ~ ssSkC0
| of(skc12,skc16,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c348,plain,
( of(skc12,skc16,skc15)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause40,clause17]) ).
cnf(c639,plain,
( in(skc42,skf15(skc42,X367),skf15(skc42,X367))
| ssSkP0(skc43,skc42)
| of(skc12,skc16,skc15) ),
inference(resolution,[status(thm)],[c374,c348]) ).
cnf(clause58,negated_conjecture,
( ~ city(X56,X55)
| ~ chevy(X56,X55)
| ~ white(X56,X55)
| ~ dirty(X56,X55)
| ~ old(X56,X55)
| ~ agent(X56,X54,X55)
| ~ in(X56,X54,X55)
| ~ placename(X56,X59)
| ~ hollywood_placename(X56,X59)
| ~ of(X56,X59,X55)
| ~ event(X56,X54)
| ~ present(X56,X54)
| ~ barrel(X56,X54)
| ~ down(X56,X54,X57)
| ~ lonely(X56,X57)
| ~ street(X56,X57)
| ~ group(X56,X58)
| ~ two(X56,X58)
| ~ ssSkP1(X58,X56)
| ~ actual_world(X56)
| ~ ssSkC0
| member(X56,skf9(X56,X58),X58) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
cnf(clause39,negated_conjecture,
( ~ ssSkC0
| down(skc12,skc14,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c329,plain,
( down(skc12,skc14,skc15)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause39,clause17]) ).
cnf(c640,plain,
( in(skc42,skf15(skc42,X368),skf15(skc42,X368))
| ssSkP0(skc43,skc42)
| down(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c374,c329]) ).
cnf(c894,plain,
( in(skc42,skf15(skc42,X868),skf15(skc42,X868))
| ssSkP0(skc43,skc42)
| ~ city(skc12,X867)
| ~ chevy(skc12,X867)
| ~ white(skc12,X867)
| ~ dirty(skc12,X867)
| ~ old(skc12,X867)
| ~ agent(skc12,skc14,X867)
| ~ in(skc12,skc14,X867)
| ~ placename(skc12,X869)
| ~ hollywood_placename(skc12,X869)
| ~ of(skc12,X869,X867)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X866)
| ~ two(skc12,X866)
| ~ ssSkP1(X866,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X866),X866) ),
inference(resolution,[status(thm)],[c640,clause58]) ).
cnf(c1661,plain,
( in(skc42,skf15(skc42,X2525),skf15(skc42,X2525))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2524)
| ~ two(skc12,X2524)
| ~ ssSkP1(X2524,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2524),X2524)
| in(skc42,skf15(skc42,X2523),skf15(skc42,X2523)) ),
inference(resolution,[status(thm)],[c894,c639]) ).
cnf(c2370,plain,
( in(skc42,skf15(skc42,X2665),skf15(skc42,X2665))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2664)
| ~ two(skc12,X2664)
| ~ ssSkP1(X2664,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2664),X2664)
| in(skc42,skf15(skc42,X2667),skf15(skc42,X2667))
| in(skc42,skf15(skc42,X2666),skf15(skc42,X2666)) ),
inference(resolution,[status(thm)],[c1661,c641]) ).
cnf(clause52,negated_conjecture,
( ~ member(X29,X31,X30)
| ~ ssSkP1(X30,X29)
| be(X29,skf16(X29,X31),X31,skf15(X29,X31)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c378,plain,
( ~ ssSkP1(X121,X122)
| be(X122,skf16(X122,skf14(X122,X121)),skf14(X122,X121),skf15(X122,skf14(X122,X121)))
| ssSkP0(X121,X122) ),
inference(resolution,[status(thm)],[clause52,clause42]) ).
cnf(c684,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| in(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c378,c310]) ).
cnf(c682,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| of(skc12,skc16,skc15) ),
inference(resolution,[status(thm)],[c378,c348]) ).
cnf(c683,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| down(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c378,c329]) ).
cnf(c1462,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| ~ city(skc12,X2308)
| ~ chevy(skc12,X2308)
| ~ white(skc12,X2308)
| ~ dirty(skc12,X2308)
| ~ old(skc12,X2308)
| ~ agent(skc12,skc14,X2308)
| ~ in(skc12,skc14,X2308)
| ~ placename(skc12,X2309)
| ~ hollywood_placename(skc12,X2309)
| ~ of(skc12,X2309,X2308)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2307)
| ~ two(skc12,X2307)
| ~ ssSkP1(X2307,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2307),X2307) ),
inference(resolution,[status(thm)],[c683,clause58]) ).
cnf(c2207,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2615)
| ~ two(skc12,X2615)
| ~ ssSkP1(X2615,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2615),X2615) ),
inference(resolution,[status(thm)],[c1462,c682]) ).
cnf(c2392,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2616)
| ~ two(skc12,X2616)
| ~ ssSkP1(X2616,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2616),X2616) ),
inference(resolution,[status(thm)],[c2207,c684]) ).
cnf(clause49,negated_conjecture,
( ~ member(X18,X20,X19)
| ~ ssSkP1(X19,X18)
| frontseat(X18,skf15(X18,X17)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c372,plain,
( ~ ssSkP1(X83,X84)
| frontseat(X84,skf15(X84,X85))
| ssSkP0(X83,X84) ),
inference(resolution,[status(thm)],[clause49,clause42]) ).
cnf(c487,plain,
( frontseat(skc42,skf15(skc42,X257))
| ssSkP0(skc43,skc42)
| down(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c372,c329]) ).
cnf(c841,plain,
( frontseat(skc42,skf15(skc42,X793))
| ssSkP0(skc43,skc42)
| ~ city(skc12,X792)
| ~ chevy(skc12,X792)
| ~ white(skc12,X792)
| ~ dirty(skc12,X792)
| ~ old(skc12,X792)
| ~ agent(skc12,skc14,X792)
| ~ in(skc12,skc14,X792)
| ~ placename(skc12,X790)
| ~ hollywood_placename(skc12,X790)
| ~ of(skc12,X790,X792)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X791)
| ~ two(skc12,X791)
| ~ ssSkP1(X791,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X791),X791) ),
inference(resolution,[status(thm)],[c487,clause58]) ).
cnf(c1511,plain,
( frontseat(skc42,skf15(skc42,X2373))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2375)
| ~ two(skc12,X2375)
| ~ ssSkP1(X2375,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2375),X2375)
| in(skc42,skf15(skc42,X2374),skf15(skc42,X2374)) ),
inference(resolution,[status(thm)],[c841,c639]) ).
cnf(c2320,plain,
( frontseat(skc42,skf15(skc42,X2602))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2601)
| ~ two(skc12,X2601)
| ~ ssSkP1(X2601,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2601),X2601)
| in(skc42,skf15(skc42,X2600),skf15(skc42,X2600))
| in(skc42,skf15(skc42,X2603),skf15(skc42,X2603)) ),
inference(resolution,[status(thm)],[c1511,c641]) ).
cnf(clause48,negated_conjecture,
( ~ member(X14,X16,X15)
| ~ ssSkP1(X15,X14)
| state(X14,skf16(X14,X13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(c370,plain,
( ~ ssSkP1(X77,X78)
| state(X78,skf16(X78,X79))
| ssSkP0(X77,X78) ),
inference(resolution,[status(thm)],[clause48,clause42]) ).
cnf(c466,plain,
( state(skc42,skf16(skc42,X250))
| ssSkP0(skc43,skc42)
| down(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c370,c329]) ).
cnf(c839,plain,
( state(skc42,skf16(skc42,X776))
| ssSkP0(skc43,skc42)
| ~ city(skc12,X777)
| ~ chevy(skc12,X777)
| ~ white(skc12,X777)
| ~ dirty(skc12,X777)
| ~ old(skc12,X777)
| ~ agent(skc12,skc14,X777)
| ~ in(skc12,skc14,X777)
| ~ placename(skc12,X779)
| ~ hollywood_placename(skc12,X779)
| ~ of(skc12,X779,X777)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X778)
| ~ two(skc12,X778)
| ~ ssSkP1(X778,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X778),X778) ),
inference(resolution,[status(thm)],[c466,clause58]) ).
cnf(c1486,plain,
( state(skc42,skf16(skc42,X2338))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2339)
| ~ two(skc12,X2339)
| ~ ssSkP1(X2339,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2339),X2339)
| in(skc42,skf15(skc42,X2340),skf15(skc42,X2340)) ),
inference(resolution,[status(thm)],[c839,c639]) ).
cnf(c2270,plain,
( state(skc42,skf16(skc42,X2596))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2599)
| ~ two(skc12,X2599)
| ~ ssSkP1(X2599,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2599),X2599)
| in(skc42,skf15(skc42,X2597),skf15(skc42,X2597))
| in(skc42,skf15(skc42,X2598),skf15(skc42,X2598)) ),
inference(resolution,[status(thm)],[c1486,c641]) ).
cnf(c486,plain,
( frontseat(skc42,skf15(skc42,X256))
| ssSkP0(skc43,skc42)
| of(skc12,skc16,skc15) ),
inference(resolution,[status(thm)],[c372,c348]) ).
cnf(c1524,plain,
( frontseat(skc42,skf15(skc42,X2132))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2134)
| ~ two(skc12,X2134)
| ~ ssSkP1(X2134,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2134),X2134)
| frontseat(skc42,skf15(skc42,X2133)) ),
inference(resolution,[status(thm)],[c841,c486]) ).
cnf(c2195,plain,
( frontseat(skc42,skf15(skc42,X2489))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2492)
| ~ two(skc12,X2492)
| ~ ssSkP1(X2492,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2492),X2492)
| frontseat(skc42,skf15(skc42,X2491))
| in(skc42,skf15(skc42,X2490),skf15(skc42,X2490)) ),
inference(resolution,[status(thm)],[c1524,c641]) ).
cnf(c1499,plain,
( state(skc42,skf16(skc42,X2078))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2079)
| ~ two(skc12,X2079)
| ~ ssSkP1(X2079,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2079),X2079)
| frontseat(skc42,skf15(skc42,X2080)) ),
inference(resolution,[status(thm)],[c839,c486]) ).
cnf(c2170,plain,
( state(skc42,skf16(skc42,X2484))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2485)
| ~ two(skc12,X2485)
| ~ ssSkP1(X2485,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2485),X2485)
| frontseat(skc42,skf15(skc42,X2487))
| in(skc42,skf15(skc42,X2486),skf15(skc42,X2486)) ),
inference(resolution,[status(thm)],[c1499,c641]) ).
cnf(c465,plain,
( state(skc42,skf16(skc42,X249))
| ssSkP0(skc43,skc42)
| of(skc12,skc16,skc15) ),
inference(resolution,[status(thm)],[c370,c348]) ).
cnf(c1476,plain,
( state(skc42,skf16(skc42,X2027))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2028)
| ~ two(skc12,X2028)
| ~ ssSkP1(X2028,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2028),X2028)
| state(skc42,skf16(skc42,X2029)) ),
inference(resolution,[status(thm)],[c839,c465]) ).
cnf(c2145,plain,
( state(skc42,skf16(skc42,X2481))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2483)
| ~ two(skc12,X2483)
| ~ ssSkP1(X2483,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2483),X2483)
| state(skc42,skf16(skc42,X2482))
| in(skc42,skf15(skc42,X2480),skf15(skc42,X2480)) ),
inference(resolution,[status(thm)],[c1476,c641]) ).
cnf(c488,plain,
( frontseat(skc42,skf15(skc42,X258))
| ssSkP0(skc43,skc42)
| in(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c372,c310]) ).
cnf(c2188,plain,
( frontseat(skc42,skf15(skc42,X2266))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2269)
| ~ two(skc12,X2269)
| ~ ssSkP1(X2269,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2269),X2269)
| frontseat(skc42,skf15(skc42,X2268))
| frontseat(skc42,skf15(skc42,X2267)) ),
inference(resolution,[status(thm)],[c1524,c488]) ).
cnf(c2163,plain,
( state(skc42,skf16(skc42,X2258))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2259)
| ~ two(skc12,X2259)
| ~ ssSkP1(X2259,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2259),X2259)
| frontseat(skc42,skf15(skc42,X2261))
| frontseat(skc42,skf15(skc42,X2260)) ),
inference(resolution,[status(thm)],[c1499,c488]) ).
cnf(c467,plain,
( state(skc42,skf16(skc42,X251))
| ssSkP0(skc43,skc42)
| in(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c370,c310]) ).
cnf(c2140,plain,
( state(skc42,skf16(skc42,X2253))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2256)
| ~ two(skc12,X2256)
| ~ ssSkP1(X2256,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2256),X2256)
| state(skc42,skf16(skc42,X2254))
| state(skc42,skf16(skc42,X2255)) ),
inference(resolution,[status(thm)],[c1476,c467]) ).
cnf(c2138,plain,
( state(skc42,skf16(skc42,X2249))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X2252)
| ~ two(skc12,X2252)
| ~ ssSkP1(X2252,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X2252),X2252)
| state(skc42,skf16(skc42,X2250))
| frontseat(skc42,skf15(skc42,X2251)) ),
inference(resolution,[status(thm)],[c1476,c488]) ).
cnf(clause45,negated_conjecture,
( ~ member(skc42,X10,skc43)
| ssSkC0
| young(skc42,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(c364,plain,
( ssSkC0
| young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[clause45,clause42]) ).
cnf(c576,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| in(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c364,clause38]) ).
cnf(c574,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| of(skc12,skc16,skc15) ),
inference(resolution,[status(thm)],[c364,clause40]) ).
cnf(c577,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| down(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c364,clause39]) ).
cnf(c856,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ~ city(skc12,X818)
| ~ chevy(skc12,X818)
| ~ white(skc12,X818)
| ~ dirty(skc12,X818)
| ~ old(skc12,X818)
| ~ agent(skc12,skc14,X818)
| ~ in(skc12,skc14,X818)
| ~ placename(skc12,X819)
| ~ hollywood_placename(skc12,X819)
| ~ of(skc12,X819,X818)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X817)
| ~ two(skc12,X817)
| ~ ssSkP1(X817,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X817),X817) ),
inference(resolution,[status(thm)],[c577,clause58]) ).
cnf(c1588,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1791)
| ~ two(skc12,X1791)
| ~ ssSkP1(X1791,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1791),X1791) ),
inference(resolution,[status(thm)],[c856,c574]) ).
cnf(c2116,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1792)
| ~ two(skc12,X1792)
| ~ ssSkP1(X1792,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1792),X1792) ),
inference(resolution,[status(thm)],[c1588,c576]) ).
cnf(clause44,negated_conjecture,
( ~ member(skc42,X9,skc43)
| ssSkC0
| fellow(skc42,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c362,plain,
( ssSkC0
| fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[clause44,clause42]) ).
cnf(c557,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| in(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c362,clause38]) ).
cnf(c555,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| of(skc12,skc16,skc15) ),
inference(resolution,[status(thm)],[c362,clause40]) ).
cnf(c558,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| down(skc12,skc14,skc15) ),
inference(resolution,[status(thm)],[c362,clause39]) ).
cnf(c854,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ~ city(skc12,X804)
| ~ chevy(skc12,X804)
| ~ white(skc12,X804)
| ~ dirty(skc12,X804)
| ~ old(skc12,X804)
| ~ agent(skc12,skc14,X804)
| ~ in(skc12,skc14,X804)
| ~ placename(skc12,X805)
| ~ hollywood_placename(skc12,X805)
| ~ of(skc12,X805,X804)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X803)
| ~ two(skc12,X803)
| ~ ssSkP1(X803,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X803),X803) ),
inference(resolution,[status(thm)],[c558,clause58]) ).
cnf(c1535,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1770)
| ~ two(skc12,X1770)
| ~ ssSkP1(X1770,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1770),X1770) ),
inference(resolution,[status(thm)],[c854,c555]) ).
cnf(c2077,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1771)
| ~ two(skc12,X1771)
| ~ ssSkP1(X1771,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1771),X1771) ),
inference(resolution,[status(thm)],[c1535,c557]) ).
cnf(clause36,negated_conjecture,
( ssSkC0
| down(skc42,skc44,skc45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c319,plain,
( in(skc12,skc14,skc15)
| down(skc42,skc44,skc45) ),
inference(resolution,[status(thm)],[clause38,clause36]) ).
cnf(c357,plain,
( of(skc12,skc16,skc15)
| down(skc42,skc44,skc45) ),
inference(resolution,[status(thm)],[clause40,clause36]) ).
cnf(c338,plain,
( down(skc12,skc14,skc15)
| down(skc42,skc44,skc45) ),
inference(resolution,[status(thm)],[clause39,clause36]) ).
cnf(c495,plain,
( down(skc42,skc44,skc45)
| ~ city(skc12,X689)
| ~ chevy(skc12,X689)
| ~ white(skc12,X689)
| ~ dirty(skc12,X689)
| ~ old(skc12,X689)
| ~ agent(skc12,skc14,X689)
| ~ in(skc12,skc14,X689)
| ~ placename(skc12,X690)
| ~ hollywood_placename(skc12,X690)
| ~ of(skc12,X690,X689)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X688)
| ~ two(skc12,X688)
| ~ ssSkP1(X688,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X688),X688) ),
inference(resolution,[status(thm)],[c338,clause58]) ).
cnf(c1428,plain,
( down(skc42,skc44,skc45)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1258)
| ~ two(skc12,X1258)
| ~ ssSkP1(X1258,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1258),X1258) ),
inference(resolution,[status(thm)],[c495,c357]) ).
cnf(c2055,plain,
( down(skc42,skc44,skc45)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1259)
| ~ two(skc12,X1259)
| ~ ssSkP1(X1259,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1259),X1259) ),
inference(resolution,[status(thm)],[c1428,c319]) ).
cnf(clause35,negated_conjecture,
( ssSkC0
| of(skc42,skc47,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c318,plain,
( in(skc12,skc14,skc15)
| of(skc42,skc47,skc46) ),
inference(resolution,[status(thm)],[clause38,clause35]) ).
cnf(c356,plain,
( of(skc12,skc16,skc15)
| of(skc42,skc47,skc46) ),
inference(resolution,[status(thm)],[clause40,clause35]) ).
cnf(c337,plain,
( down(skc12,skc14,skc15)
| of(skc42,skc47,skc46) ),
inference(resolution,[status(thm)],[clause39,clause35]) ).
cnf(c493,plain,
( of(skc42,skc47,skc46)
| ~ city(skc12,X683)
| ~ chevy(skc12,X683)
| ~ white(skc12,X683)
| ~ dirty(skc12,X683)
| ~ old(skc12,X683)
| ~ agent(skc12,skc14,X683)
| ~ in(skc12,skc14,X683)
| ~ placename(skc12,X684)
| ~ hollywood_placename(skc12,X684)
| ~ of(skc12,X684,X683)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X682)
| ~ two(skc12,X682)
| ~ ssSkP1(X682,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X682),X682) ),
inference(resolution,[status(thm)],[c337,clause58]) ).
cnf(c1400,plain,
( of(skc42,skc47,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1238)
| ~ two(skc12,X1238)
| ~ ssSkP1(X1238,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1238),X1238) ),
inference(resolution,[status(thm)],[c493,c356]) ).
cnf(c2032,plain,
( of(skc42,skc47,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1239)
| ~ two(skc12,X1239)
| ~ ssSkP1(X1239,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1239),X1239) ),
inference(resolution,[status(thm)],[c1400,c318]) ).
cnf(clause34,negated_conjecture,
( ssSkC0
| in(skc42,skc44,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c314,plain,
( in(skc12,skc14,skc15)
| in(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause38,clause34]) ).
cnf(c352,plain,
( of(skc12,skc16,skc15)
| in(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause40,clause34]) ).
cnf(c333,plain,
( down(skc12,skc14,skc15)
| in(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause39,clause34]) ).
cnf(c449,plain,
( in(skc42,skc44,skc46)
| ~ city(skc12,X671)
| ~ chevy(skc12,X671)
| ~ white(skc12,X671)
| ~ dirty(skc12,X671)
| ~ old(skc12,X671)
| ~ agent(skc12,skc14,X671)
| ~ in(skc12,skc14,X671)
| ~ placename(skc12,X672)
| ~ hollywood_placename(skc12,X672)
| ~ of(skc12,X672,X671)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X670)
| ~ two(skc12,X670)
| ~ ssSkP1(X670,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X670),X670) ),
inference(resolution,[status(thm)],[c333,clause58]) ).
cnf(c1356,plain,
( in(skc42,skc44,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1216)
| ~ two(skc12,X1216)
| ~ ssSkP1(X1216,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1216),X1216) ),
inference(resolution,[status(thm)],[c449,c352]) ).
cnf(c2012,plain,
( in(skc42,skc44,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1217)
| ~ two(skc12,X1217)
| ~ ssSkP1(X1217,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1217),X1217) ),
inference(resolution,[status(thm)],[c1356,c314]) ).
cnf(clause33,negated_conjecture,
( ssSkC0
| agent(skc42,skc44,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c313,plain,
( in(skc12,skc14,skc15)
| agent(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause38,clause33]) ).
cnf(c351,plain,
( of(skc12,skc16,skc15)
| agent(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause40,clause33]) ).
cnf(c332,plain,
( down(skc12,skc14,skc15)
| agent(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause39,clause33]) ).
cnf(c443,plain,
( agent(skc42,skc44,skc46)
| ~ city(skc12,X604)
| ~ chevy(skc12,X604)
| ~ white(skc12,X604)
| ~ dirty(skc12,X604)
| ~ old(skc12,X604)
| ~ agent(skc12,skc14,X604)
| ~ in(skc12,skc14,X604)
| ~ placename(skc12,X605)
| ~ hollywood_placename(skc12,X605)
| ~ of(skc12,X605,X604)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X603)
| ~ two(skc12,X603)
| ~ ssSkP1(X603,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X603),X603) ),
inference(resolution,[status(thm)],[c332,clause58]) ).
cnf(c1324,plain,
( agent(skc42,skc44,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1196)
| ~ two(skc12,X1196)
| ~ ssSkP1(X1196,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1196),X1196) ),
inference(resolution,[status(thm)],[c443,c351]) ).
cnf(c1985,plain,
( agent(skc42,skc44,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1197)
| ~ two(skc12,X1197)
| ~ ssSkP1(X1197,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1197),X1197) ),
inference(resolution,[status(thm)],[c1324,c313]) ).
cnf(clause3,negated_conjecture,
( ssSkC0
| city(skc42,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c322,plain,
( in(skc12,skc14,skc15)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause38,clause3]) ).
cnf(c360,plain,
( of(skc12,skc16,skc15)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause40,clause3]) ).
cnf(c341,plain,
( down(skc12,skc14,skc15)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause39,clause3]) ).
cnf(c432,plain,
( city(skc42,skc46)
| ~ city(skc12,X504)
| ~ chevy(skc12,X504)
| ~ white(skc12,X504)
| ~ dirty(skc12,X504)
| ~ old(skc12,X504)
| ~ agent(skc12,skc14,X504)
| ~ in(skc12,skc14,X504)
| ~ placename(skc12,X505)
| ~ hollywood_placename(skc12,X505)
| ~ of(skc12,X505,X504)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X503)
| ~ two(skc12,X503)
| ~ ssSkP1(X503,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X503),X503) ),
inference(resolution,[status(thm)],[c341,clause58]) ).
cnf(c1271,plain,
( city(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1103)
| ~ two(skc12,X1103)
| ~ ssSkP1(X1103,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1103),X1103) ),
inference(resolution,[status(thm)],[c432,c360]) ).
cnf(c1974,plain,
( city(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1104)
| ~ two(skc12,X1104)
| ~ ssSkP1(X1104,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1104),X1104) ),
inference(resolution,[status(thm)],[c1271,c322]) ).
cnf(clause10,negated_conjecture,
( ssSkC0
| event(skc42,skc44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c321,plain,
( in(skc12,skc14,skc15)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause38,clause10]) ).
cnf(c359,plain,
( of(skc12,skc16,skc15)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause40,clause10]) ).
cnf(c340,plain,
( down(skc12,skc14,skc15)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause39,clause10]) ).
cnf(c430,plain,
( event(skc42,skc44)
| ~ city(skc12,X492)
| ~ chevy(skc12,X492)
| ~ white(skc12,X492)
| ~ dirty(skc12,X492)
| ~ old(skc12,X492)
| ~ agent(skc12,skc14,X492)
| ~ in(skc12,skc14,X492)
| ~ placename(skc12,X493)
| ~ hollywood_placename(skc12,X493)
| ~ of(skc12,X493,X492)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X491)
| ~ two(skc12,X491)
| ~ ssSkP1(X491,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X491),X491) ),
inference(resolution,[status(thm)],[c340,clause58]) ).
cnf(c1245,plain,
( event(skc42,skc44)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1083)
| ~ two(skc12,X1083)
| ~ ssSkP1(X1083,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1083),X1083) ),
inference(resolution,[status(thm)],[c430,c359]) ).
cnf(c1925,plain,
( event(skc42,skc44)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1085)
| ~ two(skc12,X1085)
| ~ ssSkP1(X1085,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1085),X1085) ),
inference(resolution,[status(thm)],[c1245,c321]) ).
cnf(clause8,negated_conjecture,
( ssSkC0
| placename(skc42,skc47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c320,plain,
( in(skc12,skc14,skc15)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause38,clause8]) ).
cnf(c358,plain,
( of(skc12,skc16,skc15)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause40,clause8]) ).
cnf(c339,plain,
( down(skc12,skc14,skc15)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause39,clause8]) ).
cnf(c429,plain,
( placename(skc42,skc47)
| ~ city(skc12,X484)
| ~ chevy(skc12,X484)
| ~ white(skc12,X484)
| ~ dirty(skc12,X484)
| ~ old(skc12,X484)
| ~ agent(skc12,skc14,X484)
| ~ in(skc12,skc14,X484)
| ~ placename(skc12,X485)
| ~ hollywood_placename(skc12,X485)
| ~ of(skc12,X485,X484)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X483)
| ~ two(skc12,X483)
| ~ ssSkP1(X483,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X483),X483) ),
inference(resolution,[status(thm)],[c339,clause58]) ).
cnf(c1199,plain,
( placename(skc42,skc47)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1063)
| ~ two(skc12,X1063)
| ~ ssSkP1(X1063,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1063),X1063) ),
inference(resolution,[status(thm)],[c429,c358]) ).
cnf(c1908,plain,
( placename(skc42,skc47)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1064)
| ~ two(skc12,X1064)
| ~ ssSkP1(X1064,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1064),X1064) ),
inference(resolution,[status(thm)],[c1199,c320]) ).
cnf(clause15,negated_conjecture,
( ssSkC0
| group(skc42,skc43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c317,plain,
( in(skc12,skc14,skc15)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause38,clause15]) ).
cnf(c355,plain,
( of(skc12,skc16,skc15)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause40,clause15]) ).
cnf(c336,plain,
( down(skc12,skc14,skc15)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause39,clause15]) ).
cnf(c428,plain,
( group(skc42,skc43)
| ~ city(skc12,X476)
| ~ chevy(skc12,X476)
| ~ white(skc12,X476)
| ~ dirty(skc12,X476)
| ~ old(skc12,X476)
| ~ agent(skc12,skc14,X476)
| ~ in(skc12,skc14,X476)
| ~ placename(skc12,X477)
| ~ hollywood_placename(skc12,X477)
| ~ of(skc12,X477,X476)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X475)
| ~ two(skc12,X475)
| ~ ssSkP1(X475,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X475),X475) ),
inference(resolution,[status(thm)],[c336,clause58]) ).
cnf(c1190,plain,
( group(skc42,skc43)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1044)
| ~ two(skc12,X1044)
| ~ ssSkP1(X1044,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1044),X1044) ),
inference(resolution,[status(thm)],[c428,c355]) ).
cnf(c1898,plain,
( group(skc42,skc43)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1045)
| ~ two(skc12,X1045)
| ~ ssSkP1(X1045,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1045),X1045) ),
inference(resolution,[status(thm)],[c1190,c317]) ).
cnf(clause5,negated_conjecture,
( ssSkC0
| white(skc42,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c316,plain,
( in(skc12,skc14,skc15)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause38,clause5]) ).
cnf(c354,plain,
( of(skc12,skc16,skc15)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause40,clause5]) ).
cnf(c335,plain,
( down(skc12,skc14,skc15)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause39,clause5]) ).
cnf(c427,plain,
( white(skc42,skc46)
| ~ city(skc12,X468)
| ~ chevy(skc12,X468)
| ~ white(skc12,X468)
| ~ dirty(skc12,X468)
| ~ old(skc12,X468)
| ~ agent(skc12,skc14,X468)
| ~ in(skc12,skc14,X468)
| ~ placename(skc12,X469)
| ~ hollywood_placename(skc12,X469)
| ~ of(skc12,X469,X468)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X467)
| ~ two(skc12,X467)
| ~ ssSkP1(X467,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X467),X467) ),
inference(resolution,[status(thm)],[c335,clause58]) ).
cnf(c1155,plain,
( white(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1025)
| ~ two(skc12,X1025)
| ~ ssSkP1(X1025,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1025),X1025) ),
inference(resolution,[status(thm)],[c427,c354]) ).
cnf(c1861,plain,
( white(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1026)
| ~ two(skc12,X1026)
| ~ ssSkP1(X1026,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1026),X1026) ),
inference(resolution,[status(thm)],[c1155,c316]) ).
cnf(clause12,negated_conjecture,
( ssSkC0
| barrel(skc42,skc44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c315,plain,
( in(skc12,skc14,skc15)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause38,clause12]) ).
cnf(c353,plain,
( of(skc12,skc16,skc15)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause40,clause12]) ).
cnf(c334,plain,
( down(skc12,skc14,skc15)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause39,clause12]) ).
cnf(c426,plain,
( barrel(skc42,skc44)
| ~ city(skc12,X460)
| ~ chevy(skc12,X460)
| ~ white(skc12,X460)
| ~ dirty(skc12,X460)
| ~ old(skc12,X460)
| ~ agent(skc12,skc14,X460)
| ~ in(skc12,skc14,X460)
| ~ placename(skc12,X461)
| ~ hollywood_placename(skc12,X461)
| ~ of(skc12,X461,X460)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X459)
| ~ two(skc12,X459)
| ~ ssSkP1(X459,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X459),X459) ),
inference(resolution,[status(thm)],[c334,clause58]) ).
cnf(c1133,plain,
( barrel(skc42,skc44)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1004)
| ~ two(skc12,X1004)
| ~ ssSkP1(X1004,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1004),X1004) ),
inference(resolution,[status(thm)],[c426,c353]) ).
cnf(c1847,plain,
( barrel(skc42,skc44)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X1005)
| ~ two(skc12,X1005)
| ~ ssSkP1(X1005,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X1005),X1005) ),
inference(resolution,[status(thm)],[c1133,c315]) ).
cnf(clause11,negated_conjecture,
( ssSkC0
| present(skc42,skc44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c312,plain,
( in(skc12,skc14,skc15)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause38,clause11]) ).
cnf(c350,plain,
( of(skc12,skc16,skc15)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause40,clause11]) ).
cnf(c331,plain,
( down(skc12,skc14,skc15)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause39,clause11]) ).
cnf(c425,plain,
( present(skc42,skc44)
| ~ city(skc12,X452)
| ~ chevy(skc12,X452)
| ~ white(skc12,X452)
| ~ dirty(skc12,X452)
| ~ old(skc12,X452)
| ~ agent(skc12,skc14,X452)
| ~ in(skc12,skc14,X452)
| ~ placename(skc12,X453)
| ~ hollywood_placename(skc12,X453)
| ~ of(skc12,X453,X452)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X451)
| ~ two(skc12,X451)
| ~ ssSkP1(X451,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X451),X451) ),
inference(resolution,[status(thm)],[c331,clause58]) ).
cnf(c1108,plain,
( present(skc42,skc44)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X984)
| ~ two(skc12,X984)
| ~ ssSkP1(X984,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X984),X984) ),
inference(resolution,[status(thm)],[c425,c350]) ).
cnf(c1804,plain,
( present(skc42,skc44)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X986)
| ~ two(skc12,X986)
| ~ ssSkP1(X986,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X986),X986) ),
inference(resolution,[status(thm)],[c1108,c312]) ).
cnf(clause13,negated_conjecture,
( ssSkC0
| lonely(skc42,skc45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c311,plain,
( in(skc12,skc14,skc15)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause38,clause13]) ).
cnf(c349,plain,
( of(skc12,skc16,skc15)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause40,clause13]) ).
cnf(c330,plain,
( down(skc12,skc14,skc15)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause39,clause13]) ).
cnf(c424,plain,
( lonely(skc42,skc45)
| ~ city(skc12,X444)
| ~ chevy(skc12,X444)
| ~ white(skc12,X444)
| ~ dirty(skc12,X444)
| ~ old(skc12,X444)
| ~ agent(skc12,skc14,X444)
| ~ in(skc12,skc14,X444)
| ~ placename(skc12,X445)
| ~ hollywood_placename(skc12,X445)
| ~ of(skc12,X445,X444)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X443)
| ~ two(skc12,X443)
| ~ ssSkP1(X443,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X443),X443) ),
inference(resolution,[status(thm)],[c330,clause58]) ).
cnf(c1093,plain,
( lonely(skc42,skc45)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X965)
| ~ two(skc12,X965)
| ~ ssSkP1(X965,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X965),X965) ),
inference(resolution,[status(thm)],[c424,c349]) ).
cnf(c1793,plain,
( lonely(skc42,skc45)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X966)
| ~ two(skc12,X966)
| ~ ssSkP1(X966,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X966),X966) ),
inference(resolution,[status(thm)],[c1093,c311]) ).
cnf(c423,plain,
( ssSkP1(skc43,skc42)
| ~ city(skc12,X436)
| ~ chevy(skc12,X436)
| ~ white(skc12,X436)
| ~ dirty(skc12,X436)
| ~ old(skc12,X436)
| ~ agent(skc12,skc14,X436)
| ~ in(skc12,skc14,X436)
| ~ placename(skc12,X437)
| ~ hollywood_placename(skc12,X437)
| ~ of(skc12,X437,X436)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X435)
| ~ two(skc12,X435)
| ~ ssSkP1(X435,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X435),X435) ),
inference(resolution,[status(thm)],[c329,clause58]) ).
cnf(c1062,plain,
( ssSkP1(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X946)
| ~ two(skc12,X946)
| ~ ssSkP1(X946,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X946),X946) ),
inference(resolution,[status(thm)],[c423,c348]) ).
cnf(c1759,plain,
( ssSkP1(skc43,skc42)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X947)
| ~ two(skc12,X947)
| ~ ssSkP1(X947,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X947),X947) ),
inference(resolution,[status(thm)],[c1062,c310]) ).
cnf(clause9,negated_conjecture,
( ssSkC0
| hollywood_placename(skc42,skc47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c309,plain,
( in(skc12,skc14,skc15)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause38,clause9]) ).
cnf(c347,plain,
( of(skc12,skc16,skc15)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause40,clause9]) ).
cnf(c328,plain,
( down(skc12,skc14,skc15)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause39,clause9]) ).
cnf(c422,plain,
( hollywood_placename(skc42,skc47)
| ~ city(skc12,X428)
| ~ chevy(skc12,X428)
| ~ white(skc12,X428)
| ~ dirty(skc12,X428)
| ~ old(skc12,X428)
| ~ agent(skc12,skc14,X428)
| ~ in(skc12,skc14,X428)
| ~ placename(skc12,X429)
| ~ hollywood_placename(skc12,X429)
| ~ of(skc12,X429,X428)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X427)
| ~ two(skc12,X427)
| ~ ssSkP1(X427,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X427),X427) ),
inference(resolution,[status(thm)],[c328,clause58]) ).
cnf(c1047,plain,
( hollywood_placename(skc42,skc47)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X926)
| ~ two(skc12,X926)
| ~ ssSkP1(X926,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X926),X926) ),
inference(resolution,[status(thm)],[c422,c347]) ).
cnf(c1726,plain,
( hollywood_placename(skc42,skc47)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X927)
| ~ two(skc12,X927)
| ~ ssSkP1(X927,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X927),X927) ),
inference(resolution,[status(thm)],[c1047,c309]) ).
cnf(clause6,negated_conjecture,
( ssSkC0
| dirty(skc42,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c308,plain,
( in(skc12,skc14,skc15)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause38,clause6]) ).
cnf(c346,plain,
( of(skc12,skc16,skc15)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause40,clause6]) ).
cnf(c327,plain,
( down(skc12,skc14,skc15)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause39,clause6]) ).
cnf(c421,plain,
( dirty(skc42,skc46)
| ~ city(skc12,X420)
| ~ chevy(skc12,X420)
| ~ white(skc12,X420)
| ~ dirty(skc12,X420)
| ~ old(skc12,X420)
| ~ agent(skc12,skc14,X420)
| ~ in(skc12,skc14,X420)
| ~ placename(skc12,X421)
| ~ hollywood_placename(skc12,X421)
| ~ of(skc12,X421,X420)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X419)
| ~ two(skc12,X419)
| ~ ssSkP1(X419,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X419),X419) ),
inference(resolution,[status(thm)],[c327,clause58]) ).
cnf(c1027,plain,
( dirty(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X907)
| ~ two(skc12,X907)
| ~ ssSkP1(X907,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X907),X907) ),
inference(resolution,[status(thm)],[c421,c346]) ).
cnf(c1706,plain,
( dirty(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X908)
| ~ two(skc12,X908)
| ~ ssSkP1(X908,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X908),X908) ),
inference(resolution,[status(thm)],[c1027,c308]) ).
cnf(clause16,negated_conjecture,
( ssSkC0
| two(skc42,skc43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c307,plain,
( in(skc12,skc14,skc15)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause38,clause16]) ).
cnf(c345,plain,
( of(skc12,skc16,skc15)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause40,clause16]) ).
cnf(c326,plain,
( down(skc12,skc14,skc15)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause39,clause16]) ).
cnf(c420,plain,
( two(skc42,skc43)
| ~ city(skc12,X412)
| ~ chevy(skc12,X412)
| ~ white(skc12,X412)
| ~ dirty(skc12,X412)
| ~ old(skc12,X412)
| ~ agent(skc12,skc14,X412)
| ~ in(skc12,skc14,X412)
| ~ placename(skc12,X413)
| ~ hollywood_placename(skc12,X413)
| ~ of(skc12,X413,X412)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X411)
| ~ two(skc12,X411)
| ~ ssSkP1(X411,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X411),X411) ),
inference(resolution,[status(thm)],[c326,clause58]) ).
cnf(c1001,plain,
( two(skc42,skc43)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X887)
| ~ two(skc12,X887)
| ~ ssSkP1(X887,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X887),X887) ),
inference(resolution,[status(thm)],[c420,c345]) ).
cnf(c1694,plain,
( two(skc42,skc43)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X889)
| ~ two(skc12,X889)
| ~ ssSkP1(X889,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X889),X889) ),
inference(resolution,[status(thm)],[c1001,c307]) ).
cnf(clause4,negated_conjecture,
( ssSkC0
| chevy(skc42,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c306,plain,
( in(skc12,skc14,skc15)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause38,clause4]) ).
cnf(c344,plain,
( of(skc12,skc16,skc15)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause40,clause4]) ).
cnf(c325,plain,
( down(skc12,skc14,skc15)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause39,clause4]) ).
cnf(c419,plain,
( chevy(skc42,skc46)
| ~ city(skc12,X404)
| ~ chevy(skc12,X404)
| ~ white(skc12,X404)
| ~ dirty(skc12,X404)
| ~ old(skc12,X404)
| ~ agent(skc12,skc14,X404)
| ~ in(skc12,skc14,X404)
| ~ placename(skc12,X405)
| ~ hollywood_placename(skc12,X405)
| ~ of(skc12,X405,X404)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X403)
| ~ two(skc12,X403)
| ~ ssSkP1(X403,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X403),X403) ),
inference(resolution,[status(thm)],[c325,clause58]) ).
cnf(c970,plain,
( chevy(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X864)
| ~ two(skc12,X864)
| ~ ssSkP1(X864,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X864),X864) ),
inference(resolution,[status(thm)],[c419,c344]) ).
cnf(c1628,plain,
( chevy(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X865)
| ~ two(skc12,X865)
| ~ ssSkP1(X865,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X865),X865) ),
inference(resolution,[status(thm)],[c970,c306]) ).
cnf(clause7,negated_conjecture,
( ssSkC0
| old(skc42,skc46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c305,plain,
( in(skc12,skc14,skc15)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause38,clause7]) ).
cnf(c343,plain,
( of(skc12,skc16,skc15)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause40,clause7]) ).
cnf(c324,plain,
( down(skc12,skc14,skc15)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause39,clause7]) ).
cnf(c418,plain,
( old(skc42,skc46)
| ~ city(skc12,X396)
| ~ chevy(skc12,X396)
| ~ white(skc12,X396)
| ~ dirty(skc12,X396)
| ~ old(skc12,X396)
| ~ agent(skc12,skc14,X396)
| ~ in(skc12,skc14,X396)
| ~ placename(skc12,X397)
| ~ hollywood_placename(skc12,X397)
| ~ of(skc12,X397,X396)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X395)
| ~ two(skc12,X395)
| ~ ssSkP1(X395,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X395),X395) ),
inference(resolution,[status(thm)],[c324,clause58]) ).
cnf(c929,plain,
( old(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X838)
| ~ two(skc12,X838)
| ~ ssSkP1(X838,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X838),X838) ),
inference(resolution,[status(thm)],[c418,c343]) ).
cnf(c1621,plain,
( old(skc42,skc46)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X839)
| ~ two(skc12,X839)
| ~ ssSkP1(X839,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X839),X839) ),
inference(resolution,[status(thm)],[c929,c305]) ).
cnf(clause14,negated_conjecture,
( ssSkC0
| street(skc42,skc45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c304,plain,
( in(skc12,skc14,skc15)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause38,clause14]) ).
cnf(c342,plain,
( of(skc12,skc16,skc15)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause40,clause14]) ).
cnf(c323,plain,
( down(skc12,skc14,skc15)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause39,clause14]) ).
cnf(c417,plain,
( street(skc42,skc45)
| ~ city(skc12,X379)
| ~ chevy(skc12,X379)
| ~ white(skc12,X379)
| ~ dirty(skc12,X379)
| ~ old(skc12,X379)
| ~ agent(skc12,skc14,X379)
| ~ in(skc12,skc14,X379)
| ~ placename(skc12,X380)
| ~ hollywood_placename(skc12,X380)
| ~ of(skc12,X380,X379)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X378)
| ~ two(skc12,X378)
| ~ ssSkP1(X378,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X378),X378) ),
inference(resolution,[status(thm)],[c323,clause58]) ).
cnf(c916,plain,
( street(skc42,skc45)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ in(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X813)
| ~ two(skc12,X813)
| ~ ssSkP1(X813,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X813),X813) ),
inference(resolution,[status(thm)],[c417,c342]) ).
cnf(c1564,plain,
( street(skc42,skc45)
| ~ city(skc12,skc15)
| ~ chevy(skc12,skc15)
| ~ white(skc12,skc15)
| ~ dirty(skc12,skc15)
| ~ old(skc12,skc15)
| ~ agent(skc12,skc14,skc15)
| ~ placename(skc12,skc16)
| ~ hollywood_placename(skc12,skc16)
| ~ event(skc12,skc14)
| ~ present(skc12,skc14)
| ~ barrel(skc12,skc14)
| ~ lonely(skc12,skc15)
| ~ street(skc12,skc15)
| ~ group(skc12,X814)
| ~ two(skc12,X814)
| ~ ssSkP1(X814,skc12)
| ~ actual_world(skc12)
| ~ ssSkC0
| member(skc12,skf9(skc12,X814),X814) ),
inference(resolution,[status(thm)],[c916,c304]) ).
cnf(clause55,negated_conjecture,
( ~ in(X40,X39,skf14(X40,X38))
| ~ be(X40,X42,skf14(X40,X38),X39)
| ~ state(X40,X42)
| ssSkP0(X41,X40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
cnf(clause43,negated_conjecture,
( ssSkP1(X7,X8)
| member(X8,skf19(X8,X7),X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(clause47,negated_conjecture,
( ~ member(skc12,X12,skc13)
| ~ ssSkC0
| young(skc12,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(c367,plain,
( ~ ssSkC0
| young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12) ),
inference(resolution,[status(thm)],[clause47,clause43]) ).
cnf(c616,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[c367,clause17]) ).
cnf(c792,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c616,c378]) ).
cnf(c1474,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| ssSkP0(skc43,skc42)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X802,skc42) ),
inference(resolution,[status(thm)],[c792,clause55]) ).
cnf(clause46,negated_conjecture,
( ~ member(skc12,X11,skc13)
| ~ ssSkC0
| fellow(skc12,X11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c365,plain,
( ~ ssSkC0
| fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12) ),
inference(resolution,[status(thm)],[clause46,clause43]) ).
cnf(c593,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[c365,clause17]) ).
cnf(c728,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c593,c378]) ).
cnf(c1469,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| ssSkP0(skc43,skc42)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X796,skc42) ),
inference(resolution,[status(thm)],[c728,clause55]) ).
cnf(clause37,negated_conjecture,
( ~ ssSkC0
| agent(skc12,skc14,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c291,plain,
( agent(skc12,skc14,skc17)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause37,clause17]) ).
cnf(c686,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| agent(skc12,skc14,skc17) ),
inference(resolution,[status(thm)],[c378,c291]) ).
cnf(c1464,plain,
( ssSkP0(skc43,skc42)
| agent(skc12,skc14,skc17)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X775,skc42) ),
inference(resolution,[status(thm)],[c686,clause55]) ).
cnf(c1463,plain,
( ssSkP0(skc43,skc42)
| in(skc12,skc14,skc15)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X774,skc42) ),
inference(resolution,[status(thm)],[c684,clause55]) ).
cnf(c1461,plain,
( ssSkP0(skc43,skc42)
| down(skc12,skc14,skc15)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X769,skc42) ),
inference(resolution,[status(thm)],[c683,clause55]) ).
cnf(c1440,plain,
( ssSkP0(skc43,skc42)
| of(skc12,skc16,skc15)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X768,skc42) ),
inference(resolution,[status(thm)],[c682,clause55]) ).
cnf(clause29,negated_conjecture,
( ~ ssSkC0
| placename(skc12,skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c171,plain,
( placename(skc12,skc16)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause29,clause17]) ).
cnf(c688,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c378,c171]) ).
cnf(c1439,plain,
( ssSkP0(skc43,skc42)
| placename(skc12,skc16)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X767,skc42) ),
inference(resolution,[status(thm)],[c688,clause55]) ).
cnf(clause27,negated_conjecture,
( ~ ssSkC0
| city(skc12,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c141,plain,
( city(skc12,skc15)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause27,clause17]) ).
cnf(c687,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[c378,c141]) ).
cnf(c1414,plain,
( ssSkP0(skc43,skc42)
| city(skc12,skc15)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X766,skc42) ),
inference(resolution,[status(thm)],[c687,clause55]) ).
cnf(clause19,negated_conjecture,
( ~ ssSkC0
| present(skc12,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c21,plain,
( present(skc12,skc14)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause19,clause17]) ).
cnf(c685,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[c378,c21]) ).
cnf(c1413,plain,
( ssSkP0(skc43,skc42)
| present(skc12,skc14)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X765,skc42) ),
inference(resolution,[status(thm)],[c685,clause55]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| ssSkP0(skc13,skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c216,plain,
( ssSkP0(skc13,skc12)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause32,clause17]) ).
cnf(c680,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[c378,c216]) ).
cnf(c1412,plain,
( ssSkP0(skc43,skc42)
| ssSkP0(skc13,skc12)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X764,skc42) ),
inference(resolution,[status(thm)],[c680,clause55]) ).
cnf(clause30,negated_conjecture,
( ~ ssSkC0
| group(skc12,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c186,plain,
( group(skc12,skc13)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause30,clause17]) ).
cnf(c679,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[c378,c186]) ).
cnf(c1411,plain,
( ssSkP0(skc43,skc42)
| group(skc12,skc13)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X763,skc42) ),
inference(resolution,[status(thm)],[c679,clause55]) ).
cnf(clause28,negated_conjecture,
( ~ ssSkC0
| hollywood_placename(skc12,skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c156,plain,
( hollywood_placename(skc12,skc16)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause28,clause17]) ).
cnf(c678,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c378,c156]) ).
cnf(c1410,plain,
( ssSkP0(skc43,skc42)
| hollywood_placename(skc12,skc16)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X762,skc42) ),
inference(resolution,[status(thm)],[c678,clause55]) ).
cnf(clause26,negated_conjecture,
( ~ ssSkC0
| street(skc12,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c126,plain,
( street(skc12,skc15)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause26,clause17]) ).
cnf(c677,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[c378,c126]) ).
cnf(c1409,plain,
( ssSkP0(skc43,skc42)
| street(skc12,skc15)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X761,skc42) ),
inference(resolution,[status(thm)],[c677,clause55]) ).
cnf(clause24,negated_conjecture,
( ~ ssSkC0
| chevy(skc12,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c96,plain,
( chevy(skc12,skc17)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause24,clause17]) ).
cnf(c676,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[c378,c96]) ).
cnf(c1408,plain,
( ssSkP0(skc43,skc42)
| chevy(skc12,skc17)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X760,skc42) ),
inference(resolution,[status(thm)],[c676,clause55]) ).
cnf(clause22,negated_conjecture,
( ~ ssSkC0
| dirty(skc12,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c66,plain,
( dirty(skc12,skc17)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause22,clause17]) ).
cnf(c675,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[c378,c66]) ).
cnf(c1407,plain,
( ssSkP0(skc43,skc42)
| dirty(skc12,skc17)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X759,skc42) ),
inference(resolution,[status(thm)],[c675,clause55]) ).
cnf(clause18,negated_conjecture,
( ~ ssSkC0
| event(skc12,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c6,plain,
( event(skc12,skc14)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause18,clause17]) ).
cnf(c674,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[c378,c6]) ).
cnf(c1406,plain,
( ssSkP0(skc43,skc42)
| event(skc12,skc14)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X758,skc42) ),
inference(resolution,[status(thm)],[c674,clause55]) ).
cnf(clause20,negated_conjecture,
( ~ ssSkC0
| barrel(skc12,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c36,plain,
( barrel(skc12,skc14)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause20,clause17]) ).
cnf(c673,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[c378,c36]) ).
cnf(c1405,plain,
( ssSkP0(skc43,skc42)
| barrel(skc12,skc14)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X757,skc42) ),
inference(resolution,[status(thm)],[c673,clause55]) ).
cnf(clause31,negated_conjecture,
( ~ ssSkC0
| two(skc12,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c201,plain,
( two(skc12,skc13)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause31,clause17]) ).
cnf(c672,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[c378,c201]) ).
cnf(c1380,plain,
( ssSkP0(skc43,skc42)
| two(skc12,skc13)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X756,skc42) ),
inference(resolution,[status(thm)],[c672,clause55]) ).
cnf(clause25,negated_conjecture,
( ~ ssSkC0
| lonely(skc12,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c111,plain,
( lonely(skc12,skc15)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause25,clause17]) ).
cnf(c670,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[c378,c111]) ).
cnf(c1379,plain,
( ssSkP0(skc43,skc42)
| lonely(skc12,skc15)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X755,skc42) ),
inference(resolution,[status(thm)],[c670,clause55]) ).
cnf(clause23,negated_conjecture,
( ~ ssSkC0
| white(skc12,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c81,plain,
( white(skc12,skc17)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause23,clause17]) ).
cnf(c669,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[c378,c81]) ).
cnf(c1378,plain,
( ssSkP0(skc43,skc42)
| white(skc12,skc17)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X754,skc42) ),
inference(resolution,[status(thm)],[c669,clause55]) ).
cnf(clause21,negated_conjecture,
( ~ ssSkC0
| old(skc12,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c51,plain,
( old(skc12,skc17)
| ssSkP1(skc43,skc42) ),
inference(resolution,[status(thm)],[clause21,clause17]) ).
cnf(c668,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[c378,c51]) ).
cnf(c1377,plain,
( ssSkP0(skc43,skc42)
| old(skc12,skc17)
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X753,skc42) ),
inference(resolution,[status(thm)],[c668,clause55]) ).
cnf(c671,plain,
( be(skc42,skf16(skc42,skf14(skc42,skc43)),skf14(skc42,skc43),skf15(skc42,skf14(skc42,skc43)))
| ssSkP0(skc43,skc42)
| ssSkC0 ),
inference(resolution,[status(thm)],[c378,clause17]) ).
cnf(c1331,plain,
( ssSkP0(skc43,skc42)
| ssSkC0
| ~ in(skc42,skf15(skc42,skf14(skc42,skc43)),skf14(skc42,skc43))
| ~ state(skc42,skf16(skc42,skf14(skc42,skc43)))
| ssSkP0(X744,skc42) ),
inference(resolution,[status(thm)],[c671,clause55]) ).
cnf(c681,plain,
( be(X510,skf16(X510,skf14(X510,X511)),skf14(X510,X511),skf15(X510,skf14(X510,X511)))
| ssSkP0(X511,X510)
| member(X510,skf19(X510,X511),X511) ),
inference(resolution,[status(thm)],[c378,clause43]) ).
cnf(c1287,plain,
( ssSkP0(X662,X664)
| member(X664,skf19(X664,X662),X662)
| ~ in(X664,skf15(X664,skf14(X664,X662)),skf14(X664,X662))
| ~ state(X664,skf16(X664,skf14(X664,X662)))
| ssSkP0(X663,X664) ),
inference(resolution,[status(thm)],[c681,clause55]) ).
cnf(c791,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| in(skc42,skf15(skc42,X599),skf15(skc42,X599))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c616,c374]) ).
cnf(c727,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| in(skc42,skf15(skc42,X574),skf15(skc42,X574))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c593,c374]) ).
cnf(c615,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c367,c364]) ).
cnf(c603,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c367,c362]) ).
cnf(c592,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c365,c364]) ).
cnf(c580,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c365,c362]) ).
cnf(c454,plain,
( state(skc42,skf16(skc42,X86))
| ssSkP0(skc43,skc42)
| ssSkC0 ),
inference(resolution,[status(thm)],[c370,clause17]) ).
cnf(c611,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| state(skc42,skf16(skc42,X399))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c367,c454]) ).
cnf(c475,plain,
( frontseat(skc42,skf15(skc42,X87))
| ssSkP0(skc43,skc42)
| ssSkC0 ),
inference(resolution,[status(thm)],[c372,clause17]) ).
cnf(c607,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| frontseat(skc42,skf15(skc42,X398))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c367,c475]) ).
cnf(c588,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| state(skc42,skf16(skc42,X394))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c365,c454]) ).
cnf(c584,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| frontseat(skc42,skf15(skc42,X393))
| ssSkP0(skc43,skc42) ),
inference(resolution,[status(thm)],[c365,c475]) ).
cnf(c643,plain,
( in(skc42,skf15(skc42,X373),skf15(skc42,X373))
| ssSkP0(skc43,skc42)
| agent(skc12,skc14,skc17) ),
inference(resolution,[status(thm)],[c374,c291]) ).
cnf(c645,plain,
( in(skc42,skf15(skc42,X309),skf15(skc42,X309))
| ssSkP0(skc43,skc42)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c374,c171]) ).
cnf(c644,plain,
( in(skc42,skf15(skc42,X308),skf15(skc42,X308))
| ssSkP0(skc43,skc42)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[c374,c141]) ).
cnf(c642,plain,
( in(skc42,skf15(skc42,X307),skf15(skc42,X307))
| ssSkP0(skc43,skc42)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[c374,c21]) ).
cnf(c637,plain,
( in(skc42,skf15(skc42,X306),skf15(skc42,X306))
| ssSkP0(skc43,skc42)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[c374,c216]) ).
cnf(c636,plain,
( in(skc42,skf15(skc42,X305),skf15(skc42,X305))
| ssSkP0(skc43,skc42)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[c374,c186]) ).
cnf(c635,plain,
( in(skc42,skf15(skc42,X301),skf15(skc42,X301))
| ssSkP0(skc43,skc42)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c374,c156]) ).
cnf(c634,plain,
( in(skc42,skf15(skc42,X300),skf15(skc42,X300))
| ssSkP0(skc43,skc42)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[c374,c126]) ).
cnf(c633,plain,
( in(skc42,skf15(skc42,X299),skf15(skc42,X299))
| ssSkP0(skc43,skc42)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[c374,c96]) ).
cnf(c632,plain,
( in(skc42,skf15(skc42,X298),skf15(skc42,X298))
| ssSkP0(skc43,skc42)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[c374,c66]) ).
cnf(c631,plain,
( in(skc42,skf15(skc42,X297),skf15(skc42,X297))
| ssSkP0(skc43,skc42)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[c374,c6]) ).
cnf(c630,plain,
( in(skc42,skf15(skc42,X293),skf15(skc42,X293))
| ssSkP0(skc43,skc42)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[c374,c36]) ).
cnf(c629,plain,
( in(skc42,skf15(skc42,X292),skf15(skc42,X292))
| ssSkP0(skc43,skc42)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[c374,c201]) ).
cnf(c627,plain,
( in(skc42,skf15(skc42,X291),skf15(skc42,X291))
| ssSkP0(skc43,skc42)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[c374,c111]) ).
cnf(c626,plain,
( in(skc42,skf15(skc42,X290),skf15(skc42,X290))
| ssSkP0(skc43,skc42)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[c374,c81]) ).
cnf(c625,plain,
( in(skc42,skf15(skc42,X289),skf15(skc42,X289))
| ssSkP0(skc43,skc42)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[c374,c51]) ).
cnf(c618,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| in(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[c367,clause34]) ).
cnf(c617,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| agent(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[c367,clause33]) ).
cnf(c614,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| down(skc42,skc44,skc45) ),
inference(resolution,[status(thm)],[c367,clause36]) ).
cnf(c606,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| of(skc42,skc47,skc46) ),
inference(resolution,[status(thm)],[c367,clause35]) ).
cnf(c595,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| in(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[c365,clause34]) ).
cnf(c594,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| agent(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[c365,clause33]) ).
cnf(c591,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| down(skc42,skc44,skc45) ),
inference(resolution,[status(thm)],[c365,clause36]) ).
cnf(c583,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| of(skc42,skc47,skc46) ),
inference(resolution,[status(thm)],[c365,clause35]) ).
cnf(c578,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| agent(skc12,skc14,skc17) ),
inference(resolution,[status(thm)],[c364,clause37]) ).
cnf(c559,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| agent(skc12,skc14,skc17) ),
inference(resolution,[status(thm)],[c362,clause37]) ).
cnf(c638,plain,
( in(X275,skf15(X275,X274),skf15(X275,X274))
| ssSkP0(X276,X275)
| member(X275,skf19(X275,X276),X276) ),
inference(resolution,[status(thm)],[c374,clause43]) ).
cnf(c490,plain,
( frontseat(skc42,skf15(skc42,X259))
| ssSkP0(skc43,skc42)
| agent(skc12,skc14,skc17) ),
inference(resolution,[status(thm)],[c372,c291]) ).
cnf(c469,plain,
( state(skc42,skf16(skc42,X255))
| ssSkP0(skc43,skc42)
| agent(skc12,skc14,skc17) ),
inference(resolution,[status(thm)],[c370,c291]) ).
cnf(c628,plain,
( in(skc42,skf15(skc42,X229),skf15(skc42,X229))
| ssSkP0(skc43,skc42)
| ssSkC0 ),
inference(resolution,[status(thm)],[c374,clause17]) ).
cnf(c624,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[c367,clause10]) ).
cnf(c623,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[c367,clause8]) ).
cnf(c622,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[c367,clause5]) ).
cnf(c621,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[c367,clause6]) ).
cnf(c620,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[c367,clause4]) ).
cnf(c619,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[c367,clause3]) ).
cnf(c613,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[c367,clause15]) ).
cnf(c612,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[c367,clause16]) ).
cnf(c610,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[c367,clause14]) ).
cnf(c609,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[c367,clause13]) ).
cnf(c608,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[c367,clause11]) ).
cnf(c605,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[c367,clause12]) ).
cnf(c604,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[c367,clause9]) ).
cnf(c602,plain,
( young(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[c367,clause7]) ).
cnf(c601,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[c365,clause10]) ).
cnf(c600,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[c365,clause8]) ).
cnf(c599,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[c365,clause5]) ).
cnf(c598,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[c365,clause6]) ).
cnf(c597,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[c365,clause4]) ).
cnf(c596,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[c365,clause3]) ).
cnf(c590,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[c365,clause15]) ).
cnf(c589,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[c365,clause16]) ).
cnf(c587,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[c365,clause14]) ).
cnf(c586,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[c365,clause13]) ).
cnf(c585,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[c365,clause11]) ).
cnf(c582,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[c365,clause12]) ).
cnf(c581,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[c365,clause9]) ).
cnf(c579,plain,
( fellow(skc12,skf19(skc12,skc13))
| ssSkP1(skc13,skc12)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[c365,clause7]) ).
cnf(c575,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[c364,clause18]) ).
cnf(c573,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[c364,clause32]) ).
cnf(c572,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[c364,clause30]) ).
cnf(c571,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[c364,clause31]) ).
cnf(c570,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c364,clause29]) ).
cnf(c569,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c364,clause28]) ).
cnf(c568,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[c364,clause27]) ).
cnf(c567,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[c364,clause26]) ).
cnf(c566,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[c364,clause25]) ).
cnf(c565,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[c364,clause24]) ).
cnf(c564,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[c364,clause23]) ).
cnf(c563,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[c364,clause19]) ).
cnf(c562,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[c364,clause21]) ).
cnf(c561,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[c364,clause20]) ).
cnf(c560,plain,
( young(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[c364,clause22]) ).
cnf(c556,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[c362,clause18]) ).
cnf(c554,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[c362,clause32]) ).
cnf(c553,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[c362,clause30]) ).
cnf(c552,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[c362,clause31]) ).
cnf(c551,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c362,clause29]) ).
cnf(c550,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c362,clause28]) ).
cnf(c549,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[c362,clause27]) ).
cnf(c548,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[c362,clause26]) ).
cnf(c547,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[c362,clause25]) ).
cnf(c546,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[c362,clause24]) ).
cnf(c545,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[c362,clause23]) ).
cnf(c544,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[c362,clause19]) ).
cnf(c543,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[c362,clause21]) ).
cnf(c542,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[c362,clause20]) ).
cnf(c541,plain,
( fellow(skc42,skf14(skc42,skc43))
| ssSkP0(skc43,skc42)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[c362,clause22]) ).
cnf(clause57,negated_conjecture,
( ~ event(X50,X49)
| ~ present(X50,X49)
| ~ barrel(X50,X49)
| ~ agent(X50,X49,X48)
| ~ old(X50,X48)
| ~ dirty(X50,X48)
| ~ white(X50,X48)
| ~ chevy(X50,X48)
| ~ in(X50,X49,X53)
| ~ down(X50,X49,X53)
| ~ lonely(X50,X53)
| ~ street(X50,X53)
| ~ city(X50,X53)
| ~ of(X50,X51,X53)
| ~ hollywood_placename(X50,X51)
| ~ placename(X50,X51)
| ~ group(X50,X52)
| ~ two(X50,X52)
| ~ ssSkP0(X52,X50)
| ~ actual_world(X50)
| ssSkC0
| member(X50,skf21(X50,X52),X52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c383,plain,
( ~ event(skc42,X158)
| ~ present(skc42,X158)
| ~ barrel(skc42,X158)
| ~ agent(skc42,X158,X157)
| ~ old(skc42,X157)
| ~ dirty(skc42,X157)
| ~ white(skc42,X157)
| ~ chevy(skc42,X157)
| ~ in(skc42,X158,skc46)
| ~ down(skc42,X158,skc46)
| ~ lonely(skc42,skc46)
| ~ street(skc42,skc46)
| ~ city(skc42,skc46)
| ~ hollywood_placename(skc42,skc47)
| ~ placename(skc42,skc47)
| ~ group(skc42,X156)
| ~ two(skc42,X156)
| ~ ssSkP0(X156,skc42)
| ~ actual_world(skc42)
| ssSkC0
| member(skc42,skf21(skc42,X156),X156) ),
inference(resolution,[status(thm)],[clause57,clause35]) ).
cnf(c492,plain,
( frontseat(skc42,skf15(skc42,X145))
| ssSkP0(skc43,skc42)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c372,c171]) ).
cnf(c491,plain,
( frontseat(skc42,skf15(skc42,X144))
| ssSkP0(skc43,skc42)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[c372,c141]) ).
cnf(clause54,negated_conjecture,
( ~ member(X35,X37,X36)
| ~ frontseat(X35,X37)
| ~ ssSkP0(X36,X35)
| be(X35,skf11(X35,X37),X37,skf10(X37,X35)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(c381,plain,
( ~ frontseat(X142,skf19(X142,X143))
| ~ ssSkP0(X143,X142)
| be(X142,skf11(X142,skf19(X142,X143)),skf19(X142,X143),skf10(skf19(X142,X143),X142))
| ssSkP1(X143,X142) ),
inference(resolution,[status(thm)],[clause54,clause43]) ).
cnf(c489,plain,
( frontseat(skc42,skf15(skc42,X141))
| ssSkP0(skc43,skc42)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[c372,c21]) ).
cnf(c484,plain,
( frontseat(skc42,skf15(skc42,X140))
| ssSkP0(skc43,skc42)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[c372,c216]) ).
cnf(c483,plain,
( frontseat(skc42,skf15(skc42,X139))
| ssSkP0(skc43,skc42)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[c372,c186]) ).
cnf(c482,plain,
( frontseat(skc42,skf15(skc42,X138))
| ssSkP0(skc43,skc42)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c372,c156]) ).
cnf(c481,plain,
( frontseat(skc42,skf15(skc42,X137))
| ssSkP0(skc43,skc42)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[c372,c126]) ).
cnf(c480,plain,
( frontseat(skc42,skf15(skc42,X134))
| ssSkP0(skc43,skc42)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[c372,c96]) ).
cnf(c479,plain,
( frontseat(skc42,skf15(skc42,X133))
| ssSkP0(skc43,skc42)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[c372,c66]) ).
cnf(c478,plain,
( frontseat(skc42,skf15(skc42,X132))
| ssSkP0(skc43,skc42)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[c372,c6]) ).
cnf(c477,plain,
( frontseat(skc42,skf15(skc42,X131))
| ssSkP0(skc43,skc42)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[c372,c36]) ).
cnf(c476,plain,
( frontseat(skc42,skf15(skc42,X130))
| ssSkP0(skc43,skc42)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[c372,c201]) ).
cnf(clause53,negated_conjecture,
( ~ member(X32,X34,X33)
| ~ frontseat(X32,X34)
| ~ ssSkP0(X33,X32)
| in(X32,skf10(X34,X32),X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
cnf(c379,plain,
( ~ frontseat(X128,skf19(X128,X129))
| ~ ssSkP0(X129,X128)
| in(X128,skf10(skf19(X128,X129),X128),skf19(X128,X129))
| ssSkP1(X129,X128) ),
inference(resolution,[status(thm)],[clause53,clause43]) ).
cnf(c474,plain,
( frontseat(skc42,skf15(skc42,X127))
| ssSkP0(skc43,skc42)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[c372,c111]) ).
cnf(c473,plain,
( frontseat(skc42,skf15(skc42,X126))
| ssSkP0(skc43,skc42)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[c372,c81]) ).
cnf(c472,plain,
( frontseat(skc42,skf15(skc42,X125))
| ssSkP0(skc43,skc42)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[c372,c51]) ).
cnf(c471,plain,
( state(skc42,skf16(skc42,X124))
| ssSkP0(skc43,skc42)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c370,c171]) ).
cnf(c470,plain,
( state(skc42,skf16(skc42,X123))
| ssSkP0(skc43,skc42)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[c370,c141]) ).
cnf(c468,plain,
( state(skc42,skf16(skc42,X120))
| ssSkP0(skc43,skc42)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[c370,c21]) ).
cnf(c463,plain,
( state(skc42,skf16(skc42,X119))
| ssSkP0(skc43,skc42)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[c370,c216]) ).
cnf(c462,plain,
( state(skc42,skf16(skc42,X118))
| ssSkP0(skc43,skc42)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[c370,c186]) ).
cnf(c461,plain,
( state(skc42,skf16(skc42,X117))
| ssSkP0(skc43,skc42)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[c370,c156]) ).
cnf(c460,plain,
( state(skc42,skf16(skc42,X116))
| ssSkP0(skc43,skc42)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[c370,c126]) ).
cnf(c459,plain,
( state(skc42,skf16(skc42,X113))
| ssSkP0(skc43,skc42)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[c370,c96]) ).
cnf(c458,plain,
( state(skc42,skf16(skc42,X112))
| ssSkP0(skc43,skc42)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[c370,c66]) ).
cnf(c457,plain,
( state(skc42,skf16(skc42,X111))
| ssSkP0(skc43,skc42)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[c370,c6]) ).
cnf(c456,plain,
( state(skc42,skf16(skc42,X110))
| ssSkP0(skc43,skc42)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[c370,c36]) ).
cnf(c455,plain,
( state(skc42,skf16(skc42,X109))
| ssSkP0(skc43,skc42)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[c370,c201]) ).
cnf(c453,plain,
( state(skc42,skf16(skc42,X105))
| ssSkP0(skc43,skc42)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[c370,c111]) ).
cnf(c452,plain,
( state(skc42,skf16(skc42,X104))
| ssSkP0(skc43,skc42)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[c370,c81]) ).
cnf(c451,plain,
( state(skc42,skf16(skc42,X103))
| ssSkP0(skc43,skc42)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[c370,c51]) ).
cnf(c485,plain,
( frontseat(X101,skf15(X101,X100))
| ssSkP0(X102,X101)
| member(X101,skf19(X101,X102),X102) ),
inference(resolution,[status(thm)],[c372,clause43]) ).
cnf(c464,plain,
( state(X98,skf16(X98,X97))
| ssSkP0(X99,X98)
| member(X98,skf19(X98,X99),X99) ),
inference(resolution,[status(thm)],[c370,clause43]) ).
cnf(clause51,negated_conjecture,
( ~ member(X26,X28,X27)
| ~ frontseat(X26,X28)
| ~ ssSkP0(X27,X26)
| state(X26,skf11(X26,X25)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(c375,plain,
( ~ frontseat(X95,skf19(X95,X96))
| ~ ssSkP0(X96,X95)
| state(X95,skf11(X95,X94))
| ssSkP1(X96,X95) ),
inference(resolution,[status(thm)],[clause51,clause43]) ).
cnf(c300,plain,
( agent(skc12,skc14,skc17)
| down(skc42,skc44,skc45) ),
inference(resolution,[status(thm)],[clause37,clause36]) ).
cnf(c299,plain,
( agent(skc12,skc14,skc17)
| of(skc42,skc47,skc46) ),
inference(resolution,[status(thm)],[clause37,clause35]) ).
cnf(c295,plain,
( agent(skc12,skc14,skc17)
| in(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause37,clause34]) ).
cnf(c303,plain,
( agent(skc12,skc14,skc17)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause37,clause3]) ).
cnf(c294,plain,
( agent(skc12,skc14,skc17)
| agent(skc42,skc44,skc46) ),
inference(resolution,[status(thm)],[clause37,clause33]) ).
cnf(c302,plain,
( agent(skc12,skc14,skc17)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause37,clause10]) ).
cnf(c301,plain,
( agent(skc12,skc14,skc17)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause37,clause8]) ).
cnf(c298,plain,
( agent(skc12,skc14,skc17)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause37,clause15]) ).
cnf(c297,plain,
( agent(skc12,skc14,skc17)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause37,clause5]) ).
cnf(c296,plain,
( agent(skc12,skc14,skc17)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause37,clause12]) ).
cnf(c293,plain,
( agent(skc12,skc14,skc17)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause37,clause11]) ).
cnf(c292,plain,
( agent(skc12,skc14,skc17)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause37,clause13]) ).
cnf(c290,plain,
( agent(skc12,skc14,skc17)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause37,clause9]) ).
cnf(c289,plain,
( agent(skc12,skc14,skc17)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause37,clause6]) ).
cnf(c288,plain,
( agent(skc12,skc14,skc17)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause37,clause16]) ).
cnf(c287,plain,
( agent(skc12,skc14,skc17)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause37,clause4]) ).
cnf(c286,plain,
( agent(skc12,skc14,skc17)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause37,clause7]) ).
cnf(c285,plain,
( agent(skc12,skc14,skc17)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause37,clause14]) ).
cnf(c284,plain,
( down(skc42,skc44,skc45)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[clause36,clause18]) ).
cnf(c283,plain,
( down(skc42,skc44,skc45)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[clause36,clause32]) ).
cnf(c282,plain,
( down(skc42,skc44,skc45)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[clause36,clause30]) ).
cnf(c281,plain,
( down(skc42,skc44,skc45)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[clause36,clause31]) ).
cnf(c280,plain,
( down(skc42,skc44,skc45)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause36,clause29]) ).
cnf(c279,plain,
( down(skc42,skc44,skc45)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause36,clause28]) ).
cnf(c278,plain,
( down(skc42,skc44,skc45)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[clause36,clause27]) ).
cnf(c277,plain,
( down(skc42,skc44,skc45)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[clause36,clause26]) ).
cnf(c276,plain,
( down(skc42,skc44,skc45)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[clause36,clause25]) ).
cnf(c275,plain,
( down(skc42,skc44,skc45)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[clause36,clause24]) ).
cnf(c274,plain,
( down(skc42,skc44,skc45)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[clause36,clause23]) ).
cnf(c273,plain,
( down(skc42,skc44,skc45)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[clause36,clause19]) ).
cnf(c272,plain,
( down(skc42,skc44,skc45)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[clause36,clause21]) ).
cnf(c271,plain,
( down(skc42,skc44,skc45)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[clause36,clause20]) ).
cnf(c270,plain,
( down(skc42,skc44,skc45)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[clause36,clause22]) ).
cnf(c269,plain,
( of(skc42,skc47,skc46)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[clause35,clause18]) ).
cnf(c268,plain,
( of(skc42,skc47,skc46)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[clause35,clause32]) ).
cnf(c267,plain,
( of(skc42,skc47,skc46)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[clause35,clause30]) ).
cnf(c266,plain,
( of(skc42,skc47,skc46)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[clause35,clause31]) ).
cnf(c265,plain,
( of(skc42,skc47,skc46)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause35,clause29]) ).
cnf(c264,plain,
( of(skc42,skc47,skc46)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause35,clause28]) ).
cnf(c263,plain,
( of(skc42,skc47,skc46)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[clause35,clause27]) ).
cnf(c262,plain,
( of(skc42,skc47,skc46)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[clause35,clause26]) ).
cnf(c261,plain,
( of(skc42,skc47,skc46)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[clause35,clause25]) ).
cnf(c260,plain,
( of(skc42,skc47,skc46)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[clause35,clause24]) ).
cnf(c259,plain,
( of(skc42,skc47,skc46)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[clause35,clause23]) ).
cnf(c258,plain,
( of(skc42,skc47,skc46)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[clause35,clause19]) ).
cnf(c257,plain,
( of(skc42,skc47,skc46)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[clause35,clause21]) ).
cnf(c256,plain,
( of(skc42,skc47,skc46)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[clause35,clause20]) ).
cnf(c255,plain,
( of(skc42,skc47,skc46)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[clause35,clause22]) ).
cnf(c254,plain,
( in(skc42,skc44,skc46)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[clause34,clause18]) ).
cnf(c253,plain,
( in(skc42,skc44,skc46)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[clause34,clause32]) ).
cnf(c252,plain,
( in(skc42,skc44,skc46)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[clause34,clause30]) ).
cnf(c251,plain,
( in(skc42,skc44,skc46)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[clause34,clause31]) ).
cnf(c250,plain,
( in(skc42,skc44,skc46)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause34,clause29]) ).
cnf(c249,plain,
( in(skc42,skc44,skc46)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause34,clause28]) ).
cnf(c248,plain,
( in(skc42,skc44,skc46)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[clause34,clause27]) ).
cnf(c247,plain,
( in(skc42,skc44,skc46)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[clause34,clause26]) ).
cnf(c246,plain,
( in(skc42,skc44,skc46)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[clause34,clause25]) ).
cnf(c245,plain,
( in(skc42,skc44,skc46)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[clause34,clause24]) ).
cnf(c244,plain,
( in(skc42,skc44,skc46)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[clause34,clause23]) ).
cnf(c243,plain,
( in(skc42,skc44,skc46)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[clause34,clause19]) ).
cnf(c242,plain,
( in(skc42,skc44,skc46)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[clause34,clause21]) ).
cnf(c241,plain,
( in(skc42,skc44,skc46)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[clause34,clause20]) ).
cnf(c240,plain,
( in(skc42,skc44,skc46)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[clause34,clause22]) ).
cnf(c239,plain,
( agent(skc42,skc44,skc46)
| event(skc12,skc14) ),
inference(resolution,[status(thm)],[clause33,clause18]) ).
cnf(c238,plain,
( agent(skc42,skc44,skc46)
| ssSkP0(skc13,skc12) ),
inference(resolution,[status(thm)],[clause33,clause32]) ).
cnf(c237,plain,
( agent(skc42,skc44,skc46)
| group(skc12,skc13) ),
inference(resolution,[status(thm)],[clause33,clause30]) ).
cnf(c236,plain,
( agent(skc42,skc44,skc46)
| two(skc12,skc13) ),
inference(resolution,[status(thm)],[clause33,clause31]) ).
cnf(c235,plain,
( agent(skc42,skc44,skc46)
| placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause33,clause29]) ).
cnf(c234,plain,
( agent(skc42,skc44,skc46)
| hollywood_placename(skc12,skc16) ),
inference(resolution,[status(thm)],[clause33,clause28]) ).
cnf(c233,plain,
( agent(skc42,skc44,skc46)
| city(skc12,skc15) ),
inference(resolution,[status(thm)],[clause33,clause27]) ).
cnf(c232,plain,
( agent(skc42,skc44,skc46)
| street(skc12,skc15) ),
inference(resolution,[status(thm)],[clause33,clause26]) ).
cnf(c231,plain,
( agent(skc42,skc44,skc46)
| lonely(skc12,skc15) ),
inference(resolution,[status(thm)],[clause33,clause25]) ).
cnf(c230,plain,
( agent(skc42,skc44,skc46)
| chevy(skc12,skc17) ),
inference(resolution,[status(thm)],[clause33,clause24]) ).
cnf(c229,plain,
( agent(skc42,skc44,skc46)
| white(skc12,skc17) ),
inference(resolution,[status(thm)],[clause33,clause23]) ).
cnf(c228,plain,
( agent(skc42,skc44,skc46)
| present(skc12,skc14) ),
inference(resolution,[status(thm)],[clause33,clause19]) ).
cnf(c227,plain,
( agent(skc42,skc44,skc46)
| old(skc12,skc17) ),
inference(resolution,[status(thm)],[clause33,clause21]) ).
cnf(c226,plain,
( agent(skc42,skc44,skc46)
| barrel(skc12,skc14) ),
inference(resolution,[status(thm)],[clause33,clause20]) ).
cnf(c225,plain,
( agent(skc42,skc44,skc46)
| dirty(skc12,skc17) ),
inference(resolution,[status(thm)],[clause33,clause22]) ).
cnf(c224,plain,
( ssSkP0(skc13,skc12)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause32,clause3]) ).
cnf(c223,plain,
( ssSkP0(skc13,skc12)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause32,clause10]) ).
cnf(c222,plain,
( ssSkP0(skc13,skc12)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause32,clause8]) ).
cnf(c221,plain,
( ssSkP0(skc13,skc12)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause32,clause15]) ).
cnf(c220,plain,
( ssSkP0(skc13,skc12)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause32,clause5]) ).
cnf(c219,plain,
( ssSkP0(skc13,skc12)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause32,clause12]) ).
cnf(c218,plain,
( ssSkP0(skc13,skc12)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause32,clause11]) ).
cnf(c217,plain,
( ssSkP0(skc13,skc12)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause32,clause13]) ).
cnf(c215,plain,
( ssSkP0(skc13,skc12)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause32,clause9]) ).
cnf(c214,plain,
( ssSkP0(skc13,skc12)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause32,clause6]) ).
cnf(c213,plain,
( ssSkP0(skc13,skc12)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause32,clause16]) ).
cnf(c212,plain,
( ssSkP0(skc13,skc12)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause32,clause4]) ).
cnf(c211,plain,
( ssSkP0(skc13,skc12)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause32,clause7]) ).
cnf(c210,plain,
( ssSkP0(skc13,skc12)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause32,clause14]) ).
cnf(c209,plain,
( two(skc12,skc13)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause31,clause3]) ).
cnf(c208,plain,
( two(skc12,skc13)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause31,clause10]) ).
cnf(c207,plain,
( two(skc12,skc13)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause31,clause8]) ).
cnf(c206,plain,
( two(skc12,skc13)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause31,clause15]) ).
cnf(c205,plain,
( two(skc12,skc13)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause31,clause5]) ).
cnf(c204,plain,
( two(skc12,skc13)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause31,clause12]) ).
cnf(c203,plain,
( two(skc12,skc13)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause31,clause11]) ).
cnf(c202,plain,
( two(skc12,skc13)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause31,clause13]) ).
cnf(c200,plain,
( two(skc12,skc13)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause31,clause9]) ).
cnf(c199,plain,
( two(skc12,skc13)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause31,clause6]) ).
cnf(c198,plain,
( two(skc12,skc13)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause31,clause16]) ).
cnf(c197,plain,
( two(skc12,skc13)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause31,clause4]) ).
cnf(c196,plain,
( two(skc12,skc13)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause31,clause7]) ).
cnf(c195,plain,
( two(skc12,skc13)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause31,clause14]) ).
cnf(c194,plain,
( group(skc12,skc13)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause30,clause3]) ).
cnf(c193,plain,
( group(skc12,skc13)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause30,clause10]) ).
cnf(c192,plain,
( group(skc12,skc13)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause30,clause8]) ).
cnf(c191,plain,
( group(skc12,skc13)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause30,clause15]) ).
cnf(c190,plain,
( group(skc12,skc13)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause30,clause5]) ).
cnf(c189,plain,
( group(skc12,skc13)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause30,clause12]) ).
cnf(c188,plain,
( group(skc12,skc13)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause30,clause11]) ).
cnf(c187,plain,
( group(skc12,skc13)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause30,clause13]) ).
cnf(c185,plain,
( group(skc12,skc13)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause30,clause9]) ).
cnf(c184,plain,
( group(skc12,skc13)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause30,clause6]) ).
cnf(c183,plain,
( group(skc12,skc13)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause30,clause16]) ).
cnf(c182,plain,
( group(skc12,skc13)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause30,clause4]) ).
cnf(c181,plain,
( group(skc12,skc13)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause30,clause7]) ).
cnf(c180,plain,
( group(skc12,skc13)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause30,clause14]) ).
cnf(c179,plain,
( placename(skc12,skc16)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause29,clause3]) ).
cnf(c178,plain,
( placename(skc12,skc16)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause29,clause10]) ).
cnf(c177,plain,
( placename(skc12,skc16)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause29,clause8]) ).
cnf(c176,plain,
( placename(skc12,skc16)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause29,clause15]) ).
cnf(c175,plain,
( placename(skc12,skc16)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause29,clause5]) ).
cnf(c174,plain,
( placename(skc12,skc16)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause29,clause12]) ).
cnf(c173,plain,
( placename(skc12,skc16)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause29,clause11]) ).
cnf(c172,plain,
( placename(skc12,skc16)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause29,clause13]) ).
cnf(c170,plain,
( placename(skc12,skc16)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause29,clause9]) ).
cnf(c169,plain,
( placename(skc12,skc16)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause29,clause6]) ).
cnf(c168,plain,
( placename(skc12,skc16)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause29,clause16]) ).
cnf(c167,plain,
( placename(skc12,skc16)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause29,clause4]) ).
cnf(c166,plain,
( placename(skc12,skc16)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause29,clause7]) ).
cnf(c165,plain,
( placename(skc12,skc16)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause29,clause14]) ).
cnf(c164,plain,
( hollywood_placename(skc12,skc16)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause28,clause3]) ).
cnf(c163,plain,
( hollywood_placename(skc12,skc16)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause28,clause10]) ).
cnf(c162,plain,
( hollywood_placename(skc12,skc16)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause28,clause8]) ).
cnf(c161,plain,
( hollywood_placename(skc12,skc16)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause28,clause15]) ).
cnf(c160,plain,
( hollywood_placename(skc12,skc16)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause28,clause5]) ).
cnf(c159,plain,
( hollywood_placename(skc12,skc16)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause28,clause12]) ).
cnf(c158,plain,
( hollywood_placename(skc12,skc16)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause28,clause11]) ).
cnf(c157,plain,
( hollywood_placename(skc12,skc16)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause28,clause13]) ).
cnf(c155,plain,
( hollywood_placename(skc12,skc16)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause28,clause9]) ).
cnf(c154,plain,
( hollywood_placename(skc12,skc16)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause28,clause6]) ).
cnf(c153,plain,
( hollywood_placename(skc12,skc16)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause28,clause16]) ).
cnf(c152,plain,
( hollywood_placename(skc12,skc16)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause28,clause4]) ).
cnf(c151,plain,
( hollywood_placename(skc12,skc16)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause28,clause7]) ).
cnf(c150,plain,
( hollywood_placename(skc12,skc16)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause28,clause14]) ).
cnf(c149,plain,
( city(skc12,skc15)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause27,clause3]) ).
cnf(c148,plain,
( city(skc12,skc15)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause27,clause10]) ).
cnf(c147,plain,
( city(skc12,skc15)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause27,clause8]) ).
cnf(c146,plain,
( city(skc12,skc15)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause27,clause15]) ).
cnf(c145,plain,
( city(skc12,skc15)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause27,clause5]) ).
cnf(c144,plain,
( city(skc12,skc15)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause27,clause12]) ).
cnf(c143,plain,
( city(skc12,skc15)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause27,clause11]) ).
cnf(c142,plain,
( city(skc12,skc15)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause27,clause13]) ).
cnf(c140,plain,
( city(skc12,skc15)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause27,clause9]) ).
cnf(c139,plain,
( city(skc12,skc15)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause27,clause6]) ).
cnf(c138,plain,
( city(skc12,skc15)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause27,clause16]) ).
cnf(c137,plain,
( city(skc12,skc15)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause27,clause4]) ).
cnf(c136,plain,
( city(skc12,skc15)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause27,clause7]) ).
cnf(c135,plain,
( city(skc12,skc15)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause27,clause14]) ).
cnf(c134,plain,
( street(skc12,skc15)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause26,clause3]) ).
cnf(c133,plain,
( street(skc12,skc15)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause26,clause10]) ).
cnf(c132,plain,
( street(skc12,skc15)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause26,clause8]) ).
cnf(c131,plain,
( street(skc12,skc15)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause26,clause15]) ).
cnf(c130,plain,
( street(skc12,skc15)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause26,clause5]) ).
cnf(c129,plain,
( street(skc12,skc15)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause26,clause12]) ).
cnf(c128,plain,
( street(skc12,skc15)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause26,clause11]) ).
cnf(c127,plain,
( street(skc12,skc15)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause26,clause13]) ).
cnf(c125,plain,
( street(skc12,skc15)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause26,clause9]) ).
cnf(c124,plain,
( street(skc12,skc15)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause26,clause6]) ).
cnf(c123,plain,
( street(skc12,skc15)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause26,clause16]) ).
cnf(c122,plain,
( street(skc12,skc15)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause26,clause4]) ).
cnf(c121,plain,
( street(skc12,skc15)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause26,clause7]) ).
cnf(c120,plain,
( street(skc12,skc15)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause26,clause14]) ).
cnf(c119,plain,
( lonely(skc12,skc15)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause25,clause3]) ).
cnf(c118,plain,
( lonely(skc12,skc15)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause25,clause10]) ).
cnf(c117,plain,
( lonely(skc12,skc15)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause25,clause8]) ).
cnf(c116,plain,
( lonely(skc12,skc15)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause25,clause15]) ).
cnf(c115,plain,
( lonely(skc12,skc15)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause25,clause5]) ).
cnf(c114,plain,
( lonely(skc12,skc15)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause25,clause12]) ).
cnf(c113,plain,
( lonely(skc12,skc15)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause25,clause11]) ).
cnf(c112,plain,
( lonely(skc12,skc15)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause25,clause13]) ).
cnf(c110,plain,
( lonely(skc12,skc15)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause25,clause9]) ).
cnf(c109,plain,
( lonely(skc12,skc15)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause25,clause6]) ).
cnf(c108,plain,
( lonely(skc12,skc15)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause25,clause16]) ).
cnf(c107,plain,
( lonely(skc12,skc15)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause25,clause4]) ).
cnf(c106,plain,
( lonely(skc12,skc15)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause25,clause7]) ).
cnf(c105,plain,
( lonely(skc12,skc15)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause25,clause14]) ).
cnf(c104,plain,
( chevy(skc12,skc17)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause24,clause3]) ).
cnf(c103,plain,
( chevy(skc12,skc17)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause24,clause10]) ).
cnf(c102,plain,
( chevy(skc12,skc17)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause24,clause8]) ).
cnf(c101,plain,
( chevy(skc12,skc17)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause24,clause15]) ).
cnf(c100,plain,
( chevy(skc12,skc17)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause24,clause5]) ).
cnf(c99,plain,
( chevy(skc12,skc17)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause24,clause12]) ).
cnf(c98,plain,
( chevy(skc12,skc17)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause24,clause11]) ).
cnf(c97,plain,
( chevy(skc12,skc17)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause24,clause13]) ).
cnf(c95,plain,
( chevy(skc12,skc17)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause24,clause9]) ).
cnf(c94,plain,
( chevy(skc12,skc17)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause24,clause6]) ).
cnf(c93,plain,
( chevy(skc12,skc17)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause24,clause16]) ).
cnf(c92,plain,
( chevy(skc12,skc17)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause24,clause4]) ).
cnf(c91,plain,
( chevy(skc12,skc17)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause24,clause7]) ).
cnf(c90,plain,
( chevy(skc12,skc17)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause24,clause14]) ).
cnf(c89,plain,
( white(skc12,skc17)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause23,clause3]) ).
cnf(c88,plain,
( white(skc12,skc17)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause23,clause10]) ).
cnf(c87,plain,
( white(skc12,skc17)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause23,clause8]) ).
cnf(c86,plain,
( white(skc12,skc17)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause23,clause15]) ).
cnf(c85,plain,
( white(skc12,skc17)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause23,clause5]) ).
cnf(c84,plain,
( white(skc12,skc17)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause23,clause12]) ).
cnf(clause60,negated_conjecture,
( ~ city(X70,X68)
| ~ chevy(X70,X68)
| ~ white(X70,X68)
| ~ dirty(X70,X68)
| ~ old(X70,X68)
| ~ agent(X70,X67,X68)
| ~ in(X70,X67,X68)
| ~ placename(X70,X73)
| ~ hollywood_placename(X70,X73)
| ~ of(X70,X73,X68)
| ~ event(X70,X67)
| ~ present(X70,X67)
| ~ barrel(X70,X67)
| ~ down(X70,X67,X71)
| ~ lonely(X70,X71)
| ~ street(X70,X71)
| ~ young(X70,skf9(X70,X72))
| ~ fellow(X70,skf9(X70,X72))
| ~ group(X70,X69)
| ~ two(X70,X69)
| ~ ssSkP1(X69,X70)
| ~ actual_world(X70)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
cnf(c83,plain,
( white(skc12,skc17)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause23,clause11]) ).
cnf(c82,plain,
( white(skc12,skc17)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause23,clause13]) ).
cnf(c80,plain,
( white(skc12,skc17)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause23,clause9]) ).
cnf(c79,plain,
( white(skc12,skc17)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause23,clause6]) ).
cnf(clause59,negated_conjecture,
( ~ event(X63,X61)
| ~ present(X63,X61)
| ~ barrel(X63,X61)
| ~ agent(X63,X61,X60)
| ~ old(X63,X60)
| ~ dirty(X63,X60)
| ~ white(X63,X60)
| ~ chevy(X63,X60)
| ~ in(X63,X61,X66)
| ~ down(X63,X61,X66)
| ~ lonely(X63,X66)
| ~ street(X63,X66)
| ~ city(X63,X66)
| ~ of(X63,X64,X66)
| ~ hollywood_placename(X63,X64)
| ~ placename(X63,X64)
| ~ young(X63,skf21(X63,X65))
| ~ fellow(X63,skf21(X63,X65))
| ~ group(X63,X62)
| ~ two(X63,X62)
| ~ ssSkP0(X62,X63)
| ~ actual_world(X63)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
cnf(c78,plain,
( white(skc12,skc17)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause23,clause16]) ).
cnf(c77,plain,
( white(skc12,skc17)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause23,clause4]) ).
cnf(c76,plain,
( white(skc12,skc17)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause23,clause7]) ).
cnf(c75,plain,
( white(skc12,skc17)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause23,clause14]) ).
cnf(c74,plain,
( dirty(skc12,skc17)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause22,clause3]) ).
cnf(c73,plain,
( dirty(skc12,skc17)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause22,clause10]) ).
cnf(c72,plain,
( dirty(skc12,skc17)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause22,clause8]) ).
cnf(c71,plain,
( dirty(skc12,skc17)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause22,clause15]) ).
cnf(c70,plain,
( dirty(skc12,skc17)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause22,clause5]) ).
cnf(c69,plain,
( dirty(skc12,skc17)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause22,clause12]) ).
cnf(c68,plain,
( dirty(skc12,skc17)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause22,clause11]) ).
cnf(c67,plain,
( dirty(skc12,skc17)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause22,clause13]) ).
cnf(c65,plain,
( dirty(skc12,skc17)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause22,clause9]) ).
cnf(c64,plain,
( dirty(skc12,skc17)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause22,clause6]) ).
cnf(clause56,negated_conjecture,
( ~ frontseat(X45,X44)
| ~ in(X45,X44,X44)
| ~ be(X45,X43,skf19(X45,X47),X44)
| ~ state(X45,X43)
| ssSkP1(X46,X45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(c63,plain,
( dirty(skc12,skc17)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause22,clause16]) ).
cnf(c62,plain,
( dirty(skc12,skc17)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause22,clause4]) ).
cnf(c61,plain,
( dirty(skc12,skc17)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause22,clause7]) ).
cnf(c60,plain,
( dirty(skc12,skc17)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause22,clause14]) ).
cnf(c59,plain,
( old(skc12,skc17)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause21,clause3]) ).
cnf(c58,plain,
( old(skc12,skc17)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause21,clause10]) ).
cnf(c57,plain,
( old(skc12,skc17)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause21,clause8]) ).
cnf(c56,plain,
( old(skc12,skc17)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause21,clause15]) ).
cnf(c55,plain,
( old(skc12,skc17)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause21,clause5]) ).
cnf(c54,plain,
( old(skc12,skc17)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause21,clause12]) ).
cnf(c53,plain,
( old(skc12,skc17)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause21,clause11]) ).
cnf(c52,plain,
( old(skc12,skc17)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause21,clause13]) ).
cnf(c50,plain,
( old(skc12,skc17)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause21,clause9]) ).
cnf(c49,plain,
( old(skc12,skc17)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause21,clause6]) ).
cnf(c48,plain,
( old(skc12,skc17)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause21,clause16]) ).
cnf(c47,plain,
( old(skc12,skc17)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause21,clause4]) ).
cnf(c46,plain,
( old(skc12,skc17)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause21,clause7]) ).
cnf(c45,plain,
( old(skc12,skc17)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause21,clause14]) ).
cnf(c44,plain,
( barrel(skc12,skc14)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause20,clause3]) ).
cnf(c43,plain,
( barrel(skc12,skc14)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause20,clause10]) ).
cnf(c42,plain,
( barrel(skc12,skc14)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause20,clause8]) ).
cnf(c41,plain,
( barrel(skc12,skc14)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause20,clause15]) ).
cnf(c40,plain,
( barrel(skc12,skc14)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause20,clause5]) ).
cnf(c39,plain,
( barrel(skc12,skc14)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause20,clause12]) ).
cnf(c38,plain,
( barrel(skc12,skc14)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause20,clause11]) ).
cnf(c37,plain,
( barrel(skc12,skc14)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause20,clause13]) ).
cnf(c35,plain,
( barrel(skc12,skc14)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause20,clause9]) ).
cnf(c34,plain,
( barrel(skc12,skc14)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause20,clause6]) ).
cnf(c33,plain,
( barrel(skc12,skc14)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause20,clause16]) ).
cnf(c32,plain,
( barrel(skc12,skc14)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause20,clause4]) ).
cnf(c31,plain,
( barrel(skc12,skc14)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause20,clause7]) ).
cnf(c30,plain,
( barrel(skc12,skc14)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause20,clause14]) ).
cnf(c29,plain,
( present(skc12,skc14)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause19,clause3]) ).
cnf(c28,plain,
( present(skc12,skc14)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause19,clause10]) ).
cnf(c27,plain,
( present(skc12,skc14)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause19,clause8]) ).
cnf(c26,plain,
( present(skc12,skc14)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause19,clause15]) ).
cnf(c25,plain,
( present(skc12,skc14)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause19,clause5]) ).
cnf(c24,plain,
( present(skc12,skc14)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause19,clause12]) ).
cnf(c23,plain,
( present(skc12,skc14)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause19,clause11]) ).
cnf(c22,plain,
( present(skc12,skc14)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause19,clause13]) ).
cnf(c20,plain,
( present(skc12,skc14)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause19,clause9]) ).
cnf(c19,plain,
( present(skc12,skc14)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause19,clause6]) ).
cnf(c18,plain,
( present(skc12,skc14)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause19,clause16]) ).
cnf(c17,plain,
( present(skc12,skc14)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause19,clause4]) ).
cnf(c16,plain,
( present(skc12,skc14)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause19,clause7]) ).
cnf(c15,plain,
( present(skc12,skc14)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause19,clause14]) ).
cnf(c14,plain,
( event(skc12,skc14)
| city(skc42,skc46) ),
inference(resolution,[status(thm)],[clause18,clause3]) ).
cnf(c13,plain,
( event(skc12,skc14)
| event(skc42,skc44) ),
inference(resolution,[status(thm)],[clause18,clause10]) ).
cnf(c12,plain,
( event(skc12,skc14)
| placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause18,clause8]) ).
cnf(c11,plain,
( event(skc12,skc14)
| group(skc42,skc43) ),
inference(resolution,[status(thm)],[clause18,clause15]) ).
cnf(c10,plain,
( event(skc12,skc14)
| white(skc42,skc46) ),
inference(resolution,[status(thm)],[clause18,clause5]) ).
cnf(c9,plain,
( event(skc12,skc14)
| barrel(skc42,skc44) ),
inference(resolution,[status(thm)],[clause18,clause12]) ).
cnf(c8,plain,
( event(skc12,skc14)
| present(skc42,skc44) ),
inference(resolution,[status(thm)],[clause18,clause11]) ).
cnf(c7,plain,
( event(skc12,skc14)
| lonely(skc42,skc45) ),
inference(resolution,[status(thm)],[clause18,clause13]) ).
cnf(c5,plain,
( event(skc12,skc14)
| hollywood_placename(skc42,skc47) ),
inference(resolution,[status(thm)],[clause18,clause9]) ).
cnf(c4,plain,
( event(skc12,skc14)
| dirty(skc42,skc46) ),
inference(resolution,[status(thm)],[clause18,clause6]) ).
cnf(c3,plain,
( event(skc12,skc14)
| two(skc42,skc43) ),
inference(resolution,[status(thm)],[clause18,clause16]) ).
cnf(c2,plain,
( event(skc12,skc14)
| chevy(skc42,skc46) ),
inference(resolution,[status(thm)],[clause18,clause4]) ).
cnf(c1,plain,
( event(skc12,skc14)
| old(skc42,skc46) ),
inference(resolution,[status(thm)],[clause18,clause7]) ).
cnf(c0,plain,
( event(skc12,skc14)
| street(skc42,skc45) ),
inference(resolution,[status(thm)],[clause18,clause14]) ).
cnf(clause41,negated_conjecture,
( ssSkP0(X2,X4)
| frontseat(X4,skf14(X4,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(clause2,negated_conjecture,
actual_world(skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause1,negated_conjecture,
actual_world(skc42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP133-1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 13:25:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 6.90/7.10 % Version: 1.5
% 6.90/7.10 % SZS status Satisfiable
% 6.90/7.10 % SZS output start Saturation
% See solution above
% 6.90/7.13
% 6.90/7.13 % Initial clauses : 60
% 6.90/7.13 % Processed clauses : 716
% 6.90/7.13 % Factors computed : 0
% 6.90/7.13 % Resolvents computed: 2400
% 6.90/7.13 % Tautologies deleted: 20
% 6.90/7.13 % Forward subsumed : 1724
% 6.90/7.13 % Backward subsumed : 25
% 6.90/7.13 % -------- CPU Time ---------
% 6.90/7.13 % User time : 6.768 s
% 6.90/7.13 % System time : 0.013 s
% 6.90/7.13 % Total time : 6.781 s
%------------------------------------------------------------------------------