%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP011-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 : n022.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:22 AM UTC 2025
% Result : Unsatisfiable 277.53s 35.42s
% Output : CNFRefutation 278.14s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause1)
% Comments :
%------------------------------------------------------------------------------
cnf(0,plain,
city(skc31),
inference(cnf,[status(esa)],[clause1]) ).
cnf(l0,plain,
city(skc31),
inference(instantiation,[status(thm)],[0]) ).
cnf(58,plain,
( ~ chevy(X0)
| ~ city(X1)
| ~ front(X2)
| ~ front(X3)
| ~ fellow(X4)
| ~ fellow(X5)
| ~ lonely(X6)
| ~ event(X7)
| ~ seat(X2)
| ~ seat(X3)
| ~ man(X4)
| ~ man(X5)
| ~ car(X0)
| ~ white(X0)
| ~ street(X6)
| ~ dirty(X0)
| ~ hollywood(X1)
| ~ old(X0)
| ~ young(X4)
| ~ young(X5)
| ~ furniture(X2)
| ~ furniture(X3)
| ~ way(X6)
| ~ in(X7,X1)
| ~ in(X4,X2)
| ~ in(X5,X3)
| ~ barrel(X7,X0)
| ~ down(X7,X6)
| ssSkC0
| X5 = X4 ),
inference(cnf,[status(esa)],[clause59]) ).
cnf(l1,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc16)
| ~ young(skc17)
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(19,plain,
( car(skc28)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause20]) ).
cnf(l68,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(1,plain,
event(skc30),
inference(cnf,[status(esa)],[clause2]) ).
cnf(l26,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(46,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(cnf,[status(esa)],[clause47]) ).
cnf(l23,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(44,plain,
( ~ ssSkC0
| young(skc17) ),
inference(cnf,[status(esa)],[clause45]) ).
cnf(l8,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(27,plain,
( young(skc25)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause28]) ).
cnf(l46,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(14,plain,
fellow(skc17),
inference(cnf,[status(esa)],[clause15]) ).
cnf(l69,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(13,plain,
seat(skc18),
inference(cnf,[status(esa)],[clause14]) ).
cnf(l3,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(41,plain,
( ~ ssSkC0
| man(skc16) ),
inference(cnf,[status(esa)],[clause42]) ).
cnf(l65,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(52,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(cnf,[status(esa)],[clause53]) ).
cnf(l868,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(18,plain,
( white(skc28)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause19]) ).
cnf(l7,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(39,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(cnf,[status(esa)],[clause40]) ).
cnf(l21,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(16,plain,
( old(skc28)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause17]) ).
cnf(l40,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(12,plain,
front(skc19),
inference(cnf,[status(esa)],[clause13]) ).
cnf(l4,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(35,plain,
( ~ ssSkC0
| street(skc21) ),
inference(cnf,[status(esa)],[clause36]) ).
cnf(l33,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(40,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(cnf,[status(esa)],[clause41]) ).
cnf(l128,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(51,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(cnf,[status(esa)],[clause52]) ).
cnf(l18,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(3,plain,
chevy(skc28),
inference(cnf,[status(esa)],[clause4]) ).
cnf(l2,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(20,plain,
( street(skc29)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause21]) ).
cnf(l84,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l113,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(59,plain,
( ~ chevy(X0)
| ~ city(X1)
| ~ front(X2)
| ~ front(X3)
| ~ fellow(X4)
| ~ fellow(X5)
| ~ lonely(X6)
| ~ event(X7)
| ~ seat(X2)
| ~ seat(X3)
| ~ man(X4)
| ~ man(X5)
| ~ car(X0)
| ~ white(X0)
| ~ street(X6)
| ~ dirty(X0)
| ~ hollywood(X1)
| ~ old(X0)
| ~ young(X4)
| ~ young(X5)
| ~ ssSkC0
| ~ furniture(X2)
| ~ furniture(X3)
| ~ way(X6)
| ~ in(X7,X1)
| ~ in(X4,X2)
| ~ in(X5,X3)
| ~ barrel(X7,X0)
| ~ down(X7,X6)
| X5 = X4 ),
inference(cnf,[status(esa)],[clause60]) ).
cnf(l4354,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(42,plain,
( ~ ssSkC0
| front(skc18) ),
inference(cnf,[status(esa)],[clause43]) ).
cnf(l4360,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l5365,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(8,plain,
city(skc23),
inference(cnf,[status(esa)],[clause9]) ).
cnf(l4378,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(57,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(cnf,[status(esa)],[clause58]) ).
cnf(l17,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(32,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(cnf,[status(esa)],[clause33]) ).
cnf(l4851,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l5691,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(31,plain,
( ~ ssSkC0
| old(skc20) ),
inference(cnf,[status(esa)],[clause32]) ).
cnf(l5810,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5376,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(38,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(cnf,[status(esa)],[clause39]) ).
cnf(l9,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l5685,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l151,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l174,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(50,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(cnf,[status(esa)],[clause51]) ).
cnf(l152,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(30,plain,
( ssSkC0
| furniture(skc26) ),
inference(cnf,[status(esa)],[clause31]) ).
cnf(l6561,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l238,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l241,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(21,plain,
( ssSkC0
| way(skc29) ),
inference(cnf,[status(esa)],[clause22]) ).
cnf(l72,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(49,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(cnf,[status(esa)],[clause50]) ).
cnf(l173,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(5,plain,
front(skc26),
inference(cnf,[status(esa)],[clause6]) ).
cnf(l394,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(47,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(cnf,[status(esa)],[clause48]) ).
cnf(l10,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l19,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l8993,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l8987,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l164,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(36,plain,
( ~ ssSkC0
| way(skc21) ),
inference(cnf,[status(esa)],[clause37]) ).
cnf(l5813,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(26,plain,
( ssSkC0
| furniture(skc27) ),
inference(cnf,[status(esa)],[clause27]) ).
cnf(l294,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(22,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause23]) ).
cnf(l6607,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l359,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(17,plain,
( dirty(skc28)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause18]) ).
cnf(l6555,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(25,plain,
( front(skc27)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause26]) ).
cnf(l319,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(29,plain,
( seat(skc26)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause30]) ).
cnf(l159,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l16,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(24,plain,
( man(skc24)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause25]) ).
cnf(l329,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(43,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(cnf,[status(esa)],[clause44]) ).
cnf(l354,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l155,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(54,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(cnf,[status(esa)],[clause55]) ).
cnf(l8893,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l317,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l239,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(23,plain,
( fellow(skc24)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause24]) ).
cnf(l740,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5695,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(56,plain,
( skc25 != skc24
| ssSkC0 ),
inference(cnf,[status(esa)],[clause57]) ).
cnf(l8415,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l325,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(10,plain,
lonely(skc21),
inference(cnf,[status(esa)],[clause11]) ).
cnf(l8991,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(9,plain,
event(skc22),
inference(cnf,[status(esa)],[clause10]) ).
cnf(l8813,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(34,plain,
( ~ ssSkC0
| car(skc20) ),
inference(cnf,[status(esa)],[clause35]) ).
cnf(l5814,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l11,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l787,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8816,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(45,plain,
( ~ ssSkC0
| man(skc17) ),
inference(cnf,[status(esa)],[clause46]) ).
cnf(l5369,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(37,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(cnf,[status(esa)],[clause38]) ).
cnf(l8890,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(48,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(cnf,[status(esa)],[clause49]) ).
cnf(l370,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8737,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(2,plain,
lonely(skc29),
inference(cnf,[status(esa)],[clause3]) ).
cnf(l6565,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l110,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(55,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(cnf,[status(esa)],[clause56]) ).
cnf(l5377,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l432,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l5373,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l5374,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l14,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l745,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(33,plain,
( ~ ssSkC0
| white(skc20) ),
inference(cnf,[status(esa)],[clause34]) ).
cnf(l5363,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(15,plain,
young(skc16),
inference(cnf,[status(esa)],[clause16]) ).
cnf(l5823,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(4,plain,
seat(skc27),
inference(cnf,[status(esa)],[clause5]) ).
cnf(l6583,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(28,plain,
( man(skc25)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause29]) ).
cnf(l307,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l30,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6562,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(53,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(cnf,[status(esa)],[clause54]) ).
cnf(l5368,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l754,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l301,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l180,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l8990,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l324,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l5686,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l6560,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l6564,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l302,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8999,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l338,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8681,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l5815,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l6605,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l4855,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l326,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(11,plain,
chevy(skc20),
inference(cnf,[status(esa)],[clause12]) ).
cnf(l6340,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l13,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l205,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l8998,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l121,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(6,plain,
fellow(skc25),
inference(cnf,[status(esa)],[clause7]) ).
cnf(l295,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l315,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l6609,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l92,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(7,plain,
young(skc24),
inference(cnf,[status(esa)],[clause8]) ).
cnf(l445,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l277,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5165,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l443,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l9306,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5362,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l6572,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l242,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8988,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l784,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l240,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l8683,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l149,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l660,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l6191,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l8593,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l5375,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l6908,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6193,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l4646,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l10037,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l8815,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l15,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l4451,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8794,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l293,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6553,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l6856,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l4958,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l5062,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l195,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l9753,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l10058,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l5493,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l20,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l6906,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l433,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l6918,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l8597,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l327,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l63,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l4961,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l8787,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l762,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l518,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l5950,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l284,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4974,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l4907,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l9120,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9131,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5492,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5476,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l6900,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l4980,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l6923,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l4837,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l12,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l308,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6904,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4987,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l5063,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l4685,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l10667,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9068,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5863,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l8520,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l4962,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l7087,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l7052,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l6492,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l8869,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l10059,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8862,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l5577,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l8682,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l8764,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4968,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l6969,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l7065,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l4979,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6298,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l9134,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8169,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l7037,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l5156,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l8892,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l9169,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l8859,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l8980,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l6852,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l9129,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l4852,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l7106,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l9130,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l6905,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l6928,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l11090,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l8530,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l5812,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l8785,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l4854,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l11097,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l6554,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l9755,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l10055,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10078,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7100,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l9128,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7103,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l6859,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l9127,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l5764,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8171,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l10036,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l154,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l314,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l11761,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l5361,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l6874,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l8864,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l8789,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l5031,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l10056,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8986,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l7079,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l129,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l157,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l7092,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l7515,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6296,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l9135,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5252,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc18)
| ~ front(skc19)
| ~ fellow(skc17)
| ~ fellow(skc16)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc18)
| ~ seat(skc19)
| ~ man(skc17)
| ~ man(skc16)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc17)
| ~ young(skc16)
| ~ ssSkC0
| ~ furniture(skc18)
| ~ furniture(skc19)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc17,skc18)
| ~ in(skc16,skc19)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc16 = skc17 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l6294,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l8995,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l5520,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l5776,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l299,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6234,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l8852,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l6235,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l7043,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l5519,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l8735,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l10668,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l4972,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6231,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l4986,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l8790,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8592,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l8526,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l4966,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l8589,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l7095,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l8684,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l6233,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l274,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l5517,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l4990,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l727,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l728,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9126,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8992,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l203,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l9375,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l793,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6158,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l9376,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l4733,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l726,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l6210,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l11065,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5022,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l6216,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l7067,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l5521,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l6229,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l6427,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l9119,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l15492,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l9167,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l796,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l7113,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6815,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l7038,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l7243,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l7128,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l4988,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l6909,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l4932,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7112,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l11757,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l9829,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5032,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4984,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l8391,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4938,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l6795,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l756,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l770,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l6566,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l4971,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l9125,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l9828,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8994,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l5845,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l8545,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9154,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l771,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9774,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l7125,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l6589,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l12038,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l8866,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8868,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l6922,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l9006,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l6274,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l6877,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l4947,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l10065,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l769,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l11756,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l7096,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l777,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l9124,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l5150,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l4454,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l6725,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9274,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l805,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l6880,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9975,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l8782,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6581,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l6213,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l4942,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l7093,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l9754,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l4946,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l283,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l11759,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l9271,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l4327,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l7098,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l729,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7126,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l9121,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l8863,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4940,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l285,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8313,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l228,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l9136,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l6960,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4939,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l757,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l12163,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l9182,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9208,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l8989,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4770,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l8170,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l9270,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l9832,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l10215,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l5027,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l7042,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l7088,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l4763,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l7242,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l6913,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7111,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l7914,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l10663,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10046,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l6021,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l789,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l4872,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l7047,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l935,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l175,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l6030,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l381,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l331,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l4965,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l7104,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l7122,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l6551,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l9123,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l5416,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4760,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l6548,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5903,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l4328,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l597,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l4653,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l5905,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6026,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l6212,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l8731,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6297,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4652,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l767,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4931,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l575,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l5600,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l9069,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8867,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l601,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l9775,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l9580,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1221,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l10032,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l5906,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8985,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l229,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l10052,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6584,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l9853,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l4978,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6295,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l477,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l6705,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l484,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10629,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l569,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l7247,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l66,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l577,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l5901,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l9811,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l588,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l606,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l482,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l290,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l894,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l681,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4764,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l505,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6293,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4735,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l231,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l9776,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l298,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4953,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l5020,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l103,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l568,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l801,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l487,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l6816,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l596,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l598,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l600,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7129,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l566,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l7114,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l447,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l590,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l923,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l7424,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l137,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4338,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l617,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l585,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l884,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l9132,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l184,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8521,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l282,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7425,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l5844,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l287,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l567,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l614,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l7439,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l9374,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l230,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l11101,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l620,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5212,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l6893,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l605,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l5904,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8983,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8801,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l516,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l363,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l811,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l4951,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l6545,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l581,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l501,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l9831,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l572,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l563,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l6199,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l619,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l7438,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l573,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l9187,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l5203,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l8516,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1057,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4765,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l8793,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4875,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8677,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l561,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l8708,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l5349,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l7089,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l5019,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l604,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l9138,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l347,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l618,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4759,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l5351,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l318,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l6180,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l5919,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l9168,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l493,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l602,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l584,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l7432,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l7115,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l6552,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1073,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l9118,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l7086,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l7130,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8511,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1125,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l9133,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l634,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l469,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l309,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l893,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l232,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l8499,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l616,plain,
( ~ ssSkC0
| dirty(skc20) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4325,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l570,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l9191,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l9377,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l12892,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l5206,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4981,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l9117,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l564,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l4943,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l6029,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l5907,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l622,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l320,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l5378,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6808,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l578,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l8498,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l6336,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l296,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l4689,plain,
( ~ chevy(skc20)
| ~ city(skc23)
| ~ front(skc19)
| ~ front(skc18)
| ~ fellow(skc16)
| ~ fellow(skc17)
| ~ lonely(skc21)
| ~ event(skc22)
| ~ seat(skc19)
| ~ seat(skc18)
| ~ man(skc16)
| ~ man(skc17)
| ~ car(skc20)
| ~ white(skc20)
| ~ street(skc21)
| ~ dirty(skc20)
| ~ hollywood(skc23)
| ~ old(skc20)
| ~ young(skc16)
| ~ young(skc17)
| ~ ssSkC0
| ~ furniture(skc19)
| ~ furniture(skc18)
| ~ way(skc21)
| ~ in(skc22,skc23)
| ~ in(skc16,skc19)
| ~ in(skc17,skc18)
| ~ barrel(skc22,skc20)
| ~ down(skc22,skc21)
| skc17 = skc16 ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l6457,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l970,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8333,plain,
young(skc16),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4706,plain,
( ~ ssSkC0
| man(skc16) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l8961,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l4985,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l6232,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l6200,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l11862,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l356,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l615,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l5912,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l8325,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l7090,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8798,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1071,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l9115,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l5902,plain,
chevy(skc20),
inference(instantiation,[status(thm)],[11]) ).
cnf(l8331,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l8957,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l730,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l773,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l629,plain,
( ~ ssSkC0
| seat(skc19) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l9200,plain,
( ~ ssSkC0
| street(skc21) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l7373,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l9176,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6259,plain,
city(skc23),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4768,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l10726,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1058,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1068,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l5910,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l343,plain,
( ~ ssSkC0
| old(skc20) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8336,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l5914,plain,
seat(skc18),
inference(instantiation,[status(thm)],[13]) ).
cnf(l571,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8332,plain,
( ~ ssSkC0
| furniture(skc18) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l580,plain,
( ~ ssSkC0
| barrel(skc22,skc20) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l7377,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l10665,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l4708,plain,
fellow(skc17),
inference(instantiation,[status(thm)],[14]) ).
cnf(l313,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l763,plain,
( ~ ssSkC0
| in(skc16,skc19) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l8515,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l5913,plain,
( ~ ssSkC0
| in(skc17,skc18) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l4709,plain,
( ~ ssSkC0
| front(skc18) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l758,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l304,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l5518,plain,
( ~ ssSkC0
| way(skc21) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l6590,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l6132,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l7375,plain,
event(skc22),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4707,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l7374,plain,
( ~ ssSkC0
| skc17 != skc16 ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l874,plain,
( ~ ssSkC0
| hollywood(skc23) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8330,plain,
( ~ ssSkC0
| furniture(skc19) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l8047,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9230,plain,
( ~ chevy(skc28)
| ~ city(skc31)
| ~ front(skc27)
| ~ front(skc26)
| ~ fellow(skc24)
| ~ fellow(skc25)
| ~ lonely(skc29)
| ~ event(skc30)
| ~ seat(skc27)
| ~ seat(skc26)
| ~ man(skc24)
| ~ man(skc25)
| ~ car(skc28)
| ~ white(skc28)
| ~ street(skc29)
| ~ dirty(skc28)
| ~ hollywood(skc31)
| ~ old(skc28)
| ~ young(skc24)
| ~ young(skc25)
| ~ furniture(skc27)
| ~ furniture(skc26)
| ~ way(skc29)
| ~ in(skc30,skc31)
| ~ in(skc24,skc27)
| ~ in(skc25,skc26)
| ~ barrel(skc30,skc28)
| ~ down(skc30,skc29)
| ssSkC0
| skc25 = skc24 ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l582,plain,
( ~ ssSkC0
| car(skc20) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l8334,plain,
( ~ ssSkC0
| young(skc17) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l5915,plain,
front(skc19),
inference(instantiation,[status(thm)],[12]) ).
cnf(l17911,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l9974,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l17917,plain,
( ssSkC0
| furniture(skc26) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l15854,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l621,plain,
( ~ ssSkC0
| fellow(skc16) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l5513,plain,
( ~ ssSkC0
| man(skc17) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l15887,plain,
( front(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l565,plain,
( ~ ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l15913,plain,
front(skc26),
inference(instantiation,[status(thm)],[5]) ).
cnf(l16498,plain,
( ssSkC0
| furniture(skc27) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l15910,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l15911,plain,
lonely(skc29),
inference(instantiation,[status(thm)],[2]) ).
cnf(l18080,plain,
( ssSkC0
| in(skc25,skc26) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l6626,plain,
( ~ ssSkC0
| white(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l18086,plain,
( ssSkC0
| in(skc24,skc27) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l17914,plain,
event(skc30),
inference(instantiation,[status(thm)],[1]) ).
cnf(l15882,plain,
( ssSkC0
| in(skc30,skc31) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l16502,plain,
( man(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l18081,plain,
( ssSkC0
| barrel(skc30,skc28) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l15909,plain,
( ssSkC0
| way(skc29) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l18082,plain,
( skc25 != skc24
| ssSkC0 ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l8674,plain,
( seat(skc26)
| ssSkC0 ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l13302,plain,
( man(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l18085,plain,
( white(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7388,plain,
lonely(skc21),
inference(instantiation,[status(thm)],[10]) ).
cnf(l8958,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l18087,plain,
( old(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l488,plain,
( car(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l18083,plain,
fellow(skc25),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1064,plain,
( hollywood(skc31)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l16501,plain,
( street(skc29)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l15888,plain,
seat(skc27),
inference(instantiation,[status(thm)],[4]) ).
cnf(l16499,plain,
young(skc24),
inference(instantiation,[status(thm)],[7]) ).
cnf(l18079,plain,
( ssSkC0
| down(skc30,skc29) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l6916,plain,
( ~ ssSkC0
| down(skc22,skc21) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l15881,plain,
chevy(skc28),
inference(instantiation,[status(thm)],[3]) ).
cnf(l18084,plain,
( young(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l15884,plain,
( dirty(skc28)
| ssSkC0 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l15914,plain,
( fellow(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l68,l26,l23,l8,l46,l69,l3,l65,l868,l7,l21,l40,l4,l33,l128,l18,l2,l84,l113,l4354,l4360,l5365,l4378,l17,l4851,l5691,l5810,l5376,l9,l5685,l151,l174,l152,l6561,l238,l241,l72,l173,l394,l10,l19,l8993,l8987,l164,l5813,l294,l6607,l359,l6555,l319,l159,l16,l329,l354,l155,l8893,l317,l239,l740,l5695,l8415,l325,l8991,l8813,l5814,l11,l787,l8816,l5369,l8890,l370,l8737,l6565,l110,l5377,l432,l5373,l5374,l14,l745,l5363,l5823,l6583,l307,l30,l6562,l5368,l754,l301,l180,l8990,l324,l5686,l6560,l6564,l302,l8999,l338,l8681,l5815,l6605,l4855,l326,l6340,l13,l205,l8998,l121,l295,l315,l6609,l92,l445,l277,l5165,l443,l9306,l5362,l6572,l242,l8988,l784,l240,l8683,l149,l660,l6191,l8593,l5375,l6908,l6193,l4646,l10037,l8815,l15,l4451,l8794,l293,l6553,l6856,l4958,l5062,l195,l9753,l10058,l5493,l20,l6906,l433,l6918,l8597,l327,l63,l4961,l8787,l762,l518,l5950,l284,l4974,l4907,l9120,l9131,l5492,l5476,l6900,l4980,l6923,l4837,l12,l308,l6904,l4987,l5063,l4685,l10667,l9068,l5863,l8520,l4962,l7087,l7052,l6492,l8869,l10059,l8862,l5577,l8682,l8764,l4968,l6969,l7065,l4979,l6298,l9134,l8169,l7037,l5156,l8892,l9169,l8859,l8980,l6852,l9129,l4852,l7106,l9130,l6905,l6928,l11090,l8530,l5812,l8785,l4854,l11097,l6554,l9755,l10055,l10078,l7100,l9128,l7103,l6859,l9127,l5764,l8171,l10036,l154,l314,l11761,l5361,l6874,l8864,l8789,l5031,l10056,l8986,l7079,l129,l157,l7092,l7515,l6296,l9135,l5252,l6294,l8995,l5520,l5776,l299,l6234,l8852,l6235,l7043,l5519,l8735,l10668,l4972,l6231,l4986,l8790,l8592,l8526,l4966,l8589,l7095,l8684,l6233,l274,l5517,l4990,l727,l728,l9126,l8992,l203,l9375,l793,l6158,l9376,l4733,l726,l6210,l11065,l5022,l6216,l7067,l5521,l6229,l6427,l9119,l15492,l9167,l796,l7113,l6815,l7038,l7243,l7128,l4988,l6909,l4932,l7112,l11757,l9829,l5032,l4984,l8391,l4938,l6795,l756,l770,l6566,l4971,l9125,l9828,l8994,l5845,l8545,l9154,l771,l9774,l7125,l6589,l12038,l8866,l8868,l6922,l9006,l6274,l6877,l4947,l10065,l769,l11756,l7096,l777,l9124,l5150,l4454,l6725,l9274,l805,l6880,l9975,l8782,l6581,l6213,l4942,l7093,l9754,l4946,l283,l11759,l9271,l4327,l7098,l729,l7126,l9121,l8863,l4940,l285,l8313,l228,l9136,l6960,l4939,l757,l12163,l9182,l9208,l8989,l4770,l8170,l9270,l9832,l10215,l5027,l7042,l7088,l4763,l7242,l6913,l7111,l7914,l10663,l10046,l6021,l789,l4872,l7047,l935,l175,l6030,l381,l331,l4965,l7104,l7122,l6551,l9123,l5416,l4760,l6548,l5903,l4328,l597,l4653,l5905,l6026,l6212,l8731,l6297,l4652,l767,l4931,l575,l5600,l9069,l8867,l601,l9775,l9580,l1221,l10032,l5906,l8985,l229,l10052,l6584,l9853,l4978,l6295,l477,l6705,l484,l10629,l569,l7247,l66,l577,l5901,l9811,l588,l606,l482,l290,l894,l681,l4764,l505,l6293,l4735,l231,l9776,l298,l4953,l5020,l103,l568,l801,l487,l6816,l596,l598,l600,l7129,l566,l7114,l447,l590,l923,l7424,l137,l4338,l617,l585,l884,l9132,l184,l8521,l282,l7425,l5844,l287,l567,l614,l7439,l9374,l230,l11101,l620,l5212,l6893,l605,l5904,l8983,l8801,l516,l363,l811,l4951,l6545,l581,l501,l9831,l572,l563,l6199,l619,l7438,l573,l9187,l5203,l8516,l1057,l4765,l8793,l4875,l8677,l561,l8708,l5349,l7089,l5019,l604,l9138,l347,l618,l4759,l5351,l318,l6180,l5919,l9168,l493,l602,l584,l7432,l7115,l6552,l1073,l9118,l7086,l7130,l8511,l1125,l9133,l634,l469,l309,l893,l232,l8499,l616,l4325,l570,l9191,l9377,l12892,l5206,l4981,l9117,l564,l4943,l6029,l5907,l622,l320,l5378,l6808,l578,l8498,l6336,l296,l4689,l6457,l970,l8333,l4706,l8961,l4985,l6232,l6200,l11862,l356,l615,l5912,l8325,l7090,l8798,l1071,l9115,l5902,l8331,l8957,l730,l773,l629,l9200,l7373,l9176,l6259,l4768,l10726,l1058,l1068,l5910,l343,l8336,l5914,l571,l8332,l580,l7377,l10665,l4708,l313,l763,l8515,l5913,l4709,l758,l304,l5518,l6590,l6132,l7375,l4707,l7374,l874,l8330,l8047,l9230,l582,l8334,l5915,l17911,l9974,l17917,l15854,l621,l5513,l15887,l565,l15913,l16498,l15910,l15911,l18080,l6626,l18086,l17914,l15882,l16502,l18081,l15909,l18082,l8674,l13302,l18085,l7388,l8958,l18087,l488,l18083,l1064,l16501,l15888,l16499,l18079,l6916,l15881,l18084,l15884,l15914]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP011-1 : TPTP v9.0.0. Released v2.4.0.
% 0.07/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n022.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:54:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 8
% 0.18/0.46 % launching worker at depth: 9
% 2.40/0.68 % launching worker at depth: 10
% 14.00/2.16 % launching worker at depth: 11
% 277.53/35.42 % SZS status Theorem for theBenchmark
% 277.53/35.42 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------