%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP118-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:10 EDT 2024
% Result : Satisfiable 5.78s 5.94s
% Output : Saturation 5.79s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
actual_world(skc16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause3,negated_conjecture,
( ssSkC0
| old(skc16,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause2,negated_conjecture,
actual_world(skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause23,negated_conjecture,
( ~ ssSkC0
| old(skc11,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c100,plain,
( old(skc11,skc13)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause23,clause3]) ).
cnf(clause24,negated_conjecture,
( ~ ssSkC0
| dirty(skc11,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c112,plain,
( dirty(skc11,skc13)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause24,clause3]) ).
cnf(clause25,negated_conjecture,
( ~ ssSkC0
| white(skc11,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c124,plain,
( white(skc11,skc13)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause25,clause3]) ).
cnf(clause26,negated_conjecture,
( ~ ssSkC0
| chevy(skc11,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c136,plain,
( chevy(skc11,skc13)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause26,clause3]) ).
cnf(clause22,negated_conjecture,
( ~ ssSkC0
| barrel(skc11,skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c88,plain,
( barrel(skc11,skc12)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause22,clause3]) ).
cnf(clause21,negated_conjecture,
( ~ ssSkC0
| present(skc11,skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c76,plain,
( present(skc11,skc12)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause21,clause3]) ).
cnf(clause20,negated_conjecture,
( ~ ssSkC0
| event(skc11,skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c64,plain,
( event(skc11,skc12)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause20,clause3]) ).
cnf(clause19,negated_conjecture,
( ~ ssSkC0
| hollywood_placename(skc11,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c52,plain,
( hollywood_placename(skc11,skc15)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause19,clause3]) ).
cnf(clause18,negated_conjecture,
( ~ ssSkC0
| placename(skc11,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c40,plain,
( placename(skc11,skc15)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause18,clause3]) ).
cnf(clause15,negated_conjecture,
( ~ ssSkC0
| city(skc11,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c4,plain,
( city(skc11,skc14)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause15,clause3]) ).
cnf(clause16,negated_conjecture,
( ~ ssSkC0
| street(skc11,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c16,plain,
( street(skc11,skc14)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause16,clause3]) ).
cnf(clause17,negated_conjecture,
( ~ ssSkC0
| lonely(skc11,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c28,plain,
( lonely(skc11,skc14)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause17,clause3]) ).
cnf(clause34,negated_conjecture,
( ~ ssSkC0
| agent(skc11,skc12,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c246,plain,
( agent(skc11,skc12,skc13)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause34,clause3]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| in(skc11,skc12,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c214,plain,
( in(skc11,skc12,skc14)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause32,clause3]) ).
cnf(clause33,negated_conjecture,
( ~ ssSkC0
| of(skc11,skc15,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c230,plain,
( of(skc11,skc15,skc14)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause33,clause3]) ).
cnf(clause36,negated_conjecture,
( ~ agent(X7,X10,X11)
| ~ old(X7,X11)
| ~ dirty(X7,X11)
| ~ white(X7,X11)
| ~ chevy(X7,X11)
| ~ barrel(X7,X10)
| ~ present(X7,X10)
| ~ event(X7,X10)
| ~ hollywood_placename(X7,X12)
| ~ placename(X7,X12)
| ~ in(X7,X10,X8)
| ~ city(X7,X8)
| ~ of(X7,X12,X8)
| ~ street(X7,X9)
| ~ lonely(X7,X9)
| ~ down(X7,X10,X9)
| ~ actual_world(X7)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(clause31,negated_conjecture,
( ~ ssSkC0
| down(skc11,skc12,skc14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c198,plain,
( down(skc11,skc12,skc14)
| old(skc16,skc21) ),
inference(resolution,[status(thm)],[clause31,clause3]) ).
cnf(c286,plain,
( old(skc16,skc21)
| ~ agent(skc11,skc12,X93)
| ~ old(skc11,X93)
| ~ dirty(skc11,X93)
| ~ white(skc11,X93)
| ~ chevy(skc11,X93)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X94)
| ~ placename(skc11,X94)
| ~ in(skc11,skc12,X92)
| ~ city(skc11,X92)
| ~ of(skc11,X94,X92)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c198,clause36]) ).
cnf(c663,plain,
( old(skc16,skc21)
| ~ agent(skc11,skc12,X272)
| ~ old(skc11,X272)
| ~ dirty(skc11,X272)
| ~ white(skc11,X272)
| ~ chevy(skc11,X272)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c286,c230]) ).
cnf(c1572,plain,
( old(skc16,skc21)
| ~ agent(skc11,skc12,X348)
| ~ old(skc11,X348)
| ~ dirty(skc11,X348)
| ~ white(skc11,X348)
| ~ chevy(skc11,X348)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c663,c214]) ).
cnf(c2372,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1572,c246]) ).
cnf(c2390,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2372,c28]) ).
cnf(c2400,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2390,c16]) ).
cnf(c2405,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2400,c4]) ).
cnf(c2424,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2405,c40]) ).
cnf(c2429,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2424,c52]) ).
cnf(c2443,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2429,c64]) ).
cnf(c2461,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2443,c76]) ).
cnf(c2475,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2461,c88]) ).
cnf(c2482,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2475,c136]) ).
cnf(c2492,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2482,c124]) ).
cnf(c2511,plain,
( old(skc16,skc21)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2492,c112]) ).
cnf(c2520,plain,
( old(skc16,skc21)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2511,c100]) ).
cnf(c2524,plain,
( old(skc16,skc21)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2520,clause2]) ).
cnf(c2539,plain,
old(skc16,skc21),
inference(resolution,[status(thm)],[c2524,clause3]) ).
cnf(clause4,negated_conjecture,
( ssSkC0
| dirty(skc16,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c97,plain,
( old(skc11,skc13)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause23,clause4]) ).
cnf(c109,plain,
( dirty(skc11,skc13)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause24,clause4]) ).
cnf(c121,plain,
( white(skc11,skc13)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause25,clause4]) ).
cnf(c133,plain,
( chevy(skc11,skc13)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause26,clause4]) ).
cnf(c85,plain,
( barrel(skc11,skc12)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause22,clause4]) ).
cnf(c73,plain,
( present(skc11,skc12)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause21,clause4]) ).
cnf(c61,plain,
( event(skc11,skc12)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause20,clause4]) ).
cnf(c49,plain,
( hollywood_placename(skc11,skc15)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause19,clause4]) ).
cnf(c37,plain,
( placename(skc11,skc15)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause18,clause4]) ).
cnf(c1,plain,
( city(skc11,skc14)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause15,clause4]) ).
cnf(c13,plain,
( street(skc11,skc14)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause16,clause4]) ).
cnf(c25,plain,
( lonely(skc11,skc14)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause17,clause4]) ).
cnf(c242,plain,
( agent(skc11,skc12,skc13)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause34,clause4]) ).
cnf(c210,plain,
( in(skc11,skc12,skc14)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause32,clause4]) ).
cnf(c226,plain,
( of(skc11,skc15,skc14)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause33,clause4]) ).
cnf(c194,plain,
( down(skc11,skc12,skc14)
| dirty(skc16,skc21) ),
inference(resolution,[status(thm)],[clause31,clause4]) ).
cnf(c283,plain,
( dirty(skc16,skc21)
| ~ agent(skc11,skc12,X84)
| ~ old(skc11,X84)
| ~ dirty(skc11,X84)
| ~ white(skc11,X84)
| ~ chevy(skc11,X84)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X85)
| ~ placename(skc11,X85)
| ~ in(skc11,skc12,X83)
| ~ city(skc11,X83)
| ~ of(skc11,X85,X83)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c194,clause36]) ).
cnf(c620,plain,
( dirty(skc16,skc21)
| ~ agent(skc11,skc12,X195)
| ~ old(skc11,X195)
| ~ dirty(skc11,X195)
| ~ white(skc11,X195)
| ~ chevy(skc11,X195)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c283,c226]) ).
cnf(c849,plain,
( dirty(skc16,skc21)
| ~ agent(skc11,skc12,X196)
| ~ old(skc11,X196)
| ~ dirty(skc11,X196)
| ~ white(skc11,X196)
| ~ chevy(skc11,X196)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c620,c210]) ).
cnf(c865,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c849,c242]) ).
cnf(c872,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c865,c25]) ).
cnf(c886,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c872,c13]) ).
cnf(c907,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c886,c1]) ).
cnf(c922,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c907,c37]) ).
cnf(c939,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c922,c49]) ).
cnf(c943,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c939,c61]) ).
cnf(c960,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c943,c73]) ).
cnf(c984,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c960,c85]) ).
cnf(c991,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c984,c133]) ).
cnf(c1017,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c991,c121]) ).
cnf(c1028,plain,
( dirty(skc16,skc21)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1017,c109]) ).
cnf(c1041,plain,
( dirty(skc16,skc21)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1028,c97]) ).
cnf(c1048,plain,
( dirty(skc16,skc21)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1041,clause2]) ).
cnf(c1050,plain,
dirty(skc16,skc21),
inference(resolution,[status(thm)],[c1048,clause4]) ).
cnf(clause5,negated_conjecture,
( ssSkC0
| white(skc16,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c102,plain,
( old(skc11,skc13)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause23,clause5]) ).
cnf(c114,plain,
( dirty(skc11,skc13)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause24,clause5]) ).
cnf(c126,plain,
( white(skc11,skc13)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause25,clause5]) ).
cnf(c138,plain,
( chevy(skc11,skc13)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause26,clause5]) ).
cnf(c90,plain,
( barrel(skc11,skc12)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause22,clause5]) ).
cnf(c78,plain,
( present(skc11,skc12)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause21,clause5]) ).
cnf(c66,plain,
( event(skc11,skc12)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause20,clause5]) ).
cnf(c54,plain,
( hollywood_placename(skc11,skc15)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause19,clause5]) ).
cnf(c42,plain,
( placename(skc11,skc15)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause18,clause5]) ).
cnf(c6,plain,
( city(skc11,skc14)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause15,clause5]) ).
cnf(c18,plain,
( street(skc11,skc14)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause16,clause5]) ).
cnf(c30,plain,
( lonely(skc11,skc14)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause17,clause5]) ).
cnf(c249,plain,
( agent(skc11,skc12,skc13)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause34,clause5]) ).
cnf(c217,plain,
( in(skc11,skc12,skc14)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause32,clause5]) ).
cnf(c233,plain,
( of(skc11,skc15,skc14)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause33,clause5]) ).
cnf(c201,plain,
( down(skc11,skc12,skc14)
| white(skc16,skc21) ),
inference(resolution,[status(thm)],[clause31,clause5]) ).
cnf(c289,plain,
( white(skc16,skc21)
| ~ agent(skc11,skc12,X102)
| ~ old(skc11,X102)
| ~ dirty(skc11,X102)
| ~ white(skc11,X102)
| ~ chevy(skc11,X102)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X103)
| ~ placename(skc11,X103)
| ~ in(skc11,skc12,X101)
| ~ city(skc11,X101)
| ~ of(skc11,X103,X101)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c201,clause36]) ).
cnf(c712,plain,
( white(skc16,skc21)
| ~ agent(skc11,skc12,X323)
| ~ old(skc11,X323)
| ~ dirty(skc11,X323)
| ~ white(skc11,X323)
| ~ chevy(skc11,X323)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c289,c233]) ).
cnf(c2285,plain,
( white(skc16,skc21)
| ~ agent(skc11,skc12,X411)
| ~ old(skc11,X411)
| ~ dirty(skc11,X411)
| ~ white(skc11,X411)
| ~ chevy(skc11,X411)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c712,c217]) ).
cnf(c2790,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2285,c249]) ).
cnf(c2798,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2790,c30]) ).
cnf(c2817,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2798,c18]) ).
cnf(c2823,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2817,c6]) ).
cnf(c2830,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2823,c42]) ).
cnf(c2845,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2830,c54]) ).
cnf(c2854,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2845,c66]) ).
cnf(c2859,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2854,c78]) ).
cnf(c2870,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2859,c90]) ).
cnf(c2890,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2870,c138]) ).
cnf(c2907,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2890,c126]) ).
cnf(c2915,plain,
( white(skc16,skc21)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2907,c114]) ).
cnf(c2921,plain,
( white(skc16,skc21)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2915,c102]) ).
cnf(c2928,plain,
( white(skc16,skc21)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2921,clause2]) ).
cnf(c2932,plain,
white(skc16,skc21),
inference(resolution,[status(thm)],[c2928,clause5]) ).
cnf(clause6,negated_conjecture,
( ssSkC0
| chevy(skc16,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c105,plain,
( old(skc11,skc13)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause23,clause6]) ).
cnf(c117,plain,
( dirty(skc11,skc13)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause24,clause6]) ).
cnf(c129,plain,
( white(skc11,skc13)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause25,clause6]) ).
cnf(c141,plain,
( chevy(skc11,skc13)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause26,clause6]) ).
cnf(c93,plain,
( barrel(skc11,skc12)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause22,clause6]) ).
cnf(c81,plain,
( present(skc11,skc12)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause21,clause6]) ).
cnf(c69,plain,
( event(skc11,skc12)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause20,clause6]) ).
cnf(c57,plain,
( hollywood_placename(skc11,skc15)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause19,clause6]) ).
cnf(c45,plain,
( placename(skc11,skc15)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause18,clause6]) ).
cnf(c9,plain,
( city(skc11,skc14)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause15,clause6]) ).
cnf(c21,plain,
( street(skc11,skc14)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause16,clause6]) ).
cnf(c33,plain,
( lonely(skc11,skc14)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause17,clause6]) ).
cnf(c252,plain,
( agent(skc11,skc12,skc13)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause34,clause6]) ).
cnf(c220,plain,
( in(skc11,skc12,skc14)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause32,clause6]) ).
cnf(c236,plain,
( of(skc11,skc15,skc14)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause33,clause6]) ).
cnf(c204,plain,
( down(skc11,skc12,skc14)
| chevy(skc16,skc21) ),
inference(resolution,[status(thm)],[clause31,clause6]) ).
cnf(c292,plain,
( chevy(skc16,skc21)
| ~ agent(skc11,skc12,X111)
| ~ old(skc11,X111)
| ~ dirty(skc11,X111)
| ~ white(skc11,X111)
| ~ chevy(skc11,X111)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X112)
| ~ placename(skc11,X112)
| ~ in(skc11,skc12,X110)
| ~ city(skc11,X110)
| ~ of(skc11,X112,X110)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c204,clause36]) ).
cnf(c748,plain,
( chevy(skc16,skc21)
| ~ agent(skc11,skc12,X360)
| ~ old(skc11,X360)
| ~ dirty(skc11,X360)
| ~ white(skc11,X360)
| ~ chevy(skc11,X360)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c292,c236]) ).
cnf(c2576,plain,
( chevy(skc16,skc21)
| ~ agent(skc11,skc12,X486)
| ~ old(skc11,X486)
| ~ dirty(skc11,X486)
| ~ white(skc11,X486)
| ~ chevy(skc11,X486)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c748,c220]) ).
cnf(c3196,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2576,c252]) ).
cnf(c3205,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3196,c33]) ).
cnf(c3213,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3205,c21]) ).
cnf(c3217,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3213,c9]) ).
cnf(c3228,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3217,c45]) ).
cnf(c3237,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3228,c57]) ).
cnf(c3239,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3237,c69]) ).
cnf(c3246,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3239,c81]) ).
cnf(c3258,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3246,c93]) ).
cnf(c3261,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3258,c141]) ).
cnf(c3266,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3261,c129]) ).
cnf(c3273,plain,
( chevy(skc16,skc21)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3266,c117]) ).
cnf(c3284,plain,
( chevy(skc16,skc21)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3273,c105]) ).
cnf(c3287,plain,
( chevy(skc16,skc21)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3284,clause2]) ).
cnf(c3291,plain,
chevy(skc16,skc21),
inference(resolution,[status(thm)],[c3287,clause6]) ).
cnf(clause7,negated_conjecture,
( ssSkC0
| barrel(skc16,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c96,plain,
( old(skc11,skc13)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause23,clause7]) ).
cnf(c108,plain,
( dirty(skc11,skc13)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause24,clause7]) ).
cnf(c120,plain,
( white(skc11,skc13)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause25,clause7]) ).
cnf(c132,plain,
( chevy(skc11,skc13)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause26,clause7]) ).
cnf(c84,plain,
( barrel(skc11,skc12)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause22,clause7]) ).
cnf(c72,plain,
( present(skc11,skc12)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause21,clause7]) ).
cnf(c60,plain,
( event(skc11,skc12)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause20,clause7]) ).
cnf(c48,plain,
( hollywood_placename(skc11,skc15)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause19,clause7]) ).
cnf(c36,plain,
( placename(skc11,skc15)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause18,clause7]) ).
cnf(c0,plain,
( city(skc11,skc14)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause15,clause7]) ).
cnf(c12,plain,
( street(skc11,skc14)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause16,clause7]) ).
cnf(c24,plain,
( lonely(skc11,skc14)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause17,clause7]) ).
cnf(c241,plain,
( agent(skc11,skc12,skc13)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause34,clause7]) ).
cnf(c209,plain,
( in(skc11,skc12,skc14)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause32,clause7]) ).
cnf(c225,plain,
( of(skc11,skc15,skc14)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause33,clause7]) ).
cnf(c193,plain,
( down(skc11,skc12,skc14)
| barrel(skc16,skc17) ),
inference(resolution,[status(thm)],[clause31,clause7]) ).
cnf(c282,plain,
( barrel(skc16,skc17)
| ~ agent(skc11,skc12,X67)
| ~ old(skc11,X67)
| ~ dirty(skc11,X67)
| ~ white(skc11,X67)
| ~ chevy(skc11,X67)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X68)
| ~ placename(skc11,X68)
| ~ in(skc11,skc12,X66)
| ~ city(skc11,X66)
| ~ of(skc11,X68,X66)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c193,clause36]) ).
cnf(c371,plain,
( barrel(skc16,skc17)
| ~ agent(skc11,skc12,X69)
| ~ old(skc11,X69)
| ~ dirty(skc11,X69)
| ~ white(skc11,X69)
| ~ chevy(skc11,X69)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c282,c225]) ).
cnf(c373,plain,
( barrel(skc16,skc17)
| ~ agent(skc11,skc12,X70)
| ~ old(skc11,X70)
| ~ dirty(skc11,X70)
| ~ white(skc11,X70)
| ~ chevy(skc11,X70)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c371,c209]) ).
cnf(c390,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c373,c241]) ).
cnf(c413,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c390,c24]) ).
cnf(c426,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c413,c12]) ).
cnf(c450,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c426,c0]) ).
cnf(c467,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c450,c36]) ).
cnf(c483,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c467,c48]) ).
cnf(c487,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c483,c60]) ).
cnf(c508,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c487,c72]) ).
cnf(c529,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c508,c84]) ).
cnf(c538,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c529,c132]) ).
cnf(c549,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c538,c120]) ).
cnf(c565,plain,
( barrel(skc16,skc17)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c549,c108]) ).
cnf(c591,plain,
( barrel(skc16,skc17)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c565,c96]) ).
cnf(c596,plain,
( barrel(skc16,skc17)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c591,clause2]) ).
cnf(c598,plain,
barrel(skc16,skc17),
inference(resolution,[status(thm)],[c596,clause7]) ).
cnf(clause8,negated_conjecture,
( ssSkC0
| present(skc16,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c106,plain,
( old(skc11,skc13)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause23,clause8]) ).
cnf(c118,plain,
( dirty(skc11,skc13)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause24,clause8]) ).
cnf(c130,plain,
( white(skc11,skc13)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause25,clause8]) ).
cnf(c142,plain,
( chevy(skc11,skc13)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause26,clause8]) ).
cnf(c94,plain,
( barrel(skc11,skc12)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause22,clause8]) ).
cnf(c82,plain,
( present(skc11,skc12)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause21,clause8]) ).
cnf(c70,plain,
( event(skc11,skc12)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause20,clause8]) ).
cnf(c58,plain,
( hollywood_placename(skc11,skc15)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause19,clause8]) ).
cnf(c46,plain,
( placename(skc11,skc15)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause18,clause8]) ).
cnf(c10,plain,
( city(skc11,skc14)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause15,clause8]) ).
cnf(c22,plain,
( street(skc11,skc14)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause16,clause8]) ).
cnf(c34,plain,
( lonely(skc11,skc14)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause17,clause8]) ).
cnf(c254,plain,
( agent(skc11,skc12,skc13)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause34,clause8]) ).
cnf(c222,plain,
( in(skc11,skc12,skc14)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause32,clause8]) ).
cnf(c238,plain,
( of(skc11,skc15,skc14)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause33,clause8]) ).
cnf(c206,plain,
( down(skc11,skc12,skc14)
| present(skc16,skc17) ),
inference(resolution,[status(thm)],[clause31,clause8]) ).
cnf(c295,plain,
( present(skc16,skc17)
| ~ agent(skc11,skc12,X120)
| ~ old(skc11,X120)
| ~ dirty(skc11,X120)
| ~ white(skc11,X120)
| ~ chevy(skc11,X120)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X121)
| ~ placename(skc11,X121)
| ~ in(skc11,skc12,X119)
| ~ city(skc11,X119)
| ~ of(skc11,X121,X119)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c206,clause36]) ).
cnf(c786,plain,
( present(skc16,skc17)
| ~ agent(skc11,skc12,X399)
| ~ old(skc11,X399)
| ~ dirty(skc11,X399)
| ~ white(skc11,X399)
| ~ chevy(skc11,X399)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c295,c238]) ).
cnf(c2777,plain,
( present(skc16,skc17)
| ~ agent(skc11,skc12,X500)
| ~ old(skc11,X500)
| ~ dirty(skc11,X500)
| ~ white(skc11,X500)
| ~ chevy(skc11,X500)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c786,c222]) ).
cnf(c3297,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2777,c254]) ).
cnf(c3301,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3297,c34]) ).
cnf(c3312,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3301,c22]) ).
cnf(c3318,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3312,c10]) ).
cnf(c3320,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3318,c46]) ).
cnf(c3330,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3320,c58]) ).
cnf(c3333,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3330,c70]) ).
cnf(c3337,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3333,c82]) ).
cnf(c3348,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3337,c94]) ).
cnf(c3353,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3348,c142]) ).
cnf(c3360,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3353,c130]) ).
cnf(c3365,plain,
( present(skc16,skc17)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3360,c118]) ).
cnf(c3369,plain,
( present(skc16,skc17)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3365,c106]) ).
cnf(c3373,plain,
( present(skc16,skc17)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3369,clause2]) ).
cnf(c3378,plain,
present(skc16,skc17),
inference(resolution,[status(thm)],[c3373,clause8]) ).
cnf(clause9,negated_conjecture,
( ssSkC0
| event(skc16,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c104,plain,
( old(skc11,skc13)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause23,clause9]) ).
cnf(c116,plain,
( dirty(skc11,skc13)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause24,clause9]) ).
cnf(c128,plain,
( white(skc11,skc13)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause25,clause9]) ).
cnf(c140,plain,
( chevy(skc11,skc13)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause26,clause9]) ).
cnf(c92,plain,
( barrel(skc11,skc12)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause22,clause9]) ).
cnf(c80,plain,
( present(skc11,skc12)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause21,clause9]) ).
cnf(c68,plain,
( event(skc11,skc12)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause20,clause9]) ).
cnf(c56,plain,
( hollywood_placename(skc11,skc15)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause19,clause9]) ).
cnf(c44,plain,
( placename(skc11,skc15)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause18,clause9]) ).
cnf(c8,plain,
( city(skc11,skc14)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause15,clause9]) ).
cnf(c20,plain,
( street(skc11,skc14)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause16,clause9]) ).
cnf(c32,plain,
( lonely(skc11,skc14)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause17,clause9]) ).
cnf(c251,plain,
( agent(skc11,skc12,skc13)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause34,clause9]) ).
cnf(c219,plain,
( in(skc11,skc12,skc14)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause32,clause9]) ).
cnf(c235,plain,
( of(skc11,skc15,skc14)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause33,clause9]) ).
cnf(c203,plain,
( down(skc11,skc12,skc14)
| event(skc16,skc17) ),
inference(resolution,[status(thm)],[clause31,clause9]) ).
cnf(c291,plain,
( event(skc16,skc17)
| ~ agent(skc11,skc12,X108)
| ~ old(skc11,X108)
| ~ dirty(skc11,X108)
| ~ white(skc11,X108)
| ~ chevy(skc11,X108)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X109)
| ~ placename(skc11,X109)
| ~ in(skc11,skc12,X107)
| ~ city(skc11,X107)
| ~ of(skc11,X109,X107)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c203,clause36]) ).
cnf(c743,plain,
( event(skc16,skc17)
| ~ agent(skc11,skc12,X355)
| ~ old(skc11,X355)
| ~ dirty(skc11,X355)
| ~ white(skc11,X355)
| ~ chevy(skc11,X355)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c291,c235]) ).
cnf(c2569,plain,
( event(skc16,skc17)
| ~ agent(skc11,skc12,X463)
| ~ old(skc11,X463)
| ~ dirty(skc11,X463)
| ~ white(skc11,X463)
| ~ chevy(skc11,X463)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c743,c219]) ).
cnf(c3084,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2569,c251]) ).
cnf(c3097,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3084,c32]) ).
cnf(c3104,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3097,c20]) ).
cnf(c3111,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3104,c8]) ).
cnf(c3122,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3111,c44]) ).
cnf(c3127,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3122,c56]) ).
cnf(c3133,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3127,c68]) ).
cnf(c3145,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3133,c80]) ).
cnf(c3154,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3145,c92]) ).
cnf(c3158,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3154,c140]) ).
cnf(c3168,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3158,c128]) ).
cnf(c3172,plain,
( event(skc16,skc17)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3168,c116]) ).
cnf(c3186,plain,
( event(skc16,skc17)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3172,c104]) ).
cnf(c3187,plain,
( event(skc16,skc17)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3186,clause2]) ).
cnf(c3191,plain,
event(skc16,skc17),
inference(resolution,[status(thm)],[c3187,clause9]) ).
cnf(clause10,negated_conjecture,
( ssSkC0
| hollywood_placename(skc16,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c99,plain,
( old(skc11,skc13)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause23,clause10]) ).
cnf(c111,plain,
( dirty(skc11,skc13)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause24,clause10]) ).
cnf(c123,plain,
( white(skc11,skc13)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause25,clause10]) ).
cnf(c135,plain,
( chevy(skc11,skc13)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause26,clause10]) ).
cnf(c87,plain,
( barrel(skc11,skc12)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause22,clause10]) ).
cnf(c75,plain,
( present(skc11,skc12)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause21,clause10]) ).
cnf(c63,plain,
( event(skc11,skc12)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause20,clause10]) ).
cnf(c51,plain,
( hollywood_placename(skc11,skc15)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause19,clause10]) ).
cnf(c39,plain,
( placename(skc11,skc15)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause18,clause10]) ).
cnf(c3,plain,
( city(skc11,skc14)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause15,clause10]) ).
cnf(c15,plain,
( street(skc11,skc14)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause16,clause10]) ).
cnf(c27,plain,
( lonely(skc11,skc14)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause17,clause10]) ).
cnf(c245,plain,
( agent(skc11,skc12,skc13)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause34,clause10]) ).
cnf(c213,plain,
( in(skc11,skc12,skc14)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause32,clause10]) ).
cnf(c229,plain,
( of(skc11,skc15,skc14)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause33,clause10]) ).
cnf(c197,plain,
( down(skc11,skc12,skc14)
| hollywood_placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause31,clause10]) ).
cnf(c285,plain,
( hollywood_placename(skc16,skc19)
| ~ agent(skc11,skc12,X90)
| ~ old(skc11,X90)
| ~ dirty(skc11,X90)
| ~ white(skc11,X90)
| ~ chevy(skc11,X90)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X91)
| ~ placename(skc11,X91)
| ~ in(skc11,skc12,X89)
| ~ city(skc11,X89)
| ~ of(skc11,X91,X89)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c197,clause36]) ).
cnf(c657,plain,
( hollywood_placename(skc16,skc19)
| ~ agent(skc11,skc12,X266)
| ~ old(skc11,X266)
| ~ dirty(skc11,X266)
| ~ white(skc11,X266)
| ~ chevy(skc11,X266)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c285,c229]) ).
cnf(c1510,plain,
( hollywood_placename(skc16,skc19)
| ~ agent(skc11,skc12,X312)
| ~ old(skc11,X312)
| ~ dirty(skc11,X312)
| ~ white(skc11,X312)
| ~ chevy(skc11,X312)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c657,c213]) ).
cnf(c2038,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1510,c245]) ).
cnf(c2051,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2038,c27]) ).
cnf(c2062,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2051,c15]) ).
cnf(c2069,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2062,c3]) ).
cnf(c2079,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2069,c39]) ).
cnf(c2098,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2079,c51]) ).
cnf(c2123,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2098,c63]) ).
cnf(c2142,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2123,c75]) ).
cnf(c2147,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2142,c87]) ).
cnf(c2165,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2147,c135]) ).
cnf(c2178,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2165,c123]) ).
cnf(c2198,plain,
( hollywood_placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2178,c111]) ).
cnf(c2209,plain,
( hollywood_placename(skc16,skc19)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2198,c99]) ).
cnf(c2222,plain,
( hollywood_placename(skc16,skc19)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2209,clause2]) ).
cnf(c2225,plain,
hollywood_placename(skc16,skc19),
inference(resolution,[status(thm)],[c2222,clause10]) ).
cnf(clause11,negated_conjecture,
( ssSkC0
| placename(skc16,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c103,plain,
( old(skc11,skc13)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause23,clause11]) ).
cnf(c115,plain,
( dirty(skc11,skc13)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause24,clause11]) ).
cnf(c127,plain,
( white(skc11,skc13)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause25,clause11]) ).
cnf(c139,plain,
( chevy(skc11,skc13)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause26,clause11]) ).
cnf(c91,plain,
( barrel(skc11,skc12)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause22,clause11]) ).
cnf(c79,plain,
( present(skc11,skc12)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause21,clause11]) ).
cnf(c67,plain,
( event(skc11,skc12)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause20,clause11]) ).
cnf(c55,plain,
( hollywood_placename(skc11,skc15)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause19,clause11]) ).
cnf(c43,plain,
( placename(skc11,skc15)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause18,clause11]) ).
cnf(c7,plain,
( city(skc11,skc14)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause15,clause11]) ).
cnf(c19,plain,
( street(skc11,skc14)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause16,clause11]) ).
cnf(c31,plain,
( lonely(skc11,skc14)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause17,clause11]) ).
cnf(c250,plain,
( agent(skc11,skc12,skc13)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause34,clause11]) ).
cnf(c218,plain,
( in(skc11,skc12,skc14)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause32,clause11]) ).
cnf(c234,plain,
( of(skc11,skc15,skc14)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause33,clause11]) ).
cnf(c202,plain,
( down(skc11,skc12,skc14)
| placename(skc16,skc19) ),
inference(resolution,[status(thm)],[clause31,clause11]) ).
cnf(c290,plain,
( placename(skc16,skc19)
| ~ agent(skc11,skc12,X105)
| ~ old(skc11,X105)
| ~ dirty(skc11,X105)
| ~ white(skc11,X105)
| ~ chevy(skc11,X105)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X106)
| ~ placename(skc11,X106)
| ~ in(skc11,skc12,X104)
| ~ city(skc11,X104)
| ~ of(skc11,X106,X104)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c202,clause36]) ).
cnf(c720,plain,
( placename(skc16,skc19)
| ~ agent(skc11,skc12,X331)
| ~ old(skc11,X331)
| ~ dirty(skc11,X331)
| ~ white(skc11,X331)
| ~ chevy(skc11,X331)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c290,c234]) ).
cnf(c2329,plain,
( placename(skc16,skc19)
| ~ agent(skc11,skc12,X438)
| ~ old(skc11,X438)
| ~ dirty(skc11,X438)
| ~ white(skc11,X438)
| ~ chevy(skc11,X438)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c720,c218]) ).
cnf(c2950,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2329,c250]) ).
cnf(c2964,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2950,c31]) ).
cnf(c2967,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2964,c19]) ).
cnf(c2982,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2967,c7]) ).
cnf(c2984,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2982,c43]) ).
cnf(c2999,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2984,c55]) ).
cnf(c3006,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2999,c67]) ).
cnf(c3018,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3006,c79]) ).
cnf(c3021,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3018,c91]) ).
cnf(c3033,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3021,c139]) ).
cnf(c3045,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3033,c127]) ).
cnf(c3051,plain,
( placename(skc16,skc19)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3045,c115]) ).
cnf(c3057,plain,
( placename(skc16,skc19)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3051,c103]) ).
cnf(c3065,plain,
( placename(skc16,skc19)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3057,clause2]) ).
cnf(c3069,plain,
placename(skc16,skc19),
inference(resolution,[status(thm)],[c3065,clause11]) ).
cnf(clause12,negated_conjecture,
( ssSkC0
| city(skc16,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c107,plain,
( old(skc11,skc13)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause23,clause12]) ).
cnf(c119,plain,
( dirty(skc11,skc13)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause24,clause12]) ).
cnf(c131,plain,
( white(skc11,skc13)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause25,clause12]) ).
cnf(c143,plain,
( chevy(skc11,skc13)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause26,clause12]) ).
cnf(c95,plain,
( barrel(skc11,skc12)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause22,clause12]) ).
cnf(c83,plain,
( present(skc11,skc12)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause21,clause12]) ).
cnf(c71,plain,
( event(skc11,skc12)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause20,clause12]) ).
cnf(c59,plain,
( hollywood_placename(skc11,skc15)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause19,clause12]) ).
cnf(c47,plain,
( placename(skc11,skc15)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause18,clause12]) ).
cnf(c11,plain,
( city(skc11,skc14)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause15,clause12]) ).
cnf(c23,plain,
( street(skc11,skc14)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause16,clause12]) ).
cnf(c35,plain,
( lonely(skc11,skc14)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause17,clause12]) ).
cnf(c255,plain,
( agent(skc11,skc12,skc13)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause34,clause12]) ).
cnf(c223,plain,
( in(skc11,skc12,skc14)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause32,clause12]) ).
cnf(c239,plain,
( of(skc11,skc15,skc14)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause33,clause12]) ).
cnf(c207,plain,
( down(skc11,skc12,skc14)
| city(skc16,skc20) ),
inference(resolution,[status(thm)],[clause31,clause12]) ).
cnf(c296,plain,
( city(skc16,skc20)
| ~ agent(skc11,skc12,X123)
| ~ old(skc11,X123)
| ~ dirty(skc11,X123)
| ~ white(skc11,X123)
| ~ chevy(skc11,X123)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X124)
| ~ placename(skc11,X124)
| ~ in(skc11,skc12,X122)
| ~ city(skc11,X122)
| ~ of(skc11,X124,X122)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c207,clause36]) ).
cnf(c799,plain,
( city(skc16,skc20)
| ~ agent(skc11,skc12,X413)
| ~ old(skc11,X413)
| ~ dirty(skc11,X413)
| ~ white(skc11,X413)
| ~ chevy(skc11,X413)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c296,c239]) ).
cnf(c2884,plain,
( city(skc16,skc20)
| ~ agent(skc11,skc12,X501)
| ~ old(skc11,X501)
| ~ dirty(skc11,X501)
| ~ white(skc11,X501)
| ~ chevy(skc11,X501)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c799,c223]) ).
cnf(c3381,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2884,c255]) ).
cnf(c3389,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3381,c35]) ).
cnf(c3394,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3389,c23]) ).
cnf(c3397,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3394,c11]) ).
cnf(c3400,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3397,c47]) ).
cnf(c3407,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3400,c59]) ).
cnf(c3411,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3407,c71]) ).
cnf(c3419,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3411,c83]) ).
cnf(c3423,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3419,c95]) ).
cnf(c3428,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3423,c143]) ).
cnf(c3434,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3428,c131]) ).
cnf(c3436,plain,
( city(skc16,skc20)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3434,c119]) ).
cnf(c3441,plain,
( city(skc16,skc20)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3436,c107]) ).
cnf(c3445,plain,
( city(skc16,skc20)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3441,clause2]) ).
cnf(c3450,plain,
city(skc16,skc20),
inference(resolution,[status(thm)],[c3445,clause12]) ).
cnf(clause13,negated_conjecture,
( ssSkC0
| street(skc16,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c98,plain,
( old(skc11,skc13)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause23,clause13]) ).
cnf(c110,plain,
( dirty(skc11,skc13)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause24,clause13]) ).
cnf(c122,plain,
( white(skc11,skc13)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause25,clause13]) ).
cnf(c134,plain,
( chevy(skc11,skc13)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause26,clause13]) ).
cnf(c86,plain,
( barrel(skc11,skc12)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause22,clause13]) ).
cnf(c74,plain,
( present(skc11,skc12)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause21,clause13]) ).
cnf(c62,plain,
( event(skc11,skc12)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause20,clause13]) ).
cnf(c50,plain,
( hollywood_placename(skc11,skc15)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause19,clause13]) ).
cnf(c38,plain,
( placename(skc11,skc15)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause18,clause13]) ).
cnf(c2,plain,
( city(skc11,skc14)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause15,clause13]) ).
cnf(c14,plain,
( street(skc11,skc14)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause16,clause13]) ).
cnf(c26,plain,
( lonely(skc11,skc14)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause17,clause13]) ).
cnf(c244,plain,
( agent(skc11,skc12,skc13)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause34,clause13]) ).
cnf(c212,plain,
( in(skc11,skc12,skc14)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause32,clause13]) ).
cnf(c228,plain,
( of(skc11,skc15,skc14)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause33,clause13]) ).
cnf(c196,plain,
( down(skc11,skc12,skc14)
| street(skc16,skc18) ),
inference(resolution,[status(thm)],[clause31,clause13]) ).
cnf(c284,plain,
( street(skc16,skc18)
| ~ agent(skc11,skc12,X87)
| ~ old(skc11,X87)
| ~ dirty(skc11,X87)
| ~ white(skc11,X87)
| ~ chevy(skc11,X87)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X88)
| ~ placename(skc11,X88)
| ~ in(skc11,skc12,X86)
| ~ city(skc11,X86)
| ~ of(skc11,X88,X86)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c196,clause36]) ).
cnf(c632,plain,
( street(skc16,skc18)
| ~ agent(skc11,skc12,X241)
| ~ old(skc11,X241)
| ~ dirty(skc11,X241)
| ~ white(skc11,X241)
| ~ chevy(skc11,X241)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c284,c228]) ).
cnf(c1248,plain,
( street(skc16,skc18)
| ~ agent(skc11,skc12,X274)
| ~ old(skc11,X274)
| ~ dirty(skc11,X274)
| ~ white(skc11,X274)
| ~ chevy(skc11,X274)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c632,c212]) ).
cnf(c1586,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1248,c244]) ).
cnf(c1599,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1586,c26]) ).
cnf(c1622,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1599,c14]) ).
cnf(c1636,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1622,c2]) ).
cnf(c1643,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1636,c38]) ).
cnf(c1662,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1643,c50]) ).
cnf(c1675,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1662,c62]) ).
cnf(c1694,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1675,c74]) ).
cnf(c1702,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1694,c86]) ).
cnf(c1718,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1702,c134]) ).
cnf(c1734,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1718,c122]) ).
cnf(c1742,plain,
( street(skc16,skc18)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1734,c110]) ).
cnf(c1756,plain,
( street(skc16,skc18)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1742,c98]) ).
cnf(c1765,plain,
( street(skc16,skc18)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1756,clause2]) ).
cnf(c1768,plain,
street(skc16,skc18),
inference(resolution,[status(thm)],[c1765,clause13]) ).
cnf(clause14,negated_conjecture,
( ssSkC0
| lonely(skc16,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c101,plain,
( old(skc11,skc13)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause23,clause14]) ).
cnf(c113,plain,
( dirty(skc11,skc13)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause24,clause14]) ).
cnf(c125,plain,
( white(skc11,skc13)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause25,clause14]) ).
cnf(c137,plain,
( chevy(skc11,skc13)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause26,clause14]) ).
cnf(c89,plain,
( barrel(skc11,skc12)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause22,clause14]) ).
cnf(c77,plain,
( present(skc11,skc12)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause21,clause14]) ).
cnf(c65,plain,
( event(skc11,skc12)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause20,clause14]) ).
cnf(c53,plain,
( hollywood_placename(skc11,skc15)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause19,clause14]) ).
cnf(c41,plain,
( placename(skc11,skc15)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause18,clause14]) ).
cnf(c5,plain,
( city(skc11,skc14)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause15,clause14]) ).
cnf(c17,plain,
( street(skc11,skc14)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause16,clause14]) ).
cnf(c29,plain,
( lonely(skc11,skc14)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause17,clause14]) ).
cnf(c247,plain,
( agent(skc11,skc12,skc13)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause34,clause14]) ).
cnf(c215,plain,
( in(skc11,skc12,skc14)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause32,clause14]) ).
cnf(c231,plain,
( of(skc11,skc15,skc14)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause33,clause14]) ).
cnf(c199,plain,
( down(skc11,skc12,skc14)
| lonely(skc16,skc18) ),
inference(resolution,[status(thm)],[clause31,clause14]) ).
cnf(c288,plain,
( lonely(skc16,skc18)
| ~ agent(skc11,skc12,X99)
| ~ old(skc11,X99)
| ~ dirty(skc11,X99)
| ~ white(skc11,X99)
| ~ chevy(skc11,X99)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X100)
| ~ placename(skc11,X100)
| ~ in(skc11,skc12,X98)
| ~ city(skc11,X98)
| ~ of(skc11,X100,X98)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c199,clause36]) ).
cnf(c701,plain,
( lonely(skc16,skc18)
| ~ agent(skc11,skc12,X311)
| ~ old(skc11,X311)
| ~ dirty(skc11,X311)
| ~ white(skc11,X311)
| ~ chevy(skc11,X311)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c288,c231]) ).
cnf(c2022,plain,
( lonely(skc16,skc18)
| ~ agent(skc11,skc12,X381)
| ~ old(skc11,X381)
| ~ dirty(skc11,X381)
| ~ white(skc11,X381)
| ~ chevy(skc11,X381)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c701,c215]) ).
cnf(c2600,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2022,c247]) ).
cnf(c2604,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2600,c29]) ).
cnf(c2621,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2604,c17]) ).
cnf(c2636,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2621,c5]) ).
cnf(c2642,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2636,c41]) ).
cnf(c2656,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2642,c53]) ).
cnf(c2661,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2656,c65]) ).
cnf(c2674,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2661,c77]) ).
cnf(c2689,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2674,c89]) ).
cnf(c2697,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2689,c137]) ).
cnf(c2704,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2697,c125]) ).
cnf(c2724,plain,
( lonely(skc16,skc18)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2704,c113]) ).
cnf(c2730,plain,
( lonely(skc16,skc18)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2724,c101]) ).
cnf(c2736,plain,
( lonely(skc16,skc18)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2730,clause2]) ).
cnf(c2739,plain,
lonely(skc16,skc18),
inference(resolution,[status(thm)],[c2736,clause14]) ).
cnf(clause27,negated_conjecture,
( ssSkC0
| agent(skc16,skc17,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c149,plain,
( agent(skc16,skc17,skc21)
| old(skc11,skc13) ),
inference(resolution,[status(thm)],[clause27,clause23]) ).
cnf(c153,plain,
( agent(skc16,skc17,skc21)
| dirty(skc11,skc13) ),
inference(resolution,[status(thm)],[clause27,clause24]) ).
cnf(c148,plain,
( agent(skc16,skc17,skc21)
| white(skc11,skc13) ),
inference(resolution,[status(thm)],[clause27,clause25]) ).
cnf(c147,plain,
( agent(skc16,skc17,skc21)
| chevy(skc11,skc13) ),
inference(resolution,[status(thm)],[clause27,clause26]) ).
cnf(c154,plain,
( agent(skc16,skc17,skc21)
| barrel(skc11,skc12) ),
inference(resolution,[status(thm)],[clause27,clause22]) ).
cnf(c150,plain,
( agent(skc16,skc17,skc21)
| present(skc11,skc12) ),
inference(resolution,[status(thm)],[clause27,clause21]) ).
cnf(c144,plain,
( agent(skc16,skc17,skc21)
| event(skc11,skc12) ),
inference(resolution,[status(thm)],[clause27,clause20]) ).
cnf(c145,plain,
( agent(skc16,skc17,skc21)
| hollywood_placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause27,clause19]) ).
cnf(c151,plain,
( agent(skc16,skc17,skc21)
| placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause27,clause18]) ).
cnf(c155,plain,
( agent(skc16,skc17,skc21)
| city(skc11,skc14) ),
inference(resolution,[status(thm)],[clause27,clause15]) ).
cnf(c152,plain,
( agent(skc16,skc17,skc21)
| street(skc11,skc14) ),
inference(resolution,[status(thm)],[clause27,clause16]) ).
cnf(c146,plain,
( agent(skc16,skc17,skc21)
| lonely(skc11,skc14) ),
inference(resolution,[status(thm)],[clause27,clause17]) ).
cnf(c253,plain,
( agent(skc11,skc12,skc13)
| agent(skc16,skc17,skc21) ),
inference(resolution,[status(thm)],[clause34,clause27]) ).
cnf(c221,plain,
( in(skc11,skc12,skc14)
| agent(skc16,skc17,skc21) ),
inference(resolution,[status(thm)],[clause32,clause27]) ).
cnf(c237,plain,
( of(skc11,skc15,skc14)
| agent(skc16,skc17,skc21) ),
inference(resolution,[status(thm)],[clause33,clause27]) ).
cnf(c205,plain,
( down(skc11,skc12,skc14)
| agent(skc16,skc17,skc21) ),
inference(resolution,[status(thm)],[clause31,clause27]) ).
cnf(c298,plain,
( agent(skc16,skc17,skc21)
| ~ agent(skc11,skc12,X129)
| ~ old(skc11,X129)
| ~ dirty(skc11,X129)
| ~ white(skc11,X129)
| ~ chevy(skc11,X129)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X130)
| ~ placename(skc11,X130)
| ~ in(skc11,skc12,X128)
| ~ city(skc11,X128)
| ~ of(skc11,X130,X128)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c205,clause36]) ).
cnf(c835,plain,
( agent(skc16,skc17,skc21)
| ~ agent(skc11,skc12,X450)
| ~ old(skc11,X450)
| ~ dirty(skc11,X450)
| ~ white(skc11,X450)
| ~ chevy(skc11,X450)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c298,c237]) ).
cnf(c3078,plain,
( agent(skc16,skc17,skc21)
| ~ agent(skc11,skc12,X541)
| ~ old(skc11,X541)
| ~ dirty(skc11,X541)
| ~ white(skc11,X541)
| ~ chevy(skc11,X541)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c835,c221]) ).
cnf(c3582,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3078,c253]) ).
cnf(c3583,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3582,c146]) ).
cnf(c3584,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3583,c152]) ).
cnf(c3585,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3584,c155]) ).
cnf(c3586,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3585,c151]) ).
cnf(c3587,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3586,c145]) ).
cnf(c3588,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3587,c144]) ).
cnf(c3589,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3588,c150]) ).
cnf(c3590,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3589,c154]) ).
cnf(c3591,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3590,c147]) ).
cnf(c3592,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3591,c148]) ).
cnf(c3593,plain,
( agent(skc16,skc17,skc21)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3592,c153]) ).
cnf(c3594,plain,
( agent(skc16,skc17,skc21)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3593,c149]) ).
cnf(c3595,plain,
( agent(skc16,skc17,skc21)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3594,clause2]) ).
cnf(c3596,plain,
agent(skc16,skc17,skc21),
inference(resolution,[status(thm)],[c3595,clause27]) ).
cnf(clause28,negated_conjecture,
( ssSkC0
| in(skc16,skc17,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c161,plain,
( in(skc16,skc17,skc20)
| old(skc11,skc13) ),
inference(resolution,[status(thm)],[clause28,clause23]) ).
cnf(c165,plain,
( in(skc16,skc17,skc20)
| dirty(skc11,skc13) ),
inference(resolution,[status(thm)],[clause28,clause24]) ).
cnf(c160,plain,
( in(skc16,skc17,skc20)
| white(skc11,skc13) ),
inference(resolution,[status(thm)],[clause28,clause25]) ).
cnf(c159,plain,
( in(skc16,skc17,skc20)
| chevy(skc11,skc13) ),
inference(resolution,[status(thm)],[clause28,clause26]) ).
cnf(c166,plain,
( in(skc16,skc17,skc20)
| barrel(skc11,skc12) ),
inference(resolution,[status(thm)],[clause28,clause22]) ).
cnf(c162,plain,
( in(skc16,skc17,skc20)
| present(skc11,skc12) ),
inference(resolution,[status(thm)],[clause28,clause21]) ).
cnf(c156,plain,
( in(skc16,skc17,skc20)
| event(skc11,skc12) ),
inference(resolution,[status(thm)],[clause28,clause20]) ).
cnf(c157,plain,
( in(skc16,skc17,skc20)
| hollywood_placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause28,clause19]) ).
cnf(c163,plain,
( in(skc16,skc17,skc20)
| placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause28,clause18]) ).
cnf(c167,plain,
( in(skc16,skc17,skc20)
| city(skc11,skc14) ),
inference(resolution,[status(thm)],[clause28,clause15]) ).
cnf(c164,plain,
( in(skc16,skc17,skc20)
| street(skc11,skc14) ),
inference(resolution,[status(thm)],[clause28,clause16]) ).
cnf(c158,plain,
( in(skc16,skc17,skc20)
| lonely(skc11,skc14) ),
inference(resolution,[status(thm)],[clause28,clause17]) ).
cnf(c248,plain,
( agent(skc11,skc12,skc13)
| in(skc16,skc17,skc20) ),
inference(resolution,[status(thm)],[clause34,clause28]) ).
cnf(c216,plain,
( in(skc11,skc12,skc14)
| in(skc16,skc17,skc20) ),
inference(resolution,[status(thm)],[clause32,clause28]) ).
cnf(c232,plain,
( of(skc11,skc15,skc14)
| in(skc16,skc17,skc20) ),
inference(resolution,[status(thm)],[clause33,clause28]) ).
cnf(c200,plain,
( down(skc11,skc12,skc14)
| in(skc16,skc17,skc20) ),
inference(resolution,[status(thm)],[clause31,clause28]) ).
cnf(c297,plain,
( in(skc16,skc17,skc20)
| ~ agent(skc11,skc12,X126)
| ~ old(skc11,X126)
| ~ dirty(skc11,X126)
| ~ white(skc11,X126)
| ~ chevy(skc11,X126)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X127)
| ~ placename(skc11,X127)
| ~ in(skc11,skc12,X125)
| ~ city(skc11,X125)
| ~ of(skc11,X127,X125)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c200,clause36]) ).
cnf(c811,plain,
( in(skc16,skc17,skc20)
| ~ agent(skc11,skc12,X425)
| ~ old(skc11,X425)
| ~ dirty(skc11,X425)
| ~ white(skc11,X425)
| ~ chevy(skc11,X425)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c297,c232]) ).
cnf(c2939,plain,
( in(skc16,skc17,skc20)
| ~ agent(skc11,skc12,X534)
| ~ old(skc11,X534)
| ~ dirty(skc11,X534)
| ~ white(skc11,X534)
| ~ chevy(skc11,X534)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c811,c216]) ).
cnf(c3554,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2939,c248]) ).
cnf(c3555,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3554,c158]) ).
cnf(c3558,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3555,c164]) ).
cnf(c3559,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3558,c167]) ).
cnf(c3562,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3559,c163]) ).
cnf(c3563,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3562,c157]) ).
cnf(c3566,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3563,c156]) ).
cnf(c3568,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3566,c162]) ).
cnf(c3569,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3568,c166]) ).
cnf(c3571,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3569,c159]) ).
cnf(c3574,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3571,c160]) ).
cnf(c3575,plain,
( in(skc16,skc17,skc20)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3574,c165]) ).
cnf(c3578,plain,
( in(skc16,skc17,skc20)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3575,c161]) ).
cnf(c3579,plain,
( in(skc16,skc17,skc20)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3578,clause2]) ).
cnf(c3580,plain,
in(skc16,skc17,skc20),
inference(resolution,[status(thm)],[c3579,clause28]) ).
cnf(clause29,negated_conjecture,
( ssSkC0
| of(skc16,skc19,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c173,plain,
( of(skc16,skc19,skc20)
| old(skc11,skc13) ),
inference(resolution,[status(thm)],[clause29,clause23]) ).
cnf(c177,plain,
( of(skc16,skc19,skc20)
| dirty(skc11,skc13) ),
inference(resolution,[status(thm)],[clause29,clause24]) ).
cnf(c172,plain,
( of(skc16,skc19,skc20)
| white(skc11,skc13) ),
inference(resolution,[status(thm)],[clause29,clause25]) ).
cnf(c171,plain,
( of(skc16,skc19,skc20)
| chevy(skc11,skc13) ),
inference(resolution,[status(thm)],[clause29,clause26]) ).
cnf(c178,plain,
( of(skc16,skc19,skc20)
| barrel(skc11,skc12) ),
inference(resolution,[status(thm)],[clause29,clause22]) ).
cnf(c174,plain,
( of(skc16,skc19,skc20)
| present(skc11,skc12) ),
inference(resolution,[status(thm)],[clause29,clause21]) ).
cnf(c168,plain,
( of(skc16,skc19,skc20)
| event(skc11,skc12) ),
inference(resolution,[status(thm)],[clause29,clause20]) ).
cnf(c169,plain,
( of(skc16,skc19,skc20)
| hollywood_placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause29,clause19]) ).
cnf(c175,plain,
( of(skc16,skc19,skc20)
| placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause29,clause18]) ).
cnf(c179,plain,
( of(skc16,skc19,skc20)
| city(skc11,skc14) ),
inference(resolution,[status(thm)],[clause29,clause15]) ).
cnf(c176,plain,
( of(skc16,skc19,skc20)
| street(skc11,skc14) ),
inference(resolution,[status(thm)],[clause29,clause16]) ).
cnf(c170,plain,
( of(skc16,skc19,skc20)
| lonely(skc11,skc14) ),
inference(resolution,[status(thm)],[clause29,clause17]) ).
cnf(c240,plain,
( agent(skc11,skc12,skc13)
| of(skc16,skc19,skc20) ),
inference(resolution,[status(thm)],[clause34,clause29]) ).
cnf(c208,plain,
( in(skc11,skc12,skc14)
| of(skc16,skc19,skc20) ),
inference(resolution,[status(thm)],[clause32,clause29]) ).
cnf(c224,plain,
( of(skc11,skc15,skc14)
| of(skc16,skc19,skc20) ),
inference(resolution,[status(thm)],[clause33,clause29]) ).
cnf(c192,plain,
( down(skc11,skc12,skc14)
| of(skc16,skc19,skc20) ),
inference(resolution,[status(thm)],[clause31,clause29]) ).
cnf(c287,plain,
( of(skc16,skc19,skc20)
| ~ agent(skc11,skc12,X96)
| ~ old(skc11,X96)
| ~ dirty(skc11,X96)
| ~ white(skc11,X96)
| ~ chevy(skc11,X96)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X97)
| ~ placename(skc11,X97)
| ~ in(skc11,skc12,X95)
| ~ city(skc11,X95)
| ~ of(skc11,X97,X95)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c192,clause36]) ).
cnf(c684,plain,
( of(skc16,skc19,skc20)
| ~ agent(skc11,skc12,X294)
| ~ old(skc11,X294)
| ~ dirty(skc11,X294)
| ~ white(skc11,X294)
| ~ chevy(skc11,X294)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c287,c224]) ).
cnf(c1888,plain,
( of(skc16,skc19,skc20)
| ~ agent(skc11,skc12,X512)
| ~ old(skc11,X512)
| ~ dirty(skc11,X512)
| ~ white(skc11,X512)
| ~ chevy(skc11,X512)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c684,c208]) ).
cnf(c3452,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c1888,c240]) ).
cnf(c3458,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3452,c170]) ).
cnf(c3460,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3458,c176]) ).
cnf(c3466,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3460,c179]) ).
cnf(c3468,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3466,c175]) ).
cnf(c3473,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3468,c169]) ).
cnf(c3477,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3473,c168]) ).
cnf(c3480,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3477,c174]) ).
cnf(c3485,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3480,c178]) ).
cnf(c3488,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3485,c171]) ).
cnf(c3494,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3488,c172]) ).
cnf(c3497,plain,
( of(skc16,skc19,skc20)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3494,c177]) ).
cnf(c3499,plain,
( of(skc16,skc19,skc20)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3497,c173]) ).
cnf(c3503,plain,
( of(skc16,skc19,skc20)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3499,clause2]) ).
cnf(c3504,plain,
of(skc16,skc19,skc20),
inference(resolution,[status(thm)],[c3503,clause29]) ).
cnf(clause30,negated_conjecture,
( ssSkC0
| down(skc16,skc17,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c185,plain,
( down(skc16,skc17,skc18)
| old(skc11,skc13) ),
inference(resolution,[status(thm)],[clause30,clause23]) ).
cnf(c189,plain,
( down(skc16,skc17,skc18)
| dirty(skc11,skc13) ),
inference(resolution,[status(thm)],[clause30,clause24]) ).
cnf(c184,plain,
( down(skc16,skc17,skc18)
| white(skc11,skc13) ),
inference(resolution,[status(thm)],[clause30,clause25]) ).
cnf(c183,plain,
( down(skc16,skc17,skc18)
| chevy(skc11,skc13) ),
inference(resolution,[status(thm)],[clause30,clause26]) ).
cnf(c190,plain,
( down(skc16,skc17,skc18)
| barrel(skc11,skc12) ),
inference(resolution,[status(thm)],[clause30,clause22]) ).
cnf(c186,plain,
( down(skc16,skc17,skc18)
| present(skc11,skc12) ),
inference(resolution,[status(thm)],[clause30,clause21]) ).
cnf(c180,plain,
( down(skc16,skc17,skc18)
| event(skc11,skc12) ),
inference(resolution,[status(thm)],[clause30,clause20]) ).
cnf(c181,plain,
( down(skc16,skc17,skc18)
| hollywood_placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause30,clause19]) ).
cnf(c187,plain,
( down(skc16,skc17,skc18)
| placename(skc11,skc15) ),
inference(resolution,[status(thm)],[clause30,clause18]) ).
cnf(c191,plain,
( down(skc16,skc17,skc18)
| city(skc11,skc14) ),
inference(resolution,[status(thm)],[clause30,clause15]) ).
cnf(c188,plain,
( down(skc16,skc17,skc18)
| street(skc11,skc14) ),
inference(resolution,[status(thm)],[clause30,clause16]) ).
cnf(c182,plain,
( down(skc16,skc17,skc18)
| lonely(skc11,skc14) ),
inference(resolution,[status(thm)],[clause30,clause17]) ).
cnf(c243,plain,
( agent(skc11,skc12,skc13)
| down(skc16,skc17,skc18) ),
inference(resolution,[status(thm)],[clause34,clause30]) ).
cnf(c211,plain,
( in(skc11,skc12,skc14)
| down(skc16,skc17,skc18) ),
inference(resolution,[status(thm)],[clause32,clause30]) ).
cnf(c227,plain,
( of(skc11,skc15,skc14)
| down(skc16,skc17,skc18) ),
inference(resolution,[status(thm)],[clause33,clause30]) ).
cnf(c195,plain,
( down(skc11,skc12,skc14)
| down(skc16,skc17,skc18) ),
inference(resolution,[status(thm)],[clause31,clause30]) ).
cnf(c293,plain,
( down(skc16,skc17,skc18)
| ~ agent(skc11,skc12,X114)
| ~ old(skc11,X114)
| ~ dirty(skc11,X114)
| ~ white(skc11,X114)
| ~ chevy(skc11,X114)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,X115)
| ~ placename(skc11,X115)
| ~ in(skc11,skc12,X113)
| ~ city(skc11,X113)
| ~ of(skc11,X115,X113)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c195,clause36]) ).
cnf(c764,plain,
( down(skc16,skc17,skc18)
| ~ agent(skc11,skc12,X376)
| ~ old(skc11,X376)
| ~ dirty(skc11,X376)
| ~ white(skc11,X376)
| ~ chevy(skc11,X376)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ in(skc11,skc12,skc14)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c293,c227]) ).
cnf(c2584,plain,
( down(skc16,skc17,skc18)
| ~ agent(skc11,skc12,X524)
| ~ old(skc11,X524)
| ~ dirty(skc11,X524)
| ~ white(skc11,X524)
| ~ chevy(skc11,X524)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c764,c211]) ).
cnf(c3511,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ lonely(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c2584,c243]) ).
cnf(c3512,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ street(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3511,c182]) ).
cnf(c3517,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ city(skc11,skc14)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3512,c188]) ).
cnf(c3518,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3517,c191]) ).
cnf(c3523,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ hollywood_placename(skc11,skc15)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3518,c187]) ).
cnf(c3526,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ event(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3523,c181]) ).
cnf(c3527,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ present(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3526,c180]) ).
cnf(c3532,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ barrel(skc11,skc12)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3527,c186]) ).
cnf(c3535,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ chevy(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3532,c190]) ).
cnf(c3536,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ white(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3535,c183]) ).
cnf(c3541,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ dirty(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3536,c184]) ).
cnf(c3544,plain,
( down(skc16,skc17,skc18)
| ~ old(skc11,skc13)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3541,c189]) ).
cnf(c3547,plain,
( down(skc16,skc17,skc18)
| ~ actual_world(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3544,c185]) ).
cnf(c3548,plain,
( down(skc16,skc17,skc18)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3547,clause2]) ).
cnf(c3549,plain,
down(skc16,skc17,skc18),
inference(resolution,[status(thm)],[c3548,clause30]) ).
cnf(c3552,plain,
( ~ agent(skc16,skc17,X555)
| ~ old(skc16,X555)
| ~ dirty(skc16,X555)
| ~ white(skc16,X555)
| ~ chevy(skc16,X555)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,X556)
| ~ placename(skc16,X556)
| ~ in(skc16,skc17,X554)
| ~ city(skc16,X554)
| ~ of(skc16,X556,X554)
| ~ street(skc16,skc18)
| ~ lonely(skc16,skc18)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3549,clause36]) ).
cnf(c3598,plain,
( ~ agent(skc16,skc17,X557)
| ~ old(skc16,X557)
| ~ dirty(skc16,X557)
| ~ white(skc16,X557)
| ~ chevy(skc16,X557)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,skc19)
| ~ placename(skc16,skc19)
| ~ in(skc16,skc17,skc20)
| ~ city(skc16,skc20)
| ~ street(skc16,skc18)
| ~ lonely(skc16,skc18)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3552,c3504]) ).
cnf(c3599,plain,
( ~ agent(skc16,skc17,X558)
| ~ old(skc16,X558)
| ~ dirty(skc16,X558)
| ~ white(skc16,X558)
| ~ chevy(skc16,X558)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,skc19)
| ~ placename(skc16,skc19)
| ~ city(skc16,skc20)
| ~ street(skc16,skc18)
| ~ lonely(skc16,skc18)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3598,c3580]) ).
cnf(c3600,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,skc19)
| ~ placename(skc16,skc19)
| ~ city(skc16,skc20)
| ~ street(skc16,skc18)
| ~ lonely(skc16,skc18)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3599,c3596]) ).
cnf(c3601,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,skc19)
| ~ placename(skc16,skc19)
| ~ city(skc16,skc20)
| ~ street(skc16,skc18)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3600,c2739]) ).
cnf(c3602,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,skc19)
| ~ placename(skc16,skc19)
| ~ city(skc16,skc20)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3601,c1768]) ).
cnf(c3603,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,skc19)
| ~ placename(skc16,skc19)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3602,c3450]) ).
cnf(c3604,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ hollywood_placename(skc16,skc19)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3603,c3069]) ).
cnf(c3605,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ event(skc16,skc17)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3604,c2225]) ).
cnf(c3606,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ present(skc16,skc17)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3605,c3191]) ).
cnf(c3607,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ barrel(skc16,skc17)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3606,c3378]) ).
cnf(c3608,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3607,c598]) ).
cnf(c3609,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3608,c3291]) ).
cnf(c3610,plain,
( ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3609,c2932]) ).
cnf(c3611,plain,
( ~ old(skc16,skc21)
| ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3610,c1050]) ).
cnf(c3612,plain,
( ~ actual_world(skc16)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c3611,c2539]) ).
cnf(c3613,plain,
~ ssSkC0,
inference(resolution,[status(thm)],[c3612,clause1]) ).
cnf(clause35,negated_conjecture,
( ~ city(X2,X4)
| ~ street(X2,X4)
| ~ lonely(X2,X4)
| ~ down(X2,X5,X4)
| ~ in(X2,X5,X4)
| ~ placename(X2,X6)
| ~ hollywood_placename(X2,X6)
| ~ of(X2,X6,X4)
| ~ event(X2,X5)
| ~ present(X2,X5)
| ~ barrel(X2,X5)
| ~ agent(X2,X5,X3)
| ~ old(X2,X3)
| ~ dirty(X2,X3)
| ~ white(X2,X3)
| ~ chevy(X2,X3)
| ~ actual_world(X2)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c256,plain,
( ~ city(skc16,X13)
| ~ street(skc16,X13)
| ~ lonely(skc16,X13)
| ~ down(skc16,skc17,X13)
| ~ in(skc16,skc17,X13)
| ~ placename(skc16,X14)
| ~ hollywood_placename(skc16,X14)
| ~ of(skc16,X14,X13)
| ~ event(skc16,skc17)
| ~ present(skc16,skc17)
| ~ barrel(skc16,skc17)
| ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ actual_world(skc16)
| ssSkC0 ),
inference(resolution,[status(thm)],[clause35,clause27]) ).
cnf(c338,plain,
( ~ city(skc16,skc20)
| ~ street(skc16,skc20)
| ~ lonely(skc16,skc20)
| ~ down(skc16,skc17,skc20)
| ~ in(skc16,skc17,skc20)
| ~ placename(skc16,skc19)
| ~ hollywood_placename(skc16,skc19)
| ~ event(skc16,skc17)
| ~ present(skc16,skc17)
| ~ barrel(skc16,skc17)
| ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ actual_world(skc16)
| ssSkC0 ),
inference(resolution,[status(thm)],[c256,clause29]) ).
cnf(c342,plain,
( ~ city(skc16,skc20)
| ~ street(skc16,skc20)
| ~ lonely(skc16,skc20)
| ~ down(skc16,skc17,skc20)
| ~ placename(skc16,skc19)
| ~ hollywood_placename(skc16,skc19)
| ~ event(skc16,skc17)
| ~ present(skc16,skc17)
| ~ barrel(skc16,skc17)
| ~ old(skc16,skc21)
| ~ dirty(skc16,skc21)
| ~ white(skc16,skc21)
| ~ chevy(skc16,skc21)
| ~ actual_world(skc16)
| ssSkC0 ),
inference(resolution,[status(thm)],[c338,clause28]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP118-1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n017.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 13:34:23 EDT 2024
% 0.13/0.33 % CPUTime :
% 5.78/5.94 % Version: 1.5
% 5.78/5.94 % SZS status Satisfiable
% 5.78/5.94 % SZS output start Saturation
% See solution above
% 5.79/5.96
% 5.79/5.96 % Initial clauses : 36
% 5.79/5.96 % Processed clauses : 669
% 5.79/5.96 % Factors computed : 0
% 5.79/5.96 % Resolvents computed: 3614
% 5.79/5.96 % Tautologies deleted: 1
% 5.79/5.96 % Forward subsumed : 2980
% 5.79/5.96 % Backward subsumed : 647
% 5.79/5.96 % -------- CPU Time ---------
% 5.79/5.96 % User time : 5.606 s
% 5.79/5.96 % System time : 0.020 s
% 5.79/5.96 % Total time : 5.626 s
%------------------------------------------------------------------------------