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