%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP005-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:32 EDT 2024
% Result : Satisfiable 73.03s 73.33s
% Output : Saturation 73.03s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause56,negated_conjecture,
( ~ lonely(X9)
| ~ way(X9)
| ~ street(X9)
| ~ chevy(X10)
| ~ car(X10)
| ~ white(X10)
| ~ dirty(X10)
| ~ old(X10)
| ~ down(X8,X9)
| ~ barrel(X8,X10)
| ~ event(X8)
| ~ hollywood(X12)
| ~ city(X12)
| ~ in(X8,X12)
| ~ young(X6)
| ~ man(X6)
| ~ fellow(X6)
| ~ fellow(X11)
| ~ man(X11)
| ~ young(X11)
| ~ in(X6,X7)
| ~ in(X11,X7)
| ~ front(X7)
| ~ furniture(X7)
| ~ seat(X7)
| ~ ssSkC0
| X11 = X6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(clause52,negated_conjecture,
( ~ ssSkC0
| in(skc15,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(clause54,negated_conjecture,
( skc24 != skc23
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(clause18,negated_conjecture,
( ssSkC0
| chevy(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( ssSkC0
| car(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(clause20,negated_conjecture,
( ssSkC0
| white(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(clause21,negated_conjecture,
( ssSkC0
| dirty(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(clause3,negated_conjecture,
old(skc27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause16,negated_conjecture,
( ssSkC0
| lonely(skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause17,negated_conjecture,
( ssSkC0
| way(skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause4,negated_conjecture,
street(skc26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause2,negated_conjecture,
event(skc28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause1,negated_conjecture,
city(skc29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause22,negated_conjecture,
( ssSkC0
| hollywood(skc29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(clause5,negated_conjecture,
seat(skc25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(clause28,negated_conjecture,
( ssSkC0
| furniture(skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(clause27,negated_conjecture,
( ssSkC0
| front(skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(clause7,negated_conjecture,
fellow(skc23),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause24,negated_conjecture,
( ssSkC0
| man(skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(clause23,negated_conjecture,
( ssSkC0
| young(skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(clause6,negated_conjecture,
young(skc24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(clause26,negated_conjecture,
( ssSkC0
| man(skc24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(clause25,negated_conjecture,
( ssSkC0
| fellow(skc24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause45,negated_conjecture,
( ssSkC0
| barrel(skc28,skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(clause44,negated_conjecture,
( ssSkC0
| down(skc28,skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(clause46,negated_conjecture,
( ssSkC0
| in(skc28,skc29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(clause47,negated_conjecture,
( ssSkC0
| in(skc23,skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(clause48,negated_conjecture,
( ssSkC0
| in(skc24,skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(clause57,negated_conjecture,
( ~ chevy(X17)
| ~ car(X17)
| ~ white(X17)
| ~ dirty(X17)
| ~ old(X17)
| ~ lonely(X18)
| ~ way(X18)
| ~ street(X18)
| ~ event(X15)
| ~ barrel(X15,X17)
| ~ down(X15,X18)
| ~ in(X15,X20)
| ~ city(X20)
| ~ hollywood(X20)
| ~ seat(X13)
| ~ furniture(X13)
| ~ front(X13)
| ~ in(X19,X13)
| ~ fellow(X19)
| ~ man(X19)
| ~ young(X19)
| ~ in(X14,X16)
| ~ front(X16)
| ~ furniture(X16)
| ~ seat(X16)
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ssSkC0
| X14 = X19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c388,plain,
( ~ chevy(X165)
| ~ car(X165)
| ~ white(X165)
| ~ dirty(X165)
| ~ old(X165)
| ~ lonely(X169)
| ~ way(X169)
| ~ street(X169)
| ~ event(X164)
| ~ barrel(X164,X165)
| ~ down(X164,X169)
| ~ in(X164,X168)
| ~ city(X168)
| ~ hollywood(X168)
| ~ seat(X167)
| ~ furniture(X167)
| ~ front(X167)
| ~ in(X166,X167)
| ~ fellow(X166)
| ~ man(X166)
| ~ young(X166)
| ~ front(skc25)
| ~ furniture(skc25)
| ~ seat(skc25)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = X166 ),
inference(resolution,[status(thm)],[clause57,clause48]) ).
cnf(c1151,plain,
( ~ chevy(X9011)
| ~ car(X9011)
| ~ white(X9011)
| ~ dirty(X9011)
| ~ old(X9011)
| ~ lonely(X9010)
| ~ way(X9010)
| ~ street(X9010)
| ~ event(X9008)
| ~ barrel(X9008,X9011)
| ~ down(X9008,X9010)
| ~ in(X9008,X9009)
| ~ city(X9009)
| ~ hollywood(X9009)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c388,clause47]) ).
cnf(c11686,plain,
( ~ chevy(X11759)
| ~ car(X11759)
| ~ white(X11759)
| ~ dirty(X11759)
| ~ old(X11759)
| ~ lonely(X11758)
| ~ way(X11758)
| ~ street(X11758)
| ~ event(skc28)
| ~ barrel(skc28,X11759)
| ~ down(skc28,X11758)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c1151,clause46]) ).
cnf(c17395,plain,
( ~ chevy(X11764)
| ~ car(X11764)
| ~ white(X11764)
| ~ dirty(X11764)
| ~ old(X11764)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ barrel(skc28,X11764)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c11686,clause44]) ).
cnf(c17406,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17395,clause45]) ).
cnf(c17444,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ young(skc24)
| ~ man(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17406,clause25]) ).
cnf(c17465,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ young(skc24)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17444,clause26]) ).
cnf(c17467,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17465,clause6]) ).
cnf(c17471,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ~ man(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17467,clause23]) ).
cnf(c17495,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ~ fellow(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17471,clause24]) ).
cnf(c17510,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17495,clause7]) ).
cnf(c17519,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ~ furniture(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17510,clause27]) ).
cnf(c17540,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ~ seat(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17519,clause28]) ).
cnf(c17553,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ~ hollywood(skc29)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17540,clause5]) ).
cnf(c17568,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ~ city(skc29)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17553,clause22]) ).
cnf(c17575,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ~ event(skc28)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17568,clause1]) ).
cnf(c17576,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ~ street(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17575,clause2]) ).
cnf(c17577,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ~ way(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17576,clause4]) ).
cnf(c17588,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ~ lonely(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17577,clause17]) ).
cnf(c17616,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ~ old(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17588,clause16]) ).
cnf(c17620,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ~ dirty(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17616,clause3]) ).
cnf(c17632,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ~ white(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17620,clause21]) ).
cnf(c17644,plain,
( ~ chevy(skc27)
| ~ car(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17632,clause20]) ).
cnf(c17666,plain,
( ~ chevy(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17644,clause19]) ).
cnf(c17692,plain,
( ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c17666,clause18]) ).
cnf(c17737,plain,
ssSkC0,
inference(resolution,[status(thm)],[c17692,clause54]) ).
cnf(c17779,plain,
in(skc15,skc18),
inference(resolution,[status(thm)],[c17737,clause52]) ).
cnf(c17888,plain,
( ~ lonely(X12657)
| ~ way(X12657)
| ~ street(X12657)
| ~ chevy(X12658)
| ~ car(X12658)
| ~ white(X12658)
| ~ dirty(X12658)
| ~ old(X12658)
| ~ down(X12656,X12657)
| ~ barrel(X12656,X12658)
| ~ event(X12656)
| ~ hollywood(X12660)
| ~ city(X12660)
| ~ in(X12656,X12660)
| ~ young(X12659)
| ~ man(X12659)
| ~ fellow(X12659)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ in(X12659,skc18)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X12659 ),
inference(resolution,[status(thm)],[c17779,clause56]) ).
cnf(c17976,plain,
( ~ lonely(X12670)
| ~ way(X12670)
| ~ street(X12670)
| ~ chevy(X12668)
| ~ car(X12668)
| ~ white(X12668)
| ~ dirty(X12668)
| ~ old(X12668)
| ~ down(X12669,X12670)
| ~ barrel(X12669,X12668)
| ~ event(X12669)
| ~ hollywood(skc18)
| ~ city(skc18)
| ~ in(X12669,skc18)
| ~ young(X12669)
| ~ man(X12669)
| ~ fellow(X12669)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X12669 ),
inference(factor,[status(thm)],[c17888]) ).
cnf(clause53,negated_conjecture,
( ~ ssSkC0
| in(skc16,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
cnf(c17773,plain,
in(skc16,skc17),
inference(resolution,[status(thm)],[c17737,clause53]) ).
cnf(c17852,plain,
( ~ lonely(X12638)
| ~ way(X12638)
| ~ street(X12638)
| ~ chevy(X12639)
| ~ car(X12639)
| ~ white(X12639)
| ~ dirty(X12639)
| ~ old(X12639)
| ~ down(X12637,X12638)
| ~ barrel(X12637,X12639)
| ~ event(X12637)
| ~ hollywood(X12641)
| ~ city(X12641)
| ~ in(X12637,X12641)
| ~ young(X12640)
| ~ man(X12640)
| ~ fellow(X12640)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ in(X12640,skc17)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X12640 ),
inference(resolution,[status(thm)],[c17773,clause56]) ).
cnf(c17972,plain,
( ~ lonely(X12651)
| ~ way(X12651)
| ~ street(X12651)
| ~ chevy(X12653)
| ~ car(X12653)
| ~ white(X12653)
| ~ dirty(X12653)
| ~ old(X12653)
| ~ down(X12652,X12651)
| ~ barrel(X12652,X12653)
| ~ event(X12652)
| ~ hollywood(skc17)
| ~ city(skc17)
| ~ in(X12652,skc17)
| ~ young(X12652)
| ~ man(X12652)
| ~ fellow(X12652)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X12652 ),
inference(factor,[status(thm)],[c17852]) ).
cnf(clause51,negated_conjecture,
( ~ ssSkC0
| in(skc21,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(c17772,plain,
in(skc21,skc22),
inference(resolution,[status(thm)],[c17737,clause51]) ).
cnf(c17810,plain,
( ~ lonely(X12619)
| ~ way(X12619)
| ~ street(X12619)
| ~ chevy(X12620)
| ~ car(X12620)
| ~ white(X12620)
| ~ dirty(X12620)
| ~ old(X12620)
| ~ down(X12618,X12619)
| ~ barrel(X12618,X12620)
| ~ event(X12618)
| ~ hollywood(X12622)
| ~ city(X12622)
| ~ in(X12618,X12622)
| ~ young(X12621)
| ~ man(X12621)
| ~ fellow(X12621)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ in(X12621,skc22)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X12621 ),
inference(resolution,[status(thm)],[c17772,clause56]) ).
cnf(c17968,plain,
( ~ lonely(X12634)
| ~ way(X12634)
| ~ street(X12634)
| ~ chevy(X12633)
| ~ car(X12633)
| ~ white(X12633)
| ~ dirty(X12633)
| ~ old(X12633)
| ~ down(X12632,X12634)
| ~ barrel(X12632,X12633)
| ~ event(X12632)
| ~ hollywood(skc22)
| ~ city(skc22)
| ~ in(X12632,skc22)
| ~ young(X12632)
| ~ man(X12632)
| ~ fellow(X12632)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X12632 ),
inference(factor,[status(thm)],[c17810]) ).
cnf(c381,plain,
( ~ lonely(X94)
| ~ way(X94)
| ~ street(X94)
| ~ chevy(X95)
| ~ car(X95)
| ~ white(X95)
| ~ dirty(X95)
| ~ old(X95)
| ~ down(X92,X94)
| ~ barrel(X92,X95)
| ~ event(X92)
| ~ hollywood(X93)
| ~ city(X93)
| ~ in(X92,X93)
| ~ young(X96)
| ~ man(X96)
| ~ fellow(X96)
| ~ fellow(X92)
| ~ man(X92)
| ~ young(X92)
| ~ in(X96,X93)
| ~ front(X93)
| ~ furniture(X93)
| ~ seat(X93)
| ~ ssSkC0
| X92 = X96 ),
inference(factor,[status(thm)],[clause56]) ).
cnf(c17902,plain,
( ~ lonely(X12586)
| ~ way(X12586)
| ~ street(X12586)
| ~ chevy(X12588)
| ~ car(X12588)
| ~ white(X12588)
| ~ dirty(X12588)
| ~ old(X12588)
| ~ down(X12587,X12586)
| ~ barrel(X12587,X12588)
| ~ event(X12587)
| ~ hollywood(skc18)
| ~ city(skc18)
| ~ in(X12587,skc18)
| ~ young(skc15)
| ~ man(skc15)
| ~ fellow(skc15)
| ~ fellow(X12587)
| ~ man(X12587)
| ~ young(X12587)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| X12587 = skc15 ),
inference(resolution,[status(thm)],[c17779,c381]) ).
cnf(c17862,plain,
( ~ lonely(X12576)
| ~ way(X12576)
| ~ street(X12576)
| ~ chevy(X12578)
| ~ car(X12578)
| ~ white(X12578)
| ~ dirty(X12578)
| ~ old(X12578)
| ~ down(X12577,X12576)
| ~ barrel(X12577,X12578)
| ~ event(X12577)
| ~ hollywood(skc17)
| ~ city(skc17)
| ~ in(X12577,skc17)
| ~ young(skc16)
| ~ man(skc16)
| ~ fellow(skc16)
| ~ fellow(X12577)
| ~ man(X12577)
| ~ young(X12577)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| X12577 = skc16 ),
inference(resolution,[status(thm)],[c17773,c381]) ).
cnf(c17825,plain,
( ~ lonely(X12571)
| ~ way(X12571)
| ~ street(X12571)
| ~ chevy(X12573)
| ~ car(X12573)
| ~ white(X12573)
| ~ dirty(X12573)
| ~ old(X12573)
| ~ down(X12572,X12571)
| ~ barrel(X12572,X12573)
| ~ event(X12572)
| ~ hollywood(skc22)
| ~ city(skc22)
| ~ in(X12572,skc22)
| ~ young(skc21)
| ~ man(skc21)
| ~ fellow(skc21)
| ~ fellow(X12572)
| ~ man(X12572)
| ~ young(X12572)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| X12572 = skc21 ),
inference(resolution,[status(thm)],[c17772,c381]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c19,axiom,
( X84 != X83
| X85 != X86
| ~ in(X84,X85)
| in(X83,X86) ),
theory(equality) ).
cnf(c17870,plain,
( skc15 != X11887
| skc18 != X11886
| in(X11887,X11886) ),
inference(resolution,[status(thm)],[c17779,c19]) ).
cnf(c17913,plain,
( skc15 != X11888
| in(X11888,skc18) ),
inference(resolution,[status(thm)],[c17870,reflexivity]) ).
cnf(c18,axiom,
( X80 != X79
| X81 != X82
| ~ barrel(X80,X81)
| barrel(X79,X82) ),
theory(equality) ).
cnf(clause49,negated_conjecture,
( ~ ssSkC0
| barrel(skc21,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c17776,plain,
barrel(skc21,skc19),
inference(resolution,[status(thm)],[c17737,clause49]) ).
cnf(c17865,plain,
( skc21 != X11880
| skc19 != X11879
| barrel(X11880,X11879) ),
inference(resolution,[status(thm)],[c17776,c18]) ).
cnf(c17911,plain,
( skc21 != X11881
| barrel(X11881,skc19) ),
inference(resolution,[status(thm)],[c17865,reflexivity]) ).
cnf(c17827,plain,
( skc16 != X11873
| skc17 != X11872
| in(X11873,X11872) ),
inference(resolution,[status(thm)],[c17773,c19]) ).
cnf(c17909,plain,
( skc16 != X11878
| in(X11878,skc17) ),
inference(resolution,[status(thm)],[c17827,reflexivity]) ).
cnf(c17792,plain,
( skc21 != X11870
| skc22 != X11869
| in(X11870,X11869) ),
inference(resolution,[status(thm)],[c17772,c19]) ).
cnf(c17907,plain,
( skc21 != X11871
| in(X11871,skc22) ),
inference(resolution,[status(thm)],[c17792,reflexivity]) ).
cnf(c17,axiom,
( X76 != X75
| X77 != X78
| ~ down(X76,X77)
| down(X75,X78) ),
theory(equality) ).
cnf(clause50,negated_conjecture,
( ~ ssSkC0
| down(skc21,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c17769,plain,
down(skc21,skc20),
inference(resolution,[status(thm)],[c17737,clause50]) ).
cnf(c17786,plain,
( skc21 != X11863
| skc20 != X11862
| down(X11863,X11862) ),
inference(resolution,[status(thm)],[c17769,c17]) ).
cnf(c17905,plain,
( skc21 != X11864
| down(X11864,skc20) ),
inference(resolution,[status(thm)],[c17786,reflexivity]) ).
cnf(clause43,negated_conjecture,
( ~ ssSkC0
| man(skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c17785,plain,
man(skc16),
inference(resolution,[status(thm)],[c17737,clause43]) ).
cnf(clause33,negated_conjecture,
( ~ ssSkC0
| lonely(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c17784,plain,
lonely(skc20),
inference(resolution,[status(thm)],[c17737,clause33]) ).
cnf(clause38,negated_conjecture,
( ~ ssSkC0
| fellow(skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c17783,plain,
fellow(skc15),
inference(resolution,[status(thm)],[c17737,clause38]) ).
cnf(clause29,negated_conjecture,
( ~ ssSkC0
| chevy(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c17782,plain,
chevy(skc19),
inference(resolution,[status(thm)],[c17737,clause29]) ).
cnf(clause41,negated_conjecture,
( ~ ssSkC0
| furniture(skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c17781,plain,
furniture(skc17),
inference(resolution,[status(thm)],[c17737,clause41]) ).
cnf(clause31,negated_conjecture,
( ~ ssSkC0
| white(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c17780,plain,
white(skc19),
inference(resolution,[status(thm)],[c17737,clause31]) ).
cnf(clause42,negated_conjecture,
( ~ ssSkC0
| young(skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c17778,plain,
young(skc16),
inference(resolution,[status(thm)],[c17737,clause42]) ).
cnf(clause40,negated_conjecture,
( ~ ssSkC0
| front(skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c17777,plain,
front(skc17),
inference(resolution,[status(thm)],[c17737,clause40]) ).
cnf(clause30,negated_conjecture,
( ~ ssSkC0
| car(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c17775,plain,
car(skc19),
inference(resolution,[status(thm)],[c17737,clause30]) ).
cnf(clause35,negated_conjecture,
( ~ ssSkC0
| city(skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c17774,plain,
city(skc22),
inference(resolution,[status(thm)],[c17737,clause35]) ).
cnf(clause39,negated_conjecture,
( ~ ssSkC0
| man(skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c17771,plain,
man(skc15),
inference(resolution,[status(thm)],[c17737,clause39]) ).
cnf(clause36,negated_conjecture,
( ~ ssSkC0
| seat(skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c17770,plain,
seat(skc18),
inference(resolution,[status(thm)],[c17737,clause36]) ).
cnf(clause34,negated_conjecture,
( ~ ssSkC0
| way(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c17768,plain,
way(skc20),
inference(resolution,[status(thm)],[c17737,clause34]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| dirty(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c17767,plain,
dirty(skc19),
inference(resolution,[status(thm)],[c17737,clause32]) ).
cnf(clause37,negated_conjecture,
( ~ ssSkC0
| furniture(skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c17766,plain,
furniture(skc18),
inference(resolution,[status(thm)],[c17737,clause37]) ).
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
| ~ dirty(X67)
| dirty(X66) ),
theory(equality) ).
cnf(c13,axiom,
( X64 != X63
| ~ white(X64)
| white(X63) ),
theory(equality) ).
cnf(c12,axiom,
( X61 != X60
| ~ car(X61)
| car(X60) ),
theory(equality) ).
cnf(c11,axiom,
( X58 != X57
| ~ chevy(X58)
| chevy(X57) ),
theory(equality) ).
cnf(c10,axiom,
( X55 != X54
| ~ way(X55)
| way(X54) ),
theory(equality) ).
cnf(c9,axiom,
( X52 != X51
| ~ lonely(X52)
| lonely(X51) ),
theory(equality) ).
cnf(c8,axiom,
( X49 != X48
| ~ front(X49)
| front(X48) ),
theory(equality) ).
cnf(c7,axiom,
( X46 != X45
| ~ hollywood(X46)
| hollywood(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
| ~ street(X34)
| street(X33) ),
theory(equality) ).
cnf(c2,axiom,
( X31 != X30
| ~ old(X31)
| old(X30) ),
theory(equality) ).
cnf(c1,axiom,
( X28 != X27
| ~ event(X28)
| event(X27) ),
theory(equality) ).
cnf(c0,axiom,
( X25 != X24
| ~ city(X25)
| city(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/sandbox/benchmark/theBenchmark.p',clause55) ).
cnf(clause15,negated_conjecture,
young(skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(clause14,negated_conjecture,
fellow(skc16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,negated_conjecture,
seat(skc17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause12,negated_conjecture,
front(skc18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(clause11,negated_conjecture,
old(skc19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,negated_conjecture,
street(skc20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause9,negated_conjecture,
event(skc21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause8,negated_conjecture,
hollywood(skc22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : NLP005-1 : TPTP v8.1.2. Released v2.4.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 13:31:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 73.03/73.33 % Version: 1.5
% 73.03/73.33 % SZS status Satisfiable
% 73.03/73.33 % SZS output start Saturation
% See solution above
% 73.03/73.33
% 73.03/73.33 % Initial clauses : 80
% 73.03/73.33 % Processed clauses : 1177
% 73.03/73.33 % Factors computed : 67
% 73.03/73.33 % Resolvents computed: 17892
% 73.03/73.33 % Tautologies deleted: 1747
% 73.03/73.33 % Forward subsumed : 15115
% 73.03/73.33 % Backward subsumed : 1096
% 73.03/73.33 % -------- CPU Time ---------
% 73.03/73.33 % User time : 72.788 s
% 73.03/73.33 % System time : 0.129 s
% 73.03/73.33 % Total time : 72.917 s
%------------------------------------------------------------------------------