%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP013-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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 : Thu May 9 17:33:34 EDT 2024
% Result : Satisfiable 54.03s 54.23s
% Output : Saturation 54.03s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause56,negated_conjecture,
( ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ old(X7)
| ~ dirty(X7)
| ~ white(X7)
| ~ car(X7)
| ~ chevy(X7)
| ~ event(X11)
| ~ barrel(X11,X7)
| ~ down(X11,X6)
| ~ in(X11,X12)
| ~ city(X12)
| ~ hollywood(X12)
| ~ young(X10)
| ~ man(X10)
| ~ fellow(X10)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X10,X8)
| ~ in(X9,X8)
| ~ front(X8)
| ~ furniture(X8)
| ~ seat(X8)
| ~ ssSkC0
| X9 = X10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
cnf(clause53,negated_conjecture,
( ~ ssSkC0
| in(skc16,skc17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
cnf(clause54,negated_conjecture,
( skc24 != skc23
| ssSkC0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
cnf(clause18,negated_conjecture,
( ssSkC0
| old(skc27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( ssSkC0
| dirty(skc27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(clause20,negated_conjecture,
( ssSkC0
| white(skc27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(clause21,negated_conjecture,
( ssSkC0
| car(skc27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(clause3,negated_conjecture,
chevy(skc27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(clause16,negated_conjecture,
( ssSkC0
| street(skc26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(clause17,negated_conjecture,
( ssSkC0
| way(skc26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(clause4,negated_conjecture,
lonely(skc26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(clause2,negated_conjecture,
event(skc28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause1,negated_conjecture,
hollywood(skc29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause22,negated_conjecture,
( ssSkC0
| city(skc29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(clause7,negated_conjecture,
fellow(skc23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause24,negated_conjecture,
( ssSkC0
| man(skc23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(clause23,negated_conjecture,
( ssSkC0
| young(skc23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(clause27,negated_conjecture,
( ssSkC0
| front(skc25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(clause28,negated_conjecture,
( ssSkC0
| furniture(skc25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(clause5,negated_conjecture,
seat(skc25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
young(skc24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(clause26,negated_conjecture,
( ssSkC0
| man(skc24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(clause25,negated_conjecture,
( ssSkC0
| fellow(skc24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(clause45,negated_conjecture,
( ssSkC0
| down(skc28,skc26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(clause44,negated_conjecture,
( ssSkC0
| barrel(skc28,skc27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(clause46,negated_conjecture,
( ssSkC0
| in(skc28,skc29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
cnf(clause47,negated_conjecture,
( ssSkC0
| in(skc23,skc25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(clause48,negated_conjecture,
( ssSkC0
| in(skc24,skc25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(clause57,negated_conjecture,
( ~ old(X13)
| ~ dirty(X13)
| ~ white(X13)
| ~ car(X13)
| ~ chevy(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ down(X19,X14)
| ~ barrel(X19,X13)
| ~ event(X19)
| ~ hollywood(X20)
| ~ city(X20)
| ~ in(X19,X20)
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ in(X18,X17)
| ~ front(X17)
| ~ furniture(X17)
| ~ seat(X17)
| ~ young(X15)
| ~ man(X15)
| ~ fellow(X15)
| ~ seat(X16)
| ~ furniture(X16)
| ~ front(X16)
| ~ in(X15,X16)
| ssSkC0
| X15 = X18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
cnf(c388,plain,
( ~ old(X169)
| ~ dirty(X169)
| ~ white(X169)
| ~ car(X169)
| ~ chevy(X169)
| ~ street(X166)
| ~ way(X166)
| ~ lonely(X166)
| ~ down(X168,X166)
| ~ barrel(X168,X169)
| ~ event(X168)
| ~ hollywood(X167)
| ~ city(X167)
| ~ in(X168,X167)
| ~ fellow(X165)
| ~ man(X165)
| ~ young(X165)
| ~ in(X165,X164)
| ~ front(X164)
| ~ furniture(X164)
| ~ seat(X164)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ssSkC0
| skc24 = X165 ),
inference(resolution,[status(thm)],[clause57,clause48]) ).
cnf(c1149,plain,
( ~ old(X9035)
| ~ dirty(X9035)
| ~ white(X9035)
| ~ car(X9035)
| ~ chevy(X9035)
| ~ street(X9036)
| ~ way(X9036)
| ~ lonely(X9036)
| ~ down(X9037,X9036)
| ~ barrel(X9037,X9035)
| ~ event(X9037)
| ~ hollywood(X9034)
| ~ city(X9034)
| ~ in(X9037,X9034)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c388,clause47]) ).
cnf(c10081,plain,
( ~ old(X11352)
| ~ dirty(X11352)
| ~ white(X11352)
| ~ car(X11352)
| ~ chevy(X11352)
| ~ street(X11353)
| ~ way(X11353)
| ~ lonely(X11353)
| ~ down(skc28,X11353)
| ~ barrel(skc28,X11352)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c1149,clause46]) ).
cnf(c13884,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(X11366)
| ~ way(X11366)
| ~ lonely(X11366)
| ~ down(skc28,X11366)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c10081,clause44]) ).
cnf(c13933,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c13884,clause45]) ).
cnf(c13940,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ~ young(skc24)
| ~ man(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c13933,clause25]) ).
cnf(c13973,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ~ young(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c13940,clause26]) ).
cnf(c13978,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c13973,clause6]) ).
cnf(c13979,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c13978,clause5]) ).
cnf(c13990,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c13979,clause28]) ).
cnf(c14015,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c13990,clause27]) ).
cnf(c14030,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14015,clause23]) ).
cnf(c14051,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14030,clause24]) ).
cnf(c14064,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14051,clause7]) ).
cnf(c14080,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14064,clause22]) ).
cnf(c14086,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ~ event(skc28)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14080,clause1]) ).
cnf(c14087,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14086,clause2]) ).
cnf(c14088,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14087,clause4]) ).
cnf(c14101,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14088,clause17]) ).
cnf(c14110,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14101,clause16]) ).
cnf(c14131,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14110,clause3]) ).
cnf(c14133,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14131,clause21]) ).
cnf(c14173,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14133,clause20]) ).
cnf(c14177,plain,
( ~ old(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14173,clause19]) ).
cnf(c14203,plain,
( ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c14177,clause18]) ).
cnf(c14245,plain,
ssSkC0,
inference(resolution,[status(thm)],[c14203,clause54]) ).
cnf(c14290,plain,
in(skc16,skc17),
inference(resolution,[status(thm)],[c14245,clause53]) ).
cnf(c14388,plain,
( ~ street(X12185)
| ~ way(X12185)
| ~ lonely(X12185)
| ~ old(X12184)
| ~ dirty(X12184)
| ~ white(X12184)
| ~ car(X12184)
| ~ chevy(X12184)
| ~ event(X12181)
| ~ barrel(X12181,X12184)
| ~ down(X12181,X12185)
| ~ in(X12181,X12182)
| ~ city(X12182)
| ~ hollywood(X12182)
| ~ young(X12183)
| ~ man(X12183)
| ~ fellow(X12183)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ in(X12183,skc17)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X12183 ),
inference(resolution,[status(thm)],[c14290,clause56]) ).
cnf(c14450,plain,
( ~ street(X12192)
| ~ way(X12192)
| ~ lonely(X12192)
| ~ old(X12190)
| ~ dirty(X12190)
| ~ white(X12190)
| ~ car(X12190)
| ~ chevy(X12190)
| ~ event(X12191)
| ~ barrel(X12191,X12190)
| ~ down(X12191,X12192)
| ~ in(X12191,skc17)
| ~ city(skc17)
| ~ hollywood(skc17)
| ~ young(X12191)
| ~ man(X12191)
| ~ fellow(X12191)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X12191 ),
inference(factor,[status(thm)],[c14388]) ).
cnf(clause52,negated_conjecture,
( ~ ssSkC0
| in(skc15,skc18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
cnf(c14289,plain,
in(skc15,skc18),
inference(resolution,[status(thm)],[c14245,clause52]) ).
cnf(c14347,plain,
( ~ street(X12168)
| ~ way(X12168)
| ~ lonely(X12168)
| ~ old(X12167)
| ~ dirty(X12167)
| ~ white(X12167)
| ~ car(X12167)
| ~ chevy(X12167)
| ~ event(X12164)
| ~ barrel(X12164,X12167)
| ~ down(X12164,X12168)
| ~ in(X12164,X12165)
| ~ city(X12165)
| ~ hollywood(X12165)
| ~ young(X12166)
| ~ man(X12166)
| ~ fellow(X12166)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ in(X12166,skc18)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X12166 ),
inference(resolution,[status(thm)],[c14289,clause56]) ).
cnf(c14447,plain,
( ~ street(X12175)
| ~ way(X12175)
| ~ lonely(X12175)
| ~ old(X12173)
| ~ dirty(X12173)
| ~ white(X12173)
| ~ car(X12173)
| ~ chevy(X12173)
| ~ event(X12174)
| ~ barrel(X12174,X12173)
| ~ down(X12174,X12175)
| ~ in(X12174,skc18)
| ~ city(skc18)
| ~ hollywood(skc18)
| ~ young(X12174)
| ~ man(X12174)
| ~ fellow(X12174)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X12174 ),
inference(factor,[status(thm)],[c14347]) ).
cnf(clause51,negated_conjecture,
( ~ ssSkC0
| in(skc21,skc22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
cnf(c14287,plain,
in(skc21,skc22),
inference(resolution,[status(thm)],[c14245,clause51]) ).
cnf(c14312,plain,
( ~ street(X12149)
| ~ way(X12149)
| ~ lonely(X12149)
| ~ old(X12148)
| ~ dirty(X12148)
| ~ white(X12148)
| ~ car(X12148)
| ~ chevy(X12148)
| ~ event(X12145)
| ~ barrel(X12145,X12148)
| ~ down(X12145,X12149)
| ~ in(X12145,X12146)
| ~ city(X12146)
| ~ hollywood(X12146)
| ~ young(X12147)
| ~ man(X12147)
| ~ fellow(X12147)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ in(X12147,skc22)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X12147 ),
inference(resolution,[status(thm)],[c14287,clause56]) ).
cnf(c14443,plain,
( ~ street(X12155)
| ~ way(X12155)
| ~ lonely(X12155)
| ~ old(X12154)
| ~ dirty(X12154)
| ~ white(X12154)
| ~ car(X12154)
| ~ chevy(X12154)
| ~ event(X12156)
| ~ barrel(X12156,X12154)
| ~ down(X12156,X12155)
| ~ in(X12156,skc22)
| ~ city(skc22)
| ~ hollywood(skc22)
| ~ young(X12156)
| ~ man(X12156)
| ~ fellow(X12156)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X12156 ),
inference(factor,[status(thm)],[c14312]) ).
cnf(c381,plain,
( ~ street(X95)
| ~ way(X95)
| ~ lonely(X95)
| ~ old(X94)
| ~ dirty(X94)
| ~ white(X94)
| ~ car(X94)
| ~ chevy(X94)
| ~ event(X96)
| ~ barrel(X96,X94)
| ~ down(X96,X95)
| ~ in(X96,X92)
| ~ city(X92)
| ~ hollywood(X92)
| ~ young(X93)
| ~ man(X93)
| ~ fellow(X93)
| ~ fellow(X96)
| ~ man(X96)
| ~ young(X96)
| ~ in(X93,X92)
| ~ front(X92)
| ~ furniture(X92)
| ~ seat(X92)
| ~ ssSkC0
| X96 = X93 ),
inference(factor,[status(thm)],[clause56]) ).
cnf(c14386,plain,
( ~ street(X12131)
| ~ way(X12131)
| ~ lonely(X12131)
| ~ old(X12130)
| ~ dirty(X12130)
| ~ white(X12130)
| ~ car(X12130)
| ~ chevy(X12130)
| ~ event(X12129)
| ~ barrel(X12129,X12130)
| ~ down(X12129,X12131)
| ~ in(X12129,skc17)
| ~ city(skc17)
| ~ hollywood(skc17)
| ~ young(skc16)
| ~ man(skc16)
| ~ fellow(skc16)
| ~ fellow(X12129)
| ~ man(X12129)
| ~ young(X12129)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| X12129 = skc16 ),
inference(resolution,[status(thm)],[c14290,c381]) ).
cnf(c14345,plain,
( ~ street(X12121)
| ~ way(X12121)
| ~ lonely(X12121)
| ~ old(X12120)
| ~ dirty(X12120)
| ~ white(X12120)
| ~ car(X12120)
| ~ chevy(X12120)
| ~ event(X12119)
| ~ barrel(X12119,X12120)
| ~ down(X12119,X12121)
| ~ in(X12119,skc18)
| ~ city(skc18)
| ~ hollywood(skc18)
| ~ young(skc15)
| ~ man(skc15)
| ~ fellow(skc15)
| ~ fellow(X12119)
| ~ man(X12119)
| ~ young(X12119)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| X12119 = skc15 ),
inference(resolution,[status(thm)],[c14289,c381]) ).
cnf(c14310,plain,
( ~ street(X12116)
| ~ way(X12116)
| ~ lonely(X12116)
| ~ old(X12115)
| ~ dirty(X12115)
| ~ white(X12115)
| ~ car(X12115)
| ~ chevy(X12115)
| ~ event(X12114)
| ~ barrel(X12114,X12115)
| ~ down(X12114,X12116)
| ~ in(X12114,skc22)
| ~ city(skc22)
| ~ hollywood(skc22)
| ~ young(skc21)
| ~ man(skc21)
| ~ fellow(skc21)
| ~ fellow(X12114)
| ~ man(X12114)
| ~ young(X12114)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| X12114 = skc21 ),
inference(resolution,[status(thm)],[c14287,c381]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c18,axiom,
( X80 != X79
| X81 != X82
| ~ down(X80,X81)
| down(X79,X82) ),
theory(equality) ).
cnf(clause49,negated_conjecture,
( ~ ssSkC0
| down(skc21,skc20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(c14294,plain,
down(skc21,skc20),
inference(resolution,[status(thm)],[c14245,clause49]) ).
cnf(c14415,plain,
( skc21 != X11488
| skc20 != X11489
| down(X11488,X11489) ),
inference(resolution,[status(thm)],[c14294,c18]) ).
cnf(c14424,plain,
( skc21 != X11494
| down(X11494,skc20) ),
inference(resolution,[status(thm)],[c14415,reflexivity]) ).
cnf(c19,axiom,
( X84 != X83
| X85 != X86
| ~ in(X84,X85)
| in(X83,X86) ),
theory(equality) ).
cnf(c14390,plain,
( skc16 != X11485
| skc17 != X11486
| in(X11485,X11486) ),
inference(resolution,[status(thm)],[c14290,c19]) ).
cnf(c14422,plain,
( skc16 != X11487
| in(X11487,skc17) ),
inference(resolution,[status(thm)],[c14390,reflexivity]) ).
cnf(c14349,plain,
( skc15 != X11478
| skc18 != X11479
| in(X11478,X11479) ),
inference(resolution,[status(thm)],[c14289,c19]) ).
cnf(c14420,plain,
( skc15 != X11480
| in(X11480,skc18) ),
inference(resolution,[status(thm)],[c14349,reflexivity]) ).
cnf(c14314,plain,
( skc21 != X11475
| skc22 != X11476
| in(X11475,X11476) ),
inference(resolution,[status(thm)],[c14287,c19]) ).
cnf(c14418,plain,
( skc21 != X11477
| in(X11477,skc22) ),
inference(resolution,[status(thm)],[c14314,reflexivity]) ).
cnf(c17,axiom,
( X76 != X75
| X77 != X78
| ~ barrel(X76,X77)
| barrel(X75,X78) ),
theory(equality) ).
cnf(clause50,negated_conjecture,
( ~ ssSkC0
| barrel(skc21,skc19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(c14286,plain,
barrel(skc21,skc19),
inference(resolution,[status(thm)],[c14245,clause50]) ).
cnf(c14297,plain,
( skc21 != X11469
| skc19 != X11468
| barrel(X11469,X11468) ),
inference(resolution,[status(thm)],[c14286,c17]) ).
cnf(c14416,plain,
( skc21 != X11470
| barrel(X11470,skc19) ),
inference(resolution,[status(thm)],[c14297,reflexivity]) ).
cnf(clause34,negated_conjecture,
( ~ ssSkC0
| way(skc20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c14296,plain,
way(skc20),
inference(resolution,[status(thm)],[c14245,clause34]) ).
cnf(clause40,negated_conjecture,
( ~ ssSkC0
| young(skc16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(c14295,plain,
young(skc16),
inference(resolution,[status(thm)],[c14245,clause40]) ).
cnf(clause43,negated_conjecture,
( ~ ssSkC0
| furniture(skc17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c14293,plain,
furniture(skc17),
inference(resolution,[status(thm)],[c14245,clause43]) ).
cnf(clause33,negated_conjecture,
( ~ ssSkC0
| street(skc20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c14292,plain,
street(skc20),
inference(resolution,[status(thm)],[c14245,clause33]) ).
cnf(clause38,negated_conjecture,
( ~ ssSkC0
| front(skc18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c14291,plain,
front(skc18),
inference(resolution,[status(thm)],[c14245,clause38]) ).
cnf(clause31,negated_conjecture,
( ~ ssSkC0
| white(skc19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c14288,plain,
white(skc19),
inference(resolution,[status(thm)],[c14245,clause31]) ).
cnf(clause42,negated_conjecture,
( ~ ssSkC0
| seat(skc17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(c14285,plain,
seat(skc17),
inference(resolution,[status(thm)],[c14245,clause42]) ).
cnf(clause29,negated_conjecture,
( ~ ssSkC0
| old(skc19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(c14284,plain,
old(skc19),
inference(resolution,[status(thm)],[c14245,clause29]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| car(skc19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c14283,plain,
car(skc19),
inference(resolution,[status(thm)],[c14245,clause32]) ).
cnf(clause37,negated_conjecture,
( ~ ssSkC0
| man(skc15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(c14282,plain,
man(skc15),
inference(resolution,[status(thm)],[c14245,clause37]) ).
cnf(clause30,negated_conjecture,
( ~ ssSkC0
| dirty(skc19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(c14281,plain,
dirty(skc19),
inference(resolution,[status(thm)],[c14245,clause30]) ).
cnf(clause35,negated_conjecture,
( ~ ssSkC0
| hollywood(skc22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c14280,plain,
hollywood(skc22),
inference(resolution,[status(thm)],[c14245,clause35]) ).
cnf(clause36,negated_conjecture,
( ~ ssSkC0
| fellow(skc15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c14279,plain,
fellow(skc15),
inference(resolution,[status(thm)],[c14245,clause36]) ).
cnf(clause41,negated_conjecture,
( ~ ssSkC0
| man(skc16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c14278,plain,
man(skc16),
inference(resolution,[status(thm)],[c14245,clause41]) ).
cnf(clause39,negated_conjecture,
( ~ ssSkC0
| furniture(skc18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c14277,plain,
furniture(skc18),
inference(resolution,[status(thm)],[c14245,clause39]) ).
cnf(c16,axiom,
( X73 != X72
| ~ furniture(X73)
| furniture(X72) ),
theory(equality) ).
cnf(c15,axiom,
( X70 != X69
| ~ man(X70)
| man(X69) ),
theory(equality) ).
cnf(c14,axiom,
( X67 != X66
| ~ car(X67)
| car(X66) ),
theory(equality) ).
cnf(c13,axiom,
( X64 != X63
| ~ white(X64)
| white(X63) ),
theory(equality) ).
cnf(c12,axiom,
( X61 != X60
| ~ dirty(X61)
| dirty(X60) ),
theory(equality) ).
cnf(c11,axiom,
( X58 != X57
| ~ old(X58)
| old(X57) ),
theory(equality) ).
cnf(c10,axiom,
( X55 != X54
| ~ way(X55)
| way(X54) ),
theory(equality) ).
cnf(c9,axiom,
( X52 != X51
| ~ street(X52)
| street(X51) ),
theory(equality) ).
cnf(c8,axiom,
( X49 != X48
| ~ front(X49)
| front(X48) ),
theory(equality) ).
cnf(c7,axiom,
( X46 != X45
| ~ city(X46)
| city(X45) ),
theory(equality) ).
cnf(c6,axiom,
( X43 != X42
| ~ fellow(X43)
| fellow(X42) ),
theory(equality) ).
cnf(c5,axiom,
( X40 != X39
| ~ young(X40)
| young(X39) ),
theory(equality) ).
cnf(c4,axiom,
( X37 != X36
| ~ seat(X37)
| seat(X36) ),
theory(equality) ).
cnf(c3,axiom,
( X34 != X33
| ~ lonely(X34)
| lonely(X33) ),
theory(equality) ).
cnf(c2,axiom,
( X31 != X30
| ~ chevy(X31)
| chevy(X30) ),
theory(equality) ).
cnf(c1,axiom,
( X28 != X27
| ~ event(X28)
| event(X27) ),
theory(equality) ).
cnf(c0,axiom,
( X25 != X24
| ~ hollywood(X25)
| hollywood(X24) ),
theory(equality) ).
cnf(transitivity,axiom,
( X23 != X21
| X21 != X22
| X23 = X22 ),
theory(equality) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(clause55,negated_conjecture,
( skc16 != skc15
| ~ ssSkC0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
cnf(clause15,negated_conjecture,
young(skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(clause14,negated_conjecture,
fellow(skc16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,negated_conjecture,
front(skc17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(clause12,negated_conjecture,
seat(skc18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(clause11,negated_conjecture,
chevy(skc19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,negated_conjecture,
lonely(skc20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(clause9,negated_conjecture,
event(skc21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(clause8,negated_conjecture,
city(skc22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NLP013-1 : TPTP v8.1.2. Released v2.4.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 13:47:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 54.03/54.23 % Version: 1.5
% 54.03/54.23 % SZS status Satisfiable
% 54.03/54.23 % SZS output start Saturation
% See solution above
% 54.03/54.24
% 54.03/54.24 % Initial clauses : 80
% 54.03/54.24 % Processed clauses : 1112
% 54.03/54.24 % Factors computed : 67
% 54.03/54.24 % Resolvents computed: 14366
% 54.03/54.24 % Tautologies deleted: 1209
% 54.03/54.24 % Forward subsumed : 12192
% 54.03/54.24 % Backward subsumed : 1031
% 54.03/54.24 % -------- CPU Time ---------
% 54.03/54.24 % User time : 53.760 s
% 54.03/54.24 % System time : 0.103 s
% 54.03/54.24 % Total time : 53.863 s
%------------------------------------------------------------------------------