%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NLP009-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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 11:59:21 AM UTC 2025
% Result : Unsatisfiable 194.98s 24.94s
% Output : CNFRefutation 194.98s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named clause1)
% Comments :
%------------------------------------------------------------------------------
cnf(0,plain,
hollywood(skc27),
inference(cnf,[status(esa)],[clause1]) ).
cnf(l0,plain,
hollywood(skc27),
inference(instantiation,[status(thm)],[0]) ).
cnf(52,plain,
( ~ old(X0)
| ~ hollywood(X1)
| ~ young(X2)
| ~ young(X3)
| ~ fellow(X2)
| ~ fellow(X3)
| ~ street(X4)
| ~ event(X5)
| ~ seat(X6)
| ~ city(X1)
| ~ white(X0)
| ~ man(X2)
| ~ man(X3)
| ~ lonely(X4)
| ~ way(X4)
| ~ chevy(X0)
| ~ car(X0)
| ~ dirty(X0)
| ~ front(X6)
| ~ furniture(X6)
| ~ in(X5,X1)
| ~ in(X2,X6)
| ~ in(X3,X6)
| ~ down(X5,X4)
| ~ barrel(X5,X0)
| ssSkC0
| X3 = X2 ),
inference(cnf,[status(esa)],[clause53]) ).
cnf(l1,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc16)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc26,skc27)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(19,plain,
( way(skc25)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause20]) ).
cnf(l87,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(12,plain,
young(skc15),
inference(cnf,[status(esa)],[clause13]) ).
cnf(l129,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(13,plain,
fellow(skc14),
inference(cnf,[status(esa)],[clause14]) ).
cnf(l6,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(20,plain,
( city(skc27)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause21]) ).
cnf(l7,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(18,plain,
( lonely(skc25)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause19]) ).
cnf(l8,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(37,plain,
( ~ ssSkC0
| man(skc15) ),
inference(cnf,[status(esa)],[clause38]) ).
cnf(l62,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(17,plain,
( ssSkC0
| dirty(skc24) ),
inference(cnf,[status(esa)],[clause18]) ).
cnf(l49,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(34,plain,
( ~ ssSkC0
| young(skc14) ),
inference(cnf,[status(esa)],[clause35]) ).
cnf(l3138,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(2,plain,
street(skc25),
inference(cnf,[status(esa)],[clause3]) ).
cnf(l13,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(41,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(cnf,[status(esa)],[clause42]) ).
cnf(l19,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(28,plain,
( ~ ssSkC0
| way(skc17) ),
inference(cnf,[status(esa)],[clause29]) ).
cnf(l33,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(1,plain,
event(skc26),
inference(cnf,[status(esa)],[clause2]) ).
cnf(l16,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(38,plain,
( ~ ssSkC0
| front(skc16) ),
inference(cnf,[status(esa)],[clause39]) ).
cnf(l147,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l4,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(15,plain,
( car(skc24)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause16]) ).
cnf(l17,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(40,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(cnf,[status(esa)],[clause41]) ).
cnf(l11,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(36,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(cnf,[status(esa)],[clause37]) ).
cnf(l36,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(53,plain,
( ~ old(X0)
| ~ hollywood(X1)
| ~ young(X2)
| ~ young(X3)
| ~ fellow(X2)
| ~ fellow(X3)
| ~ street(X4)
| ~ event(X5)
| ~ seat(X6)
| ~ city(X1)
| ~ white(X0)
| ~ man(X2)
| ~ man(X3)
| ~ lonely(X4)
| ~ way(X4)
| ~ chevy(X0)
| ~ car(X0)
| ~ ssSkC0
| ~ dirty(X0)
| ~ front(X6)
| ~ furniture(X6)
| ~ in(X5,X1)
| ~ in(X2,X6)
| ~ in(X3,X6)
| ~ down(X5,X4)
| ~ barrel(X5,X0)
| X3 = X2 ),
inference(cnf,[status(esa)],[clause54]) ).
cnf(l3571,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc15)
| ~ young(skc14)
| ~ fellow(skc15)
| ~ fellow(skc14)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc15)
| ~ man(skc14)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc15,skc16)
| ~ in(skc14,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc14 = skc15 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(48,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(cnf,[status(esa)],[clause49]) ).
cnf(l10731,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(10,plain,
lonely(skc17),
inference(cnf,[status(esa)],[clause11]) ).
cnf(l10750,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(3,plain,
old(skc24),
inference(cnf,[status(esa)],[clause4]) ).
cnf(l2,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(46,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(cnf,[status(esa)],[clause47]) ).
cnf(l4021,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(45,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(cnf,[status(esa)],[clause46]) ).
cnf(l10729,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(30,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(cnf,[status(esa)],[clause31]) ).
cnf(l10732,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(16,plain,
( white(skc24)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause17]) ).
cnf(l14,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(14,plain,
( chevy(skc24)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause15]) ).
cnf(l12,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l23,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(31,plain,
( ~ ssSkC0
| white(skc18) ),
inference(cnf,[status(esa)],[clause32]) ).
cnf(l10743,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l11507,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l285,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(8,plain,
event(skc19),
inference(cnf,[status(esa)],[clause9]) ).
cnf(l4025,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(29,plain,
( ~ ssSkC0
| old(skc18) ),
inference(cnf,[status(esa)],[clause30]) ).
cnf(l86,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(49,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(cnf,[status(esa)],[clause50]) ).
cnf(l10727,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l52,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(33,plain,
( ~ ssSkC0
| city(skc20) ),
inference(cnf,[status(esa)],[clause34]) ).
cnf(l10741,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(35,plain,
( ~ ssSkC0
| man(skc14) ),
inference(cnf,[status(esa)],[clause36]) ).
cnf(l122,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l11506,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(21,plain,
( young(skc21)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause22]) ).
cnf(l3195,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(42,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(cnf,[status(esa)],[clause43]) ).
cnf(l26,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(22,plain,
( man(skc21)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause23]) ).
cnf(l149,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l716,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(32,plain,
( ~ ssSkC0
| car(skc18) ),
inference(cnf,[status(esa)],[clause33]) ).
cnf(l10735,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4091,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1085,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1392,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l21,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l3419,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l44,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4086,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(24,plain,
( man(skc22)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause25]) ).
cnf(l1471,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1515,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l5086,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4087,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l530,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l6941,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l206,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l2563,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3444,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l426,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(39,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(cnf,[status(esa)],[clause40]) ).
cnf(l4024,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l144,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(25,plain,
( ssSkC0
| front(skc23) ),
inference(cnf,[status(esa)],[clause26]) ).
cnf(l4144,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(23,plain,
( fellow(skc22)
| ssSkC0 ),
inference(cnf,[status(esa)],[clause24]) ).
cnf(l6950,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(5,plain,
young(skc22),
inference(cnf,[status(esa)],[clause6]) ).
cnf(l1521,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3714,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1472,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l3064,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc15)
| ~ young(skc14)
| ~ fellow(skc15)
| ~ fellow(skc14)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc15)
| ~ man(skc14)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc15,skc16)
| ~ in(skc14,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc14 = skc15 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l4991,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l118,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1478,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(27,plain,
( ~ ssSkC0
| street(skc17) ),
inference(cnf,[status(esa)],[clause28]) ).
cnf(l4005,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l4339,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3921,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3828,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l5118,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(4,plain,
seat(skc23),
inference(cnf,[status(esa)],[clause5]) ).
cnf(l3955,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6933,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(51,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(cnf,[status(esa)],[clause52]) ).
cnf(l18,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(47,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(cnf,[status(esa)],[clause48]) ).
cnf(l10725,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(7,plain,
hollywood(skc20),
inference(cnf,[status(esa)],[clause8]) ).
cnf(l3703,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6936,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(50,plain,
( skc22 != skc21
| ssSkC0 ),
inference(cnf,[status(esa)],[clause51]) ).
cnf(l8719,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l6939,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l6706,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l5101,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3522,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l6297,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5116,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l9,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(44,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(cnf,[status(esa)],[clause45]) ).
cnf(l3676,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l5531,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l5743,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3086,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4134,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l8371,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l11504,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l6942,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1497,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l5408,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(43,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(cnf,[status(esa)],[clause44]) ).
cnf(l8390,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l1393,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l11510,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1474,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l3829,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l5567,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l10687,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l5741,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l12358,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l6955,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4136,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l6948,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(11,plain,
seat(skc16),
inference(cnf,[status(esa)],[clause12]) ).
cnf(l3,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l4138,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5020,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3065,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5739,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l10693,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l7093,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l3820,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l8417,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7012,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l4135,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(26,plain,
( ssSkC0
| furniture(skc23) ),
inference(cnf,[status(esa)],[clause27]) ).
cnf(l3788,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l5745,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l10683,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(9,plain,
chevy(skc18),
inference(cnf,[status(esa)],[clause10]) ).
cnf(l4143,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4093,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l6864,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3621,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l10688,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3932,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l3787,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4338,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l4140,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l4992,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l10682,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5744,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3096,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3810,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l8697,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l3760,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l8720,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1514,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3920,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3159,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3679,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l5740,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(6,plain,
fellow(skc21),
inference(cnf,[status(esa)],[clause7]) ).
cnf(l5066,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l8416,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l7092,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1479,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l7546,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l4139,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3821,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l6871,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l3107,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l3747,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l3817,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l7685,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l7013,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l3257,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l3785,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l4059,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3816,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3097,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l4141,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5114,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l6964,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l9143,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1495,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l3950,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4132,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l5234,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1517,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l4193,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3939,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l10724,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3929,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3751,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l1389,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l6952,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l7683,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l7547,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l6988,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l10690,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l10681,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3237,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l4235,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3531,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l9147,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l3331,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l3238,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l6094,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l3784,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l6257,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1476,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l6696,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l4068,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l10680,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l10689,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l6793,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l10730,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3746,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3792,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l6951,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l1486,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1520,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l6998,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l4121,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l6902,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8448,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l4131,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l5566,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l5131,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4423,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7125,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l3254,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7146,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l3622,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1470,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l3758,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3954,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4400,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3750,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l3841,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l5775,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l3765,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1523,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3809,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l4189,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l6258,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l3581,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l46,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l6095,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4701,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l10684,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l3334,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3947,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3674,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l5100,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l6692,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3941,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l5129,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l4370,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3214,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l4006,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l3716,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3333,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l4748,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l191,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l1400,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4712,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l5410,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4029,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4162,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l6938,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l3946,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4133,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l4589,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l4252,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l7684,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4692,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3255,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l5121,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l9036,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l371,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l193,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc15)
| ~ young(skc14)
| ~ fellow(skc15)
| ~ fellow(skc14)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc15)
| ~ man(skc14)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc15,skc16)
| ~ in(skc14,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc14 = skc15 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3098,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4710,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l6697,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3671,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4792,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l374,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l3672,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l3360,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l330,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3155,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l10747,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l3344,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l4260,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l4719,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l350,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1468,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l10691,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3779,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l5771,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3774,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l7548,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4747,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l8725,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l5232,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l8150,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l10686,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l3345,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l4591,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l7549,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l4699,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1475,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l7015,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3749,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l7011,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l4896,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l551,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3104,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4058,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l336,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4689,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l4693,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l4752,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3748,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3348,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3625,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3587,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l6737,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l6996,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l3110,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3209,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l8722,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l343,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l3149,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l3426,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l335,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l3811,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l3584,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l344,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l4142,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l3154,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l3128,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l3646,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3129,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l4137,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l203,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3948,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l3100,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l10685,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l339,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l535,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l4161,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l8152,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l3190,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l4261,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3132,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l3228,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4259,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l349,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l3355,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l346,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l4160,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l3699,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3739,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l3701,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l3280,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3342,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l3624,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l3719,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3303,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l3162,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l3134,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l4598,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l3423,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l3698,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l4393,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l4691,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l372,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l4389,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4149,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3133,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l3655,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l3513,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l3156,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l3188,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4698,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l4315,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l9071,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3240,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l4285,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l9065,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3794,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l3332,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l4150,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l7592,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3726,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l4080,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l3402,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3182,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l3300,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l4323,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l7686,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l4083,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l4023,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l3169,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3298,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4344,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8190,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4250,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l4092,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l4596,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l4089,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l4017,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l348,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4736,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3727,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l4391,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3883,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3875,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l4390,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l4394,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l4396,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l4251,plain,
( ~ ssSkC0
| way(skc17) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l4313,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l3705,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l3656,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l3220,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4082,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l7787,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l3740,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3712,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3925,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l4300,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3700,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4774,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3235,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l4305,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l4307,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3177,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l3729,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l4956,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l4108,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l7681,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4711,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l6694,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l4304,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3115,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3304,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l4151,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3309,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l4232,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2573,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l3314,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3130,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3724,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l334,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l3109,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l4324,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l3710,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l5379,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l22,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3168,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l6935,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l4314,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l4581,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l3730,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l3721,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l6937,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3717,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l154,plain,
( ~ old(skc18)
| ~ hollywood(skc20)
| ~ young(skc14)
| ~ young(skc15)
| ~ fellow(skc14)
| ~ fellow(skc15)
| ~ street(skc17)
| ~ event(skc19)
| ~ seat(skc16)
| ~ city(skc20)
| ~ white(skc18)
| ~ man(skc14)
| ~ man(skc15)
| ~ lonely(skc17)
| ~ way(skc17)
| ~ chevy(skc18)
| ~ car(skc18)
| ~ ssSkC0
| ~ dirty(skc18)
| ~ front(skc16)
| ~ furniture(skc16)
| ~ in(skc19,skc20)
| ~ in(skc14,skc16)
| ~ in(skc15,skc16)
| ~ down(skc19,skc17)
| ~ barrel(skc19,skc18)
| skc15 = skc14 ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l4079,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l4316,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l8277,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l12574,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3460,plain,
( ~ ssSkC0
| old(skc18) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l4395,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8502,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l668,plain,
( ~ ssSkC0
| city(skc20) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3961,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l3761,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l4595,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l178,plain,
( ~ ssSkC0
| in(skc14,skc16) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l3771,plain,
( ~ ssSkC0
| dirty(skc18) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3964,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l5105,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3239,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l3425,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l4942,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3697,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l3773,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l8528,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3126,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l3968,plain,
( ~ ssSkC0
| car(skc18) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l5529,plain,
( ~ ssSkC0
| down(skc19,skc17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l3299,plain,
( ~ ssSkC0
| fellow(skc15) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l3382,plain,
( ~ old(skc24)
| ~ hollywood(skc27)
| ~ young(skc21)
| ~ young(skc22)
| ~ fellow(skc21)
| ~ fellow(skc22)
| ~ street(skc25)
| ~ event(skc26)
| ~ seat(skc23)
| ~ city(skc27)
| ~ white(skc24)
| ~ man(skc21)
| ~ man(skc22)
| ~ lonely(skc25)
| ~ way(skc25)
| ~ chevy(skc24)
| ~ car(skc24)
| ~ dirty(skc24)
| ~ front(skc23)
| ~ furniture(skc23)
| ~ in(skc26,skc27)
| ~ in(skc21,skc23)
| ~ in(skc22,skc23)
| ~ down(skc26,skc25)
| ~ barrel(skc26,skc24)
| ssSkC0
| skc22 = skc21 ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l5141,plain,
( way(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8543,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l3559,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3568,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l11035,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3131,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l8541,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l8384,plain,
( lonely(skc25)
| ssSkC0 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l4840,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l8535,plain,
( ssSkC0
| barrel(skc26,skc24) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l5235,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3562,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8532,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l6281,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l8534,plain,
seat(skc23),
inference(instantiation,[status(thm)],[4]) ).
cnf(l4187,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l7302,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l5527,plain,
( ~ ssSkC0
| front(skc16) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l5216,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l5143,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l11091,plain,
( ssSkC0
| in(skc22,skc23) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l5134,plain,
event(skc26),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4010,plain,
young(skc15),
inference(instantiation,[status(thm)],[12]) ).
cnf(l3383,plain,
old(skc24),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4155,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l8522,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l4233,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l3192,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3565,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l11085,plain,
fellow(skc21),
inference(instantiation,[status(thm)],[6]) ).
cnf(l3561,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l3759,plain,
( ~ ssSkC0
| in(skc15,skc16) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l11144,plain,
( chevy(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l8531,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l5219,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l176,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l4004,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l3556,plain,
( man(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l5220,plain,
( city(skc27)
| ssSkC0 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l6923,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l8537,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l8524,plain,
( white(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l3965,plain,
( ~ ssSkC0
| in(skc19,skc20) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l179,plain,
seat(skc16),
inference(instantiation,[status(thm)],[11]) ).
cnf(l6273,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l8533,plain,
( ssSkC0
| in(skc26,skc27) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l4011,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3963,plain,
( ~ ssSkC0
| furniture(skc16) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l8526,plain,
( fellow(skc22)
| ssSkC0 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l8525,plain,
( man(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l4012,plain,
( ~ ssSkC0
| white(skc18) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l536,plain,
( ~ ssSkC0
| street(skc17) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l3866,plain,
( ~ ssSkC0
| young(skc14) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l7318,plain,
( ssSkC0
| dirty(skc24) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3135,plain,
chevy(skc18),
inference(instantiation,[status(thm)],[9]) ).
cnf(l8542,plain,
( ssSkC0
| down(skc26,skc25) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l5370,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l342,plain,
fellow(skc14),
inference(instantiation,[status(thm)],[13]) ).
cnf(l3558,plain,
( young(skc21)
| ssSkC0 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l5218,plain,
street(skc25),
inference(instantiation,[status(thm)],[2]) ).
cnf(l5916,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l6286,plain,
( car(skc24)
| ssSkC0 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l8539,plain,
( ssSkC0
| furniture(skc23) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l4013,plain,
( ~ ssSkC0
| barrel(skc19,skc18) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l173,plain,
( ~ ssSkC0
| man(skc14) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l11033,plain,
( ssSkC0
| in(skc21,skc23) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l3969,plain,
( ~ ssSkC0
| man(skc15) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l8540,plain,
young(skc22),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3962,plain,
lonely(skc17),
inference(instantiation,[status(thm)],[10]) ).
cnf(l3967,plain,
hollywood(skc20),
inference(instantiation,[status(thm)],[7]) ).
cnf(l13761,plain,
( skc22 != skc21
| ssSkC0 ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l5135,plain,
( ssSkC0
| front(skc23) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3970,plain,
event(skc19),
inference(instantiation,[status(thm)],[8]) ).
cnf(l11772,plain,
( ~ ssSkC0
| skc15 != skc14 ),
inference(instantiation,[status(thm)],[51]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l87,l129,l6,l7,l8,l62,l49,l3138,l13,l19,l33,l16,l147,l4,l17,l11,l36,l3571,l10731,l10750,l2,l4021,l10729,l10732,l14,l12,l23,l10743,l11507,l285,l4025,l86,l10727,l52,l10741,l122,l11506,l3195,l26,l149,l716,l10735,l4091,l1085,l1392,l21,l3419,l44,l4086,l1471,l1515,l5086,l4087,l530,l6941,l206,l2563,l3444,l426,l4024,l144,l4144,l6950,l1521,l3714,l1472,l3064,l4991,l118,l1478,l4005,l4339,l3921,l3828,l5118,l3955,l6933,l18,l10725,l3703,l6936,l8719,l6939,l6706,l5101,l3522,l6297,l5116,l9,l3676,l5531,l5743,l3086,l4134,l8371,l11504,l6942,l1497,l5408,l8390,l1393,l11510,l1474,l3829,l5567,l10687,l5741,l12358,l6955,l4136,l6948,l3,l4138,l5020,l3065,l5739,l10693,l7093,l3820,l8417,l7012,l4135,l3788,l5745,l10683,l4143,l4093,l6864,l3621,l10688,l3932,l3787,l4338,l4140,l4992,l10682,l5744,l3096,l3810,l8697,l3760,l8720,l1514,l3920,l3159,l3679,l5740,l5066,l8416,l7092,l1479,l7546,l4139,l3821,l6871,l3107,l3747,l3817,l7685,l7013,l3257,l3785,l4059,l3816,l3097,l4141,l5114,l6964,l9143,l1495,l3950,l4132,l5234,l1517,l4193,l3939,l10724,l3929,l3751,l1389,l6952,l7683,l7547,l6988,l10690,l10681,l3237,l4235,l3531,l9147,l3331,l3238,l6094,l3784,l6257,l1476,l6696,l4068,l10680,l10689,l6793,l10730,l3746,l3792,l6951,l1486,l1520,l6998,l4121,l6902,l8448,l4131,l5566,l5131,l4423,l7125,l3254,l7146,l3622,l1470,l3758,l3954,l4400,l3750,l3841,l5775,l3765,l1523,l3809,l4189,l6258,l3581,l46,l6095,l4701,l10684,l3334,l3947,l3674,l5100,l6692,l3941,l5129,l4370,l3214,l4006,l3716,l3333,l4748,l191,l1400,l4712,l5410,l4029,l4162,l6938,l3946,l4133,l4589,l4252,l7684,l4692,l3255,l5121,l9036,l371,l193,l3098,l4710,l6697,l3671,l4792,l374,l3672,l3360,l330,l3155,l10747,l3344,l4260,l4719,l350,l1468,l10691,l3779,l5771,l3774,l7548,l4747,l8725,l5232,l8150,l10686,l3345,l4591,l7549,l4699,l1475,l7015,l3749,l7011,l4896,l551,l3104,l4058,l336,l4689,l4693,l4752,l3748,l3348,l3625,l3587,l6737,l6996,l3110,l3209,l8722,l343,l3149,l3426,l335,l3811,l3584,l344,l4142,l3154,l3128,l3646,l3129,l4137,l203,l3948,l3100,l10685,l339,l535,l4161,l8152,l3190,l4261,l3132,l3228,l4259,l349,l3355,l346,l4160,l3699,l3739,l3701,l3280,l3342,l3624,l3719,l3303,l3162,l3134,l4598,l3423,l3698,l4393,l4691,l372,l4389,l4149,l3133,l3655,l3513,l3156,l3188,l4698,l4315,l9071,l3240,l4285,l9065,l3794,l3332,l4150,l7592,l3726,l4080,l3402,l3182,l3300,l4323,l7686,l4083,l4023,l3169,l3298,l4344,l8190,l4250,l4092,l4596,l4089,l4017,l348,l4736,l3727,l4391,l3883,l3875,l4390,l4394,l4396,l4251,l4313,l3705,l3656,l3220,l4082,l7787,l3740,l3712,l3925,l4300,l3700,l4774,l3235,l4305,l4307,l3177,l3729,l4956,l4108,l7681,l4711,l6694,l4304,l3115,l3304,l4151,l3309,l4232,l2573,l3314,l3130,l3724,l334,l3109,l4324,l3710,l5379,l22,l3168,l6935,l4314,l4581,l3730,l3721,l6937,l3717,l154,l4079,l4316,l8277,l12574,l3460,l4395,l8502,l668,l3961,l3761,l4595,l178,l3771,l3964,l5105,l3239,l3425,l4942,l3697,l3773,l8528,l3126,l3968,l5529,l3299,l3382,l5141,l8543,l3559,l3568,l11035,l3131,l8541,l8384,l4840,l8535,l5235,l3562,l8532,l6281,l8534,l4187,l7302,l5527,l5216,l5143,l11091,l5134,l4010,l3383,l4155,l8522,l4233,l3192,l3565,l11085,l3561,l3759,l11144,l8531,l5219,l176,l4004,l3556,l5220,l6923,l8537,l8524,l3965,l179,l6273,l8533,l4011,l3963,l8526,l8525,l4012,l536,l3866,l7318,l3135,l8542,l5370,l342,l3558,l5218,l5916,l6286,l8539,l4013,l173,l11033,l3969,l8540,l3962,l3967,l13761,l5135,l3970,l11772]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP009-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 : n017.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:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 6
% 0.19/0.42 % launching worker at depth: 9
% 1.68/0.61 % launching worker at depth: 10
% 12.35/1.94 % launching worker at depth: 11
% 194.98/24.94 % SZS status Theorem for theBenchmark
% 194.98/24.94 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------