%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP004-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 : n028.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:20 AM UTC 2025
% Result : Unsatisfiable 224.67s 28.63s
% Output : CNFRefutation 224.67s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause59)
% Comments :
%------------------------------------------------------------------------------
cnf(58,plain,
( ~ old(X0)
| ~ hollywood(X1)
| ~ seat(X2)
| ~ seat(X3)
| ~ fellow(X4)
| ~ fellow(X5)
| ~ street(X6)
| ~ event(X7)
| ~ front(X2)
| ~ front(X3)
| ~ furniture(X2)
| ~ furniture(X3)
| ~ white(X0)
| ~ car(X0)
| ~ city(X1)
| ~ dirty(X0)
| ~ young(X4)
| ~ young(X5)
| ~ chevy(X0)
| ~ lonely(X6)
| ~ man(X4)
| ~ man(X5)
| ~ way(X6)
| ~ in(X7,X1)
| ~ in(X4,X2)
| ~ in(X5,X3)
| ~ down(X7,X6)
| ~ barrel(X7,X0)
| ssSkC0
| X5 = X4 ),
inference(cnf,[status(esa)],[clause59]) ).
cnf(l0,plain,
( ~ old(skc21)
| ~ hollywood(skc23)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ street(skc20)
| ~ event(skc22)
| ~ front(skc19)
| ~ front(skc18)
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ white(skc21)
| ~ car(skc21)
| ~ city(skc23)
| ~ dirty(skc21)
| ~ young(skc16)
| ~ young(skc17)
| ~ chevy(skc21)
| ~ lonely(skc20)
| ~ man(skc16)
| ~ man(skc17)
| ~ way(skc20)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ down(skc22,skc20)
| ~ barrel(skc22,skc21)
| ssSkC0
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(42,plain,
( ~ ssSkC0
| front(skc18) ),
inference(cnf,[status(esa)],[clause43]) ).
cnf(l7606,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(36,plain,
( ~ ssSkC0
| car(skc21) ),
inference(cnf,[status(esa)],[clause37]) ).
cnf(l7713,plain,
( ~ ssSkC0
| car(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(44,plain,
( ~ ssSkC0
| young(skc17) ),
inference(cnf,[status(esa)],[clause45]) ).
cnf(l7603,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(57,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(cnf,[status(esa)],[clause58]) ).
cnf(l7608,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(10,plain,
chevy(skc21),
inference(cnf,[status(esa)],[clause11]) ).
cnf(l7675,plain,
chevy(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(52,plain,
( ~ ssSkC0
| down(skc22,skc20) ),
inference(cnf,[status(esa)],[clause53]) ).
cnf(l7595,plain,
( ~ ssSkC0
| down(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(35,plain,
( ~ ssSkC0
| white(skc21) ),
inference(cnf,[status(esa)],[clause36]) ).
cnf(l7590,plain,
( ~ ssSkC0
| white(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(9,plain,
event(skc22),
inference(cnf,[status(esa)],[clause10]) ).
cnf(l7589,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(41,plain,
( ~ ssSkC0
| man(skc16) ),
inference(cnf,[status(esa)],[clause42]) ).
cnf(l7676,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l7764,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(39,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(cnf,[status(esa)],[clause40]) ).
cnf(l7742,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(31,plain,
( ~ ssSkC0
| street(skc20) ),
inference(cnf,[status(esa)],[clause32]) ).
cnf(l7591,plain,
( ~ ssSkC0
| street(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(56,plain,
( skc25 != skc24
| ssSkC0 ),
inference(cnf,[status(esa)],[clause57]) ).
cnf(l7596,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(18,plain,
( white(skc28)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause19]) ).
cnf(l7613,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(54,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(cnf,[status(esa)],[clause55]) ).
cnf(l7649,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(24,plain,
( furniture(skc27)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause25]) ).
cnf(l7615,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(40,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(cnf,[status(esa)],[clause41]) ).
cnf(l7684,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(12,plain,
front(skc19),
inference(cnf,[status(esa)],[clause13]) ).
cnf(l7739,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(34,plain,
( ~ ssSkC0
| dirty(skc21) ),
inference(cnf,[status(esa)],[clause35]) ).
cnf(l7597,plain,
( ~ ssSkC0
| dirty(skc21) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(47,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(cnf,[status(esa)],[clause48]) ).
cnf(l7624,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(19,plain,
( ssSkC0
| dirty(skc28) ),
inference(cnf,[status(esa)],[clause20]) ).
cnf(l7639,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7938,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l7601,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(48,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(cnf,[status(esa)],[clause49]) ).
cnf(l9956,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(15,plain,
young(skc16),
inference(cnf,[status(esa)],[clause16]) ).
cnf(l7611,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(21,plain,
( ssSkC0
| way(skc29) ),
inference(cnf,[status(esa)],[clause22]) ).
cnf(l12448,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7707,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(20,plain,
( ssSkC0
| lonely(skc29) ),
inference(cnf,[status(esa)],[clause21]) ).
cnf(l11870,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l13992,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(16,plain,
( ssSkC0
| chevy(skc28) ),
inference(cnf,[status(esa)],[clause17]) ).
cnf(l9196,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11871,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(26,plain,
( ssSkC0
| man(skc24) ),
inference(cnf,[status(esa)],[clause27]) ).
cnf(l20331,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(59,plain,
( ~ old(X0)
| ~ hollywood(X1)
| ~ seat(X2)
| ~ seat(X3)
| ~ fellow(X4)
| ~ fellow(X5)
| ~ street(X6)
| ~ event(X7)
| ~ front(X2)
| ~ front(X3)
| ~ furniture(X2)
| ~ furniture(X3)
| ~ white(X0)
| ~ car(X0)
| ~ city(X1)
| ~ ssSkC0
| ~ dirty(X0)
| ~ young(X4)
| ~ young(X5)
| ~ chevy(X0)
| ~ lonely(X6)
| ~ man(X4)
| ~ man(X5)
| ~ way(X6)
| ~ in(X7,X1)
| ~ in(X4,X2)
| ~ in(X5,X3)
| ~ down(X7,X6)
| ~ barrel(X7,X0)
| X5 = X4 ),
inference(cnf,[status(esa)],[clause60]) ).
cnf(l8075,plain,
( ~ old(skc21)
| ~ hollywood(skc23)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ street(skc20)
| ~ event(skc22)
| ~ front(skc19)
| ~ front(skc18)
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ white(skc21)
| ~ car(skc21)
| ~ city(skc23)
| ~ ssSkC0
| ~ dirty(skc21)
| ~ young(skc16)
| ~ young(skc17)
| ~ chevy(skc21)
| ~ lonely(skc20)
| ~ man(skc16)
| ~ man(skc17)
| ~ way(skc20)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ down(skc22,skc20)
| ~ barrel(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(4,plain,
front(skc27),
inference(cnf,[status(esa)],[clause5]) ).
cnf(l12457,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(33,plain,
( ~ ssSkC0
| old(skc21) ),
inference(cnf,[status(esa)],[clause34]) ).
cnf(l1,plain,
( ~ ssSkC0
| old(skc21) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(8,plain,
hollywood(skc23),
inference(cnf,[status(esa)],[clause9]) ).
cnf(l3327,plain,
hollywood(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(37,plain,
( ~ ssSkC0
| city(skc23) ),
inference(cnf,[status(esa)],[clause38]) ).
cnf(l8192,plain,
( ~ ssSkC0
| city(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l7677,plain,
( ~ ssSkC0
| city(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l12458,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(46,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(cnf,[status(esa)],[clause47]) ).
cnf(l9957,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(13,plain,
seat(skc18),
inference(cnf,[status(esa)],[clause14]) ).
cnf(l7598,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(28,plain,
( furniture(skc26)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause29]) ).
cnf(l9191,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8203,plain,
chevy(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(25,plain,
( fellow(skc24)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause26]) ).
cnf(l12434,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(29,plain,
( ssSkC0
| young(skc25) ),
inference(cnf,[status(esa)],[clause30]) ).
cnf(l9445,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7712,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(49,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(cnf,[status(esa)],[clause50]) ).
cnf(l13868,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l14027,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8291,plain,
hollywood(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(30,plain,
( ssSkC0
| man(skc25) ),
inference(cnf,[status(esa)],[clause31]) ).
cnf(l12454,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(7,plain,
young(skc24),
inference(cnf,[status(esa)],[clause8]) ).
cnf(l9184,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8289,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l20307,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(14,plain,
fellow(skc17),
inference(cnf,[status(esa)],[clause15]) ).
cnf(l7593,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l12532,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(50,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(cnf,[status(esa)],[clause51]) ).
cnf(l9190,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9739,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l9187,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l13876,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(1,plain,
event(skc30),
inference(cnf,[status(esa)],[clause2]) ).
cnf(l13872,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(38,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(cnf,[status(esa)],[clause39]) ).
cnf(l7637,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l12608,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(5,plain,
seat(skc26),
inference(cnf,[status(esa)],[clause6]) ).
cnf(l12533,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(22,plain,
( city(skc31)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause23]) ).
cnf(l7801,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l13895,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l20304,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l9183,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(51,plain,
( ~ ssSkC0
| barrel(skc22,skc21) ),
inference(cnf,[status(esa)],[clause52]) ).
cnf(l9542,plain,
( ~ ssSkC0
| barrel(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l8356,plain,
( ~ ssSkC0
| car(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l9510,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(3,plain,
old(skc28),
inference(cnf,[status(esa)],[clause4]) ).
cnf(l7610,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12436,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8183,plain,
( ~ ssSkC0
| old(skc21) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8326,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l7759,plain,
( ~ ssSkC0
| barrel(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l8187,plain,
( ~ ssSkC0
| street(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8197,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l13875,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8332,plain,
( ~ ssSkC0
| dirty(skc21) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(23,plain,
( seat(skc27)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause24]) ).
cnf(l9182,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l20305,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l20301,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l13764,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12435,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(17,plain,
( car(skc28)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause18]) ).
cnf(l9195,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8199,plain,
( ~ ssSkC0
| down(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(27,plain,
( front(skc26)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause28]) ).
cnf(l9185,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l13894,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l12606,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l20333,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l8193,plain,
( ~ ssSkC0
| white(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l20337,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13873,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(55,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(cnf,[status(esa)],[clause56]) ).
cnf(l8742,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(53,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(cnf,[status(esa)],[clause54]) ).
cnf(l7594,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l2,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8590,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l13870,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11181,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(2,plain,
street(skc29),
inference(cnf,[status(esa)],[clause3]) ).
cnf(l13765,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(0,plain,
hollywood(skc31),
inference(cnf,[status(esa)],[clause1]) ).
cnf(l9545,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l13890,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11189,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9471,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11185,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l11172,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l20338,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8016,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l10721,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l12611,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l13880,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l11237,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l11193,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11190,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l14030,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8017,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l20299,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l20332,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10552,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(32,plain,
( ~ ssSkC0
| way(skc20) ),
inference(cnf,[status(esa)],[clause33]) ).
cnf(l7607,plain,
( ~ ssSkC0
| way(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8198,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l11171,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l7659,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l10204,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8173,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(43,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(cnf,[status(esa)],[clause44]) ).
cnf(l8184,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l10208,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(11,plain,
lonely(skc20),
inference(cnf,[status(esa)],[clause12]) ).
cnf(l8202,plain,
lonely(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l8093,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l13888,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l13929,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12568,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8120,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l20336,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l12531,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l13600,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l20311,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11213,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7868,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12441,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l10018,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l11905,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12526,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l12586,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8185,plain,
( ~ ssSkC0
| way(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l14152,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l13613,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13585,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l9497,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l9922,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12412,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l9927,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11166,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13878,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l10145,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7753,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l12575,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l13338,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8283,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l9498,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12581,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(6,plain,
fellow(skc25),
inference(cnf,[status(esa)],[clause7]) ).
cnf(l12589,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l13869,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l12618,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12559,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10551,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l11921,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l8100,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9933,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l10261,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11206,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l14033,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8362,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11542,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11169,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l11577,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(45,plain,
( ~ ssSkC0
| man(skc17) ),
inference(cnf,[status(esa)],[clause46]) ).
cnf(l8303,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l11736,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8440,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12449,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l15440,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l11176,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8112,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12309,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9477,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l10431,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l11202,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9918,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l10264,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l20308,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8109,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l13951,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l10433,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10716,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l11907,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l15441,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l13950,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13763,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l13968,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l12573,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l11561,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l8495,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8101,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l11558,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l20306,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l11204,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l8374,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11491,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13879,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l12555,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8386,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l12188,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l13966,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10430,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l13949,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8377,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l10206,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l13174,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l11606,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8373,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8186,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l8391,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l9868,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l20300,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7688,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12050,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12053,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l8693,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l13214,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8102,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l12578,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l17678,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l20302,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12569,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11919,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8125,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8380,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l8196,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l11447,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12530,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l9084,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9919,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l11862,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l8359,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l11560,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8347,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l11526,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l8371,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l10779,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l14694,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l12062,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11552,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11444,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l12056,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l8348,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l9108,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9088,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9501,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l14695,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l10550,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l13175,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9930,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9030,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9921,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8360,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l13173,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8378,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9092,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11165,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9056,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l11548,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l9034,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l13965,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l14777,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l11446,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8292,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9194,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l9028,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8387,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l12035,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l9186,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l9087,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l12040,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12474,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9473,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8077,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l8097,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7602,plain,
lonely(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l9099,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11442,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12031,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10201,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l11909,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l9038,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8098,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8290,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8096,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8065,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11445,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l14137,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7929,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l16816,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l13147,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l12558,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l9122,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l20309,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l13249,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l14023,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l13186,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l11201,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l9079,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11545,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l16834,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l12765,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l8130,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l11579,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8110,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l8106,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l12557,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8095,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l11175,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l10214,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11441,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l10588,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l20310,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l2911,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l11392,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8363,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l7835,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l20298,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8543,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l13165,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l14693,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8529,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l12034,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12028,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l13250,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l17975,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8535,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l2915,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8521,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l12060,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9042,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l16141,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8520,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l14028,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l20334,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l18022,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l8416,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l14157,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l10158,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l8515,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l7863,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l13154,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2908,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l11180,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2906,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l13164,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l12565,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l13185,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8523,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l13153,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l9051,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l11872,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8554,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l10267,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8256,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l12897,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l11918,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l13182,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8557,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12214,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13109,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l13242,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l12110,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l12282,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l12617,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l2815,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l12213,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l8423,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8510,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l13194,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l13191,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8367,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9054,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l2809,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12218,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2903,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2806,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9667,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l11026,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l19964,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l8417,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12210,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l8793,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l12561,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l13190,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8191,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l10292,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l8414,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l11753,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l11747,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l13241,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l11750,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l12113,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l11914,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l11790,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l2814,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l12753,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11778,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12123,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12047,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9031,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l13889,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l11187,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l2916,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2902,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8278,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l11833,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l204,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l14696,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8716,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l11758,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l10262,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2923,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l11776,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l2905,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l8518,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l9095,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8385,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11743,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9049,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12042,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l13101,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8115,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12483,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11449,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l11912,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l11692,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7616,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l12212,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l13112,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9029,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l11751,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2821,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2811,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12046,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l14136,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l16094,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8803,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l13885,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l8361,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8514,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l7617,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12216,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l13102,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12122,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2812,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1595,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l11678,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8478,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l11443,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l16093,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l11799,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11742,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11829,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l8274,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11756,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8389,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8136,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l9123,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l7894,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l7905,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7946,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l8021,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11781,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l11749,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l7919,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8540,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12285,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9081,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l7957,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l11757,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7915,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l2807,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l12219,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8388,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l13286,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2823,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2909,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l16817,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l13177,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l7989,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l7910,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8565,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l9994,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7936,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l8123,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7941,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9121,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l12032,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l14061,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l9844,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l16835,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l11785,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12584,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l2820,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7908,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8561,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l12560,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l16826,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8190,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l10170,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l7727,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l7934,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l20303,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l7932,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l20335,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7978,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l10127,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8564,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l11780,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l7928,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l8024,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l12088,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l8027,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l17825,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l10365,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l11890,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l7945,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l9058,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2925,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l12121,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2904,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l9262,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l11690,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l11186,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7914,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8375,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10212,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11752,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l13251,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l11873,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l12089,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l7900,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8127,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8502,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l10494,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l9102,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l10074,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l10114,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l11529,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l8231,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l10106,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l10109,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13326,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8627,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l10103,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l7968,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8124,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l9985,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9842,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l10124,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10108,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l10107,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l9841,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l10113,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l12115,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l9502,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l7907,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7933,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9264,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l11788,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l8384,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8541,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l10133,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l10115,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8468,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l12710,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2810,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8469,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12724,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l7994,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12623,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l7896,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11733,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l10228,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2808,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l14647,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l12723,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7631,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12217,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12713,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l10361,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8567,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l10227,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l12735,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l18415,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l10226,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l11741,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l12708,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8470,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l12749,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l9033,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l7698,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l11597,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l12734,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l12739,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2813,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l7943,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l12698,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12707,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l12733,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l10116,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l11744,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l12711,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l11528,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l12699,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l7901,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l12726,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l12714,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l12118,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8025,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l10362,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l12029,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l12624,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l7679,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l12013,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9895,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l9899,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9909,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l9896,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9904,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l9900,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l10392,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9913,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9897,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l12730,plain,
( seat(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l10400,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l7680,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9890,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12732,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l7687,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10396,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l11986,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9906,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8288,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l10398,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10403,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7689,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l10388,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l11997,plain,
( ~ old(skc28)
| ~ hollywood(skc31)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ street(skc29)
| ~ event(skc30)
| ~ front(skc27)
| ~ front(skc26)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ white(skc28)
| ~ car(skc28)
| ~ city(skc31)
| ~ dirty(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ chevy(skc28)
| ~ lonely(skc29)
| ~ man(skc24)
| ~ man(skc25)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ down(skc30,skc29)
| ~ barrel(skc30,skc28)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l9892,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l12174,plain,
( ssSkC0
| lonely(skc29) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l12179,plain,
( ssSkC0
| chevy(skc28) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l12139,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l12038,plain,
hollywood(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(l12161,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l13319,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l12953,plain,
( city(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l12163,plain,
street(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l11971,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l12164,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l12025,plain,
old(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l12142,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l9889,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l10387,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l7895,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l7683,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l12173,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9901,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l12166,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l14637,plain,
( ssSkC0
| man(skc24) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l13289,plain,
( ssSkC0
| man(skc25) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l12172,plain,
front(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l12169,plain,
seat(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l13293,plain,
( furniture(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7685,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l15218,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l12170,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l13291,plain,
( ssSkC0
| dirty(skc28) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l12177,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l13321,plain,
( furniture(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l12162,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l12144,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l12960,plain,
( ssSkC0
| young(skc25) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l14634,plain,
( front(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l12138,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l7606,l7713,l7603,l7608,l7675,l7595,l7590,l7589,l7676,l7764,l7742,l7591,l7596,l7613,l7649,l7615,l7684,l7739,l7597,l7624,l7639,l7938,l7601,l9956,l7611,l12448,l7707,l11870,l13992,l9196,l11871,l20331,l8075,l12457,l1,l3327,l8192,l7677,l12458,l9957,l7598,l9191,l8203,l12434,l9445,l7712,l13868,l14027,l8291,l12454,l9184,l8289,l20307,l7593,l12532,l9190,l9739,l9187,l13876,l13872,l7637,l12608,l12533,l7801,l13895,l20304,l9183,l9542,l8356,l9510,l7610,l12436,l8183,l8326,l7759,l8187,l8197,l13875,l8332,l9182,l20305,l20301,l13764,l12435,l9195,l8199,l9185,l13894,l12606,l20333,l8193,l20337,l13873,l8742,l7594,l2,l8590,l13870,l11181,l13765,l9545,l13890,l11189,l9471,l11185,l11172,l20338,l8016,l10721,l12611,l13880,l11237,l11193,l11190,l14030,l8017,l20299,l20332,l10552,l7607,l8198,l11171,l7659,l10204,l8173,l8184,l10208,l8202,l8093,l13888,l13929,l12568,l8120,l20336,l12531,l13600,l20311,l11213,l7868,l12441,l10018,l11905,l12526,l12586,l8185,l14152,l13613,l13585,l9497,l9922,l12412,l9927,l11166,l13878,l10145,l7753,l12575,l13338,l8283,l9498,l12581,l12589,l13869,l12618,l12559,l10551,l11921,l8100,l9933,l10261,l11206,l14033,l8362,l11542,l11169,l11577,l8303,l11736,l8440,l12449,l15440,l11176,l8112,l12309,l9477,l10431,l11202,l9918,l10264,l20308,l8109,l13951,l10433,l10716,l11907,l15441,l13950,l13763,l13968,l12573,l11561,l8495,l8101,l11558,l20306,l11204,l8374,l11491,l13879,l12555,l8386,l12188,l13966,l10430,l13949,l8377,l10206,l13174,l11606,l8373,l8186,l8391,l9868,l20300,l7688,l12050,l12053,l8693,l13214,l8102,l12578,l17678,l20302,l12569,l11919,l8125,l8380,l8196,l11447,l12530,l9084,l9919,l11862,l8359,l11560,l8347,l11526,l8371,l10779,l14694,l12062,l11552,l11444,l12056,l8348,l9108,l9088,l9501,l14695,l10550,l13175,l9930,l9030,l9921,l8360,l13173,l8378,l9092,l11165,l9056,l11548,l9034,l13965,l14777,l11446,l8292,l9194,l9028,l8387,l12035,l9186,l9087,l12040,l12474,l9473,l8077,l8097,l7602,l9099,l11442,l12031,l10201,l11909,l9038,l8098,l8290,l8096,l8065,l11445,l14137,l7929,l16816,l13147,l12558,l9122,l20309,l13249,l14023,l13186,l11201,l9079,l11545,l16834,l12765,l8130,l11579,l8110,l8106,l12557,l8095,l11175,l10214,l11441,l10588,l6,l20310,l2911,l11392,l8363,l7835,l20298,l8543,l13165,l14693,l8529,l12034,l12028,l13250,l17975,l8535,l2915,l8521,l12060,l9042,l16141,l8520,l14028,l20334,l18022,l8416,l14157,l10158,l8515,l7863,l13154,l2908,l11180,l2906,l13164,l12565,l13185,l8523,l13153,l9051,l11872,l8554,l10267,l8256,l12897,l11918,l13182,l8557,l12214,l13109,l13242,l12110,l12282,l12617,l2815,l12213,l8423,l8510,l13194,l13191,l8367,l9054,l2809,l12218,l2903,l2806,l9667,l11026,l19964,l8417,l12210,l8793,l12561,l13190,l8191,l10292,l8414,l11753,l11747,l13241,l11750,l12113,l11914,l11790,l2814,l12753,l11778,l12123,l12047,l9031,l13889,l11187,l2916,l2902,l8278,l11833,l204,l14696,l8716,l11758,l10262,l2923,l11776,l2905,l8518,l9095,l8385,l11743,l9049,l12042,l13101,l8115,l12483,l11449,l11912,l11692,l7616,l12212,l13112,l9029,l11751,l2821,l2811,l12046,l14136,l16094,l8803,l13885,l8361,l8514,l7617,l12216,l13102,l12122,l2812,l1595,l11678,l8478,l11443,l16093,l11799,l11742,l11829,l8274,l11756,l8389,l8136,l9123,l7894,l7905,l7946,l8021,l11781,l11749,l7919,l8540,l12285,l9081,l7957,l11757,l7915,l2807,l12219,l8388,l13286,l2823,l2909,l16817,l13177,l7989,l7910,l8565,l9994,l7936,l8123,l7941,l9121,l12032,l14061,l9844,l16835,l11785,l12584,l2820,l7908,l8561,l12560,l16826,l8190,l10170,l7727,l7934,l20303,l7932,l20335,l7978,l10127,l8564,l11780,l7928,l8024,l12088,l8027,l17825,l10365,l11890,l7945,l9058,l2925,l12121,l2904,l9262,l11690,l11186,l7914,l8375,l10212,l11752,l13251,l11873,l12089,l7900,l8127,l8502,l10494,l9102,l10074,l10114,l11529,l8231,l10106,l10109,l13326,l8627,l10103,l7968,l8124,l9985,l9842,l10124,l10108,l10107,l9841,l10113,l12115,l9502,l7907,l7933,l9264,l11788,l8384,l8541,l10133,l10115,l8468,l12710,l2810,l8469,l12724,l7994,l12623,l7896,l11733,l10228,l2808,l14647,l12723,l7631,l12217,l12713,l10361,l8567,l10227,l12735,l18415,l10226,l11741,l12708,l8470,l12749,l9033,l7698,l11597,l12734,l12739,l2813,l7943,l12698,l12707,l12733,l10116,l11744,l12711,l11528,l12699,l7901,l12726,l12714,l12118,l8025,l10362,l12029,l12624,l7679,l12013,l9895,l9899,l9909,l9896,l9904,l9900,l10392,l9913,l9897,l12730,l10400,l7680,l9890,l12732,l7687,l10396,l11986,l9906,l8288,l10398,l10403,l7689,l10388,l11997,l9892,l12174,l12179,l12139,l12038,l12161,l13319,l12953,l12163,l11971,l12164,l12025,l12142,l9889,l10387,l7895,l7683,l12173,l9901,l12166,l14637,l13289,l12172,l12169,l13293,l7685,l15218,l12170,l13291,l12177,l13321,l12162,l12144,l12960,l14634,l12138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP004-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.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 21 07:51:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.33 % launching worker at depth: 1
% 0.12/0.33 % launching worker at depth: 5
% 0.12/0.33 % launching worker at depth: 4
% 0.12/0.33 % launching worker at depth: 6
% 0.12/0.33 % launching worker at depth: 2
% 0.12/0.33 % launching worker at depth: 3
% 0.12/0.33 % launching worker at depth: 7
% 0.12/0.33 % launching worker at depth: 8
% 0.18/0.46 % launching worker at depth: 9
% 2.59/0.71 % launching worker at depth: 10
% 19.27/2.82 % launching worker at depth: 11
% 224.67/28.63 % SZS status Theorem for theBenchmark
% 224.67/28.63 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------