%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP117-1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 : Fri Jul 25 11:59:38 AM UTC 2025
% Result : Unsatisfiable 0.13s 0.38s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause1)
% Comments :
%------------------------------------------------------------------------------
cnf(0,plain,
actual_world(skc18),
inference(cnf,[status(esa)],[clause1]) ).
cnf(l0,plain,
actual_world(skc18),
inference(instantiation,[status(thm)],[0]) ).
cnf(35,plain,
( ~ ssSkC0
| ~ actual_world(X0)
| ~ old(X0,X1)
| ~ present(X0,X2)
| ~ hollywood_placename(X0,X3)
| ~ dirty(X0,X1)
| ~ chevy(X0,X1)
| ~ white(X0,X1)
| ~ barrel(X0,X2)
| ~ lonely(X0,X4)
| ~ street(X0,X4)
| ~ event(X0,X2)
| ~ city(X0,X5)
| ~ placename(X0,X3)
| ~ down(X0,X2,X4)
| ~ agent(X0,X2,X1)
| ~ in(X0,X2,X5)
| ~ of(X0,X3,X5) ),
inference(cnf,[status(esa)],[clause36]) ).
cnf(l1,plain,
( ~ ssSkC0
| ~ actual_world(skc18)
| ~ old(skc18,skc23)
| ~ present(skc18,skc19)
| ~ hollywood_placename(skc18,skc21)
| ~ dirty(skc18,skc23)
| ~ chevy(skc18,skc23)
| ~ white(skc18,skc23)
| ~ barrel(skc18,skc19)
| ~ lonely(skc18,skc20)
| ~ street(skc18,skc20)
| ~ event(skc18,skc19)
| ~ city(skc18,skc22)
| ~ placename(skc18,skc21)
| ~ down(skc18,skc19,skc20)
| ~ agent(skc18,skc19,skc23)
| ~ in(skc18,skc19,skc22)
| ~ of(skc18,skc21,skc22) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(27,plain,
( ssSkC0
| in(skc18,skc19,skc22) ),
inference(cnf,[status(esa)],[clause28]) ).
cnf(l2,plain,
( ssSkC0
| in(skc18,skc19,skc22) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(5,plain,
( ssSkC0
| chevy(skc18,skc23) ),
inference(cnf,[status(esa)],[clause6]) ).
cnf(l3,plain,
( ssSkC0
| chevy(skc18,skc23) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(2,plain,
( ssSkC0
| old(skc18,skc23) ),
inference(cnf,[status(esa)],[clause3]) ).
cnf(l4,plain,
( ssSkC0
| old(skc18,skc23) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(8,plain,
( ssSkC0
| event(skc18,skc19) ),
inference(cnf,[status(esa)],[clause9]) ).
cnf(l5,plain,
( ssSkC0
| event(skc18,skc19) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(4,plain,
( ssSkC0
| white(skc18,skc23) ),
inference(cnf,[status(esa)],[clause5]) ).
cnf(l6,plain,
( ssSkC0
| white(skc18,skc23) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(28,plain,
( ssSkC0
| of(skc18,skc21,skc22) ),
inference(cnf,[status(esa)],[clause29]) ).
cnf(l7,plain,
( ssSkC0
| of(skc18,skc21,skc22) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(17,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(cnf,[status(esa)],[clause18]) ).
cnf(l8,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(20,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(cnf,[status(esa)],[clause21]) ).
cnf(l9,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(26,plain,
( ssSkC0
| agent(skc18,skc19,skc23) ),
inference(cnf,[status(esa)],[clause27]) ).
cnf(l10,plain,
( ssSkC0
| agent(skc18,skc19,skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(13,plain,
( ssSkC0
| lonely(skc18,skc20) ),
inference(cnf,[status(esa)],[clause14]) ).
cnf(l11,plain,
( ssSkC0
| lonely(skc18,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(9,plain,
( ssSkC0
| hollywood_placename(skc18,skc21) ),
inference(cnf,[status(esa)],[clause10]) ).
cnf(l12,plain,
( ssSkC0
| hollywood_placename(skc18,skc21) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(34,plain,
( ~ actual_world(X0)
| ~ old(X0,X1)
| ~ present(X0,X2)
| ~ hollywood_placename(X0,X3)
| ~ dirty(X0,X1)
| ~ chevy(X0,X1)
| ~ white(X0,X1)
| ~ barrel(X0,X2)
| ~ lonely(X0,X4)
| ~ street(X0,X4)
| ~ event(X0,X2)
| ~ city(X0,X5)
| ~ placename(X0,X3)
| ~ down(X0,X2,X4)
| ~ agent(X0,X2,X1)
| ~ in(X0,X2,X5)
| ~ of(X0,X3,X5)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause35]) ).
cnf(l13,plain,
( ~ actual_world(skc18)
| ~ old(skc18,skc23)
| ~ present(skc18,skc19)
| ~ hollywood_placename(skc18,skc21)
| ~ dirty(skc18,skc23)
| ~ chevy(skc18,skc23)
| ~ white(skc18,skc23)
| ~ barrel(skc18,skc19)
| ~ lonely(skc18,skc20)
| ~ street(skc18,skc20)
| ~ event(skc18,skc19)
| ~ city(skc18,skc22)
| ~ placename(skc18,skc21)
| ~ down(skc18,skc19,skc20)
| ~ agent(skc18,skc19,skc23)
| ~ in(skc18,skc19,skc22)
| ~ of(skc18,skc21,skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[34]) ).
cnf(12,plain,
( ssSkC0
| street(skc18,skc20) ),
inference(cnf,[status(esa)],[clause13]) ).
cnf(l33,plain,
( ssSkC0
| street(skc18,skc20) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l79,plain,
( ssSkC0
| chevy(skc18,skc23) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l29,plain,
( ssSkC0
| agent(skc18,skc19,skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(3,plain,
( ssSkC0
| dirty(skc18,skc23) ),
inference(cnf,[status(esa)],[clause4]) ).
cnf(l65,plain,
( ssSkC0
| dirty(skc18,skc23) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l124,plain,
( ssSkC0
| old(skc18,skc23) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(11,plain,
( ssSkC0
| city(skc18,skc22) ),
inference(cnf,[status(esa)],[clause12]) ).
cnf(l78,plain,
( ssSkC0
| city(skc18,skc22) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l125,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l126,plain,
( ssSkC0
| city(skc18,skc22) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l102,plain,
( ssSkC0
| dirty(skc18,skc23) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(22,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(cnf,[status(esa)],[clause23]) ).
cnf(l132,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(10,plain,
( ssSkC0
| placename(skc18,skc21) ),
inference(cnf,[status(esa)],[clause11]) ).
cnf(l39,plain,
( ssSkC0
| placename(skc18,skc21) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l133,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(32,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(cnf,[status(esa)],[clause33]) ).
cnf(l127,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l53,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(6,plain,
( ssSkC0
| barrel(skc18,skc19) ),
inference(cnf,[status(esa)],[clause7]) ).
cnf(l35,plain,
( ssSkC0
| barrel(skc18,skc19) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(29,plain,
( ssSkC0
| down(skc18,skc19,skc20) ),
inference(cnf,[status(esa)],[clause30]) ).
cnf(l48,plain,
( ssSkC0
| down(skc18,skc19,skc20) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(7,plain,
( ssSkC0
| present(skc18,skc19) ),
inference(cnf,[status(esa)],[clause8]) ).
cnf(l66,plain,
( ssSkC0
| present(skc18,skc19) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l15,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l16,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(15,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(cnf,[status(esa)],[clause16]) ).
cnf(l134,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l101,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(30,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(cnf,[status(esa)],[clause31]) ).
cnf(l129,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l21,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(1,plain,
actual_world(skc12),
inference(cnf,[status(esa)],[clause2]) ).
cnf(l61,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(33,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(cnf,[status(esa)],[clause34]) ).
cnf(l135,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(18,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(cnf,[status(esa)],[clause19]) ).
cnf(l136,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(21,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(cnf,[status(esa)],[clause22]) ).
cnf(l137,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l138,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l139,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l24,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l32,plain,
( ssSkC0
| barrel(skc18,skc19) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l59,plain,
( ssSkC0
| hollywood_placename(skc18,skc21) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l54,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l91,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l140,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(16,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(cnf,[status(esa)],[clause17]) ).
cnf(l52,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l82,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(25,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(cnf,[status(esa)],[clause26]) ).
cnf(l37,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l31,plain,
( ssSkC0
| placename(skc18,skc21) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l49,plain,
( ssSkC0
| lonely(skc18,skc20) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l22,plain,
( ssSkC0
| in(skc18,skc19,skc22) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l141,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l85,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l142,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l86,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(14,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(cnf,[status(esa)],[clause15]) ).
cnf(l143,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(31,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(cnf,[status(esa)],[clause32]) ).
cnf(l144,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l30,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(24,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(cnf,[status(esa)],[clause25]) ).
cnf(l17,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l145,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l146,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(23,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(cnf,[status(esa)],[clause24]) ).
cnf(l147,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l47,plain,
( ssSkC0
| event(skc18,skc19) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(19,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(cnf,[status(esa)],[clause20]) ).
cnf(l148,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l149,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l25,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l154,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l80,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l155,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l156,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l43,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l34,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l157,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l158,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l58,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l60,plain,
( ssSkC0
| white(skc18,skc23) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l81,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l159,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l62,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l50,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l69,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l90,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l160,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l161,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l151,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l64,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l193,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l170,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l207,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l208,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l14,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l107,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l166,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l209,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l181,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l210,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l211,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l45,plain,
( ssSkC0
| street(skc18,skc20) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l212,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l213,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l184,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l214,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l198,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l70,plain,
( ssSkC0
| present(skc18,skc19) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l215,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l174,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l67,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l216,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l217,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l38,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l218,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l219,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l220,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l182,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l189,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l111,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l221,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l117,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l27,plain,
( ssSkC0
| down(skc18,skc19,skc20) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l222,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l191,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l19,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l23,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l223,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l224,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l169,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l44,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l201,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l225,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l226,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l227,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l228,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l150,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l130,plain,
( ssSkC0
| of(skc18,skc21,skc22) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l26,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l20,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l163,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l205,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l229,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l230,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l231,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l63,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l232,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l162,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l113,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l202,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l233,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l234,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l186,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l167,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l235,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l183,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l236,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l87,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l237,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l171,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l238,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l206,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l239,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l179,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l240,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l36,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l241,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l40,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l195,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l97,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l112,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l254,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l267,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l73,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l68,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l176,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l246,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l76,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l89,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l116,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l115,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l268,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l71,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l248,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l172,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l269,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l251,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l270,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l245,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l256,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l119,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l271,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l249,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l100,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l272,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l273,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l165,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l95,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l247,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l188,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l242,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l28,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l274,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l275,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l276,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l190,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l42,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l75,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l277,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l96,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l265,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l173,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l253,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l278,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l187,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l279,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l280,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l109,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l281,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l282,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l121,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l283,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l83,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l284,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l168,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l57,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l285,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l178,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l286,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l105,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l287,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l114,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l244,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l56,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l288,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l289,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l290,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l123,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l291,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l292,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l293,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l294,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l106,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l295,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l197,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l296,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l94,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l297,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l257,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l74,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l298,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l250,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l299,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l185,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l300,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l301,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l92,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l302,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l252,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l303,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l304,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l305,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l306,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l307,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l93,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l308,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l203,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l309,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l310,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l311,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l108,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l312,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l313,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l110,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l194,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l314,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l315,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l316,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l317,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l318,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l319,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l320,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l258,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l122,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l321,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l322,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l323,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l88,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l324,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l128,plain,
( ~ ssSkC0
| ~ actual_world(skc12)
| ~ old(skc12,skc14)
| ~ present(skc12,skc13)
| ~ hollywood_placename(skc12,skc15)
| ~ dirty(skc12,skc14)
| ~ chevy(skc12,skc14)
| ~ white(skc12,skc14)
| ~ barrel(skc12,skc13)
| ~ lonely(skc12,skc17)
| ~ street(skc12,skc17)
| ~ event(skc12,skc13)
| ~ city(skc12,skc16)
| ~ placename(skc12,skc15)
| ~ down(skc12,skc13,skc17)
| ~ agent(skc12,skc13,skc14)
| ~ in(skc12,skc13,skc16)
| ~ of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l325,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l326,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l327,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l328,plain,
( ~ ssSkC0
| barrel(skc12,skc13) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l329,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l51,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l330,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l77,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l331,plain,
( ~ ssSkC0
| dirty(skc12,skc14) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l332,plain,
( ~ ssSkC0
| street(skc12,skc17) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l333,plain,
( ~ ssSkC0
| agent(skc12,skc13,skc14) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l152,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l334,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l103,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l335,plain,
actual_world(skc12),
inference(instantiation,[status(thm)],[1]) ).
cnf(l336,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l84,plain,
( ~ ssSkC0
| event(skc12,skc13) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l337,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l338,plain,
( ~ ssSkC0
| old(skc12,skc14) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l339,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l340,plain,
( ~ ssSkC0
| chevy(skc12,skc14) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l200,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l55,plain,
( ~ ssSkC0
| in(skc12,skc13,skc16) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l341,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l342,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l343,plain,
( ~ ssSkC0
| hollywood_placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l131,plain,
( ~ ssSkC0
| placename(skc12,skc15) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l255,plain,
( ~ ssSkC0
| lonely(skc12,skc17) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l344,plain,
( ~ ssSkC0
| of(skc12,skc15,skc16) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l345,plain,
( ~ ssSkC0
| city(skc12,skc16) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l346,plain,
( ~ ssSkC0
| down(skc12,skc13,skc17) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l347,plain,
( ~ ssSkC0
| white(skc12,skc14) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l348,plain,
( ~ ssSkC0
| present(skc12,skc13) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l33,l79,l29,l65,l124,l78,l125,l126,l102,l132,l39,l133,l127,l53,l35,l48,l66,l15,l16,l134,l101,l129,l21,l61,l135,l136,l137,l138,l139,l24,l32,l59,l54,l91,l140,l52,l82,l37,l31,l49,l22,l141,l85,l142,l86,l143,l144,l30,l17,l145,l146,l147,l47,l148,l149,l25,l154,l80,l155,l156,l43,l34,l157,l158,l58,l60,l81,l159,l62,l50,l69,l90,l160,l161,l151,l64,l193,l170,l207,l208,l14,l107,l166,l209,l181,l210,l211,l45,l212,l213,l184,l214,l198,l70,l215,l174,l67,l216,l217,l38,l218,l219,l220,l182,l189,l111,l221,l117,l27,l222,l191,l19,l23,l223,l224,l169,l44,l201,l225,l226,l227,l228,l150,l130,l26,l20,l163,l205,l229,l230,l231,l63,l232,l162,l113,l202,l233,l234,l186,l167,l235,l183,l236,l87,l237,l171,l238,l206,l239,l179,l240,l36,l241,l40,l195,l97,l112,l254,l267,l73,l68,l176,l246,l76,l89,l116,l115,l268,l71,l248,l172,l269,l251,l270,l245,l256,l119,l271,l249,l100,l272,l273,l165,l95,l247,l188,l242,l28,l274,l275,l276,l190,l42,l75,l277,l96,l265,l173,l253,l278,l187,l279,l280,l109,l281,l282,l121,l283,l83,l284,l168,l57,l285,l178,l286,l105,l287,l114,l244,l56,l288,l289,l290,l123,l291,l292,l293,l294,l106,l295,l197,l296,l94,l297,l257,l74,l298,l250,l299,l185,l300,l301,l92,l302,l252,l303,l304,l305,l306,l307,l93,l308,l203,l309,l310,l311,l108,l312,l313,l110,l194,l314,l315,l316,l317,l318,l319,l320,l258,l122,l321,l322,l323,l88,l324,l128,l325,l326,l327,l328,l329,l51,l330,l77,l331,l332,l333,l152,l334,l103,l335,l336,l84,l337,l338,l339,l340,l200,l55,l341,l342,l343,l131,l255,l344,l345,l346,l347,l348]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP117-1 : TPTP v9.0.0. Released v2.4.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Jul 21 08:49:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.35 % launching worker at depth: 1
% 0.13/0.35 % launching worker at depth: 6
% 0.13/0.35 % launching worker at depth: 2
% 0.13/0.35 % launching worker at depth: 3
% 0.13/0.35 % launching worker at depth: 5
% 0.13/0.35 % launching worker at depth: 7
% 0.13/0.35 % launching worker at depth: 8
% 0.13/0.35 % launching worker at depth: 4
% 0.13/0.35 % launching worker at depth: 9
% 0.13/0.38 % SZS status Theorem for theBenchmark
% 0.13/0.38 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------