%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP008-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:33 EDT 2024
% Result : Satisfiable 35.67s 35.91s
% Output : Saturation 35.67s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause56,negated_conjecture,
( ~ old(X6)
| ~ dirty(X6)
| ~ white(X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ street(X7)
| ~ way(X7)
| ~ lonely(X7)
| ~ down(X10,X7)
| ~ barrel(X10,X6)
| ~ event(X10)
| ~ hollywood(X12)
| ~ city(X12)
| ~ in(X10,X12)
| ~ young(X11)
| ~ man(X11)
| ~ fellow(X11)
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ in(X11,X9)
| ~ in(X8,X9)
| ~ front(X9)
| ~ furniture(X9)
| ~ seat(X9)
| ~ ssSkC0
| X8 = X11 ),
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(clause3,negated_conjecture,
lonely(skc27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause21,negated_conjecture,
( ssSkC0
| way(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(clause20,negated_conjecture,
( ssSkC0
| street(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(clause4,negated_conjecture,
chevy(skc26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause19,negated_conjecture,
( ssSkC0
| car(skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(clause18,negated_conjecture,
( ssSkC0
| white(skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause17,negated_conjecture,
( ssSkC0
| dirty(skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause16,negated_conjecture,
( ssSkC0
| old(skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause2,negated_conjecture,
event(skc28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause22,negated_conjecture,
( ssSkC0
| hollywood(skc29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(clause1,negated_conjecture,
city(skc29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
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(clause27,negated_conjecture,
( ssSkC0
| front(skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(clause28,negated_conjecture,
( ssSkC0
| furniture(skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(clause5,negated_conjecture,
seat(skc25),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
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(clause44,negated_conjecture,
( ssSkC0
| down(skc28,skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(clause45,negated_conjecture,
( ssSkC0
| barrel(skc28,skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
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,
( ~ lonely(X13)
| ~ way(X13)
| ~ street(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ down(X17,X13)
| ~ barrel(X17,X14)
| ~ event(X17)
| ~ hollywood(X20)
| ~ city(X20)
| ~ in(X17,X20)
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ in(X18,X15)
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ young(X16)
| ~ man(X16)
| ~ fellow(X16)
| ~ seat(X19)
| ~ furniture(X19)
| ~ front(X19)
| ~ in(X16,X19)
| ssSkC0
| X16 = X18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c388,plain,
( ~ lonely(X168)
| ~ way(X168)
| ~ street(X168)
| ~ chevy(X164)
| ~ car(X164)
| ~ white(X164)
| ~ dirty(X164)
| ~ old(X164)
| ~ down(X167,X168)
| ~ barrel(X167,X164)
| ~ event(X167)
| ~ hollywood(X165)
| ~ city(X165)
| ~ in(X167,X165)
| ~ fellow(X169)
| ~ man(X169)
| ~ young(X169)
| ~ in(X169,X166)
| ~ front(X166)
| ~ furniture(X166)
| ~ seat(X166)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ssSkC0
| skc24 = X169 ),
inference(resolution,[status(thm)],[clause57,clause48]) ).
cnf(c1151,plain,
( ~ lonely(X9093)
| ~ way(X9093)
| ~ street(X9093)
| ~ chevy(X9092)
| ~ car(X9092)
| ~ white(X9092)
| ~ dirty(X9092)
| ~ old(X9092)
| ~ down(X9091,X9093)
| ~ barrel(X9091,X9092)
| ~ event(X9091)
| ~ hollywood(X9090)
| ~ city(X9090)
| ~ in(X9091,X9090)
| ~ 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(c7921,plain,
( ~ lonely(X10294)
| ~ way(X10294)
| ~ street(X10294)
| ~ chevy(X10295)
| ~ car(X10295)
| ~ white(X10295)
| ~ dirty(X10295)
| ~ old(X10295)
| ~ down(skc28,X10294)
| ~ barrel(skc28,X10295)
| ~ 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)],[c1151,clause46]) ).
cnf(c9666,plain,
( ~ lonely(X10308)
| ~ way(X10308)
| ~ street(X10308)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ down(skc28,X10308)
| ~ 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)],[c7921,clause45]) ).
cnf(c9714,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(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)],[c9666,clause44]) ).
cnf(c9728,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(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)],[c9714,clause25]) ).
cnf(c9758,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(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)],[c9728,clause26]) ).
cnf(c9766,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(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)],[c9758,clause6]) ).
cnf(c9767,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ~ furniture(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9766,clause5]) ).
cnf(c9896,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ~ front(skc25)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9767,clause28]) ).
cnf(c9918,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ~ young(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9896,clause27]) ).
cnf(c9938,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ~ man(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9918,clause23]) ).
cnf(c9955,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ~ fellow(skc23)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9938,clause24]) ).
cnf(c9969,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ~ city(skc29)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9955,clause7]) ).
cnf(c9970,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ~ hollywood(skc29)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9969,clause1]) ).
cnf(c9982,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ~ event(skc28)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9970,clause22]) ).
cnf(c9992,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ~ old(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9982,clause2]) ).
cnf(c9994,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ~ dirty(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9992,clause16]) ).
cnf(c10029,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ~ white(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c9994,clause17]) ).
cnf(c10043,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ~ car(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c10029,clause18]) ).
cnf(c10064,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ~ chevy(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c10043,clause19]) ).
cnf(c10077,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ~ street(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c10064,clause4]) ).
cnf(c10098,plain,
( ~ lonely(skc27)
| ~ way(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c10077,clause20]) ).
cnf(c10100,plain,
( ~ lonely(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c10098,clause21]) ).
cnf(c10120,plain,
( ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c10100,clause3]) ).
cnf(c10179,plain,
ssSkC0,
inference(resolution,[status(thm)],[c10120,clause54]) ).
cnf(c10195,plain,
in(skc15,skc18),
inference(resolution,[status(thm)],[c10179,clause52]) ).
cnf(c10299,plain,
( ~ old(X11096)
| ~ dirty(X11096)
| ~ white(X11096)
| ~ car(X11096)
| ~ chevy(X11096)
| ~ street(X11097)
| ~ way(X11097)
| ~ lonely(X11097)
| ~ down(X11095,X11097)
| ~ barrel(X11095,X11096)
| ~ event(X11095)
| ~ hollywood(X11093)
| ~ city(X11093)
| ~ in(X11095,X11093)
| ~ young(X11094)
| ~ man(X11094)
| ~ fellow(X11094)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ in(X11094,skc18)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X11094 ),
inference(resolution,[status(thm)],[c10195,clause56]) ).
cnf(c10340,plain,
( ~ old(X11104)
| ~ dirty(X11104)
| ~ white(X11104)
| ~ car(X11104)
| ~ chevy(X11104)
| ~ street(X11102)
| ~ way(X11102)
| ~ lonely(X11102)
| ~ down(X11103,X11102)
| ~ barrel(X11103,X11104)
| ~ event(X11103)
| ~ hollywood(skc18)
| ~ city(skc18)
| ~ in(X11103,skc18)
| ~ young(X11103)
| ~ man(X11103)
| ~ fellow(X11103)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X11103 ),
inference(factor,[status(thm)],[c10299]) ).
cnf(clause51,negated_conjecture,
( ~ ssSkC0
| in(skc21,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(c10193,plain,
in(skc21,skc22),
inference(resolution,[status(thm)],[c10179,clause51]) ).
cnf(c10260,plain,
( ~ old(X11078)
| ~ dirty(X11078)
| ~ white(X11078)
| ~ car(X11078)
| ~ chevy(X11078)
| ~ street(X11079)
| ~ way(X11079)
| ~ lonely(X11079)
| ~ down(X11077,X11079)
| ~ barrel(X11077,X11078)
| ~ event(X11077)
| ~ hollywood(X11075)
| ~ city(X11075)
| ~ in(X11077,X11075)
| ~ young(X11076)
| ~ man(X11076)
| ~ fellow(X11076)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ in(X11076,skc22)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X11076 ),
inference(resolution,[status(thm)],[c10193,clause56]) ).
cnf(c10337,plain,
( ~ old(X11085)
| ~ dirty(X11085)
| ~ white(X11085)
| ~ car(X11085)
| ~ chevy(X11085)
| ~ street(X11084)
| ~ way(X11084)
| ~ lonely(X11084)
| ~ down(X11086,X11084)
| ~ barrel(X11086,X11085)
| ~ event(X11086)
| ~ hollywood(skc22)
| ~ city(skc22)
| ~ in(X11086,skc22)
| ~ young(X11086)
| ~ man(X11086)
| ~ fellow(X11086)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X11086 ),
inference(factor,[status(thm)],[c10260]) ).
cnf(clause53,negated_conjecture,
( ~ ssSkC0
| in(skc16,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
cnf(c10182,plain,
in(skc16,skc17),
inference(resolution,[status(thm)],[c10179,clause53]) ).
cnf(c10220,plain,
( ~ old(X11060)
| ~ dirty(X11060)
| ~ white(X11060)
| ~ car(X11060)
| ~ chevy(X11060)
| ~ street(X11061)
| ~ way(X11061)
| ~ lonely(X11061)
| ~ down(X11059,X11061)
| ~ barrel(X11059,X11060)
| ~ event(X11059)
| ~ hollywood(X11057)
| ~ city(X11057)
| ~ in(X11059,X11057)
| ~ young(X11058)
| ~ man(X11058)
| ~ fellow(X11058)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ in(X11058,skc17)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X11058 ),
inference(resolution,[status(thm)],[c10182,clause56]) ).
cnf(c10334,plain,
( ~ old(X11070)
| ~ dirty(X11070)
| ~ white(X11070)
| ~ car(X11070)
| ~ chevy(X11070)
| ~ street(X11072)
| ~ way(X11072)
| ~ lonely(X11072)
| ~ down(X11071,X11072)
| ~ barrel(X11071,X11070)
| ~ event(X11071)
| ~ hollywood(skc17)
| ~ city(skc17)
| ~ in(X11071,skc17)
| ~ young(X11071)
| ~ man(X11071)
| ~ fellow(X11071)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X11071 ),
inference(factor,[status(thm)],[c10220]) ).
cnf(c381,plain,
( ~ old(X95)
| ~ dirty(X95)
| ~ white(X95)
| ~ car(X95)
| ~ chevy(X95)
| ~ street(X96)
| ~ way(X96)
| ~ lonely(X96)
| ~ down(X92,X96)
| ~ barrel(X92,X95)
| ~ event(X92)
| ~ hollywood(X93)
| ~ city(X93)
| ~ in(X92,X93)
| ~ young(X94)
| ~ man(X94)
| ~ fellow(X94)
| ~ fellow(X92)
| ~ man(X92)
| ~ young(X92)
| ~ in(X94,X93)
| ~ front(X93)
| ~ furniture(X93)
| ~ seat(X93)
| ~ ssSkC0
| X92 = X94 ),
inference(factor,[status(thm)],[clause56]) ).
cnf(c10296,plain,
( ~ old(X11047)
| ~ dirty(X11047)
| ~ white(X11047)
| ~ car(X11047)
| ~ chevy(X11047)
| ~ street(X11048)
| ~ way(X11048)
| ~ lonely(X11048)
| ~ down(X11049,X11048)
| ~ barrel(X11049,X11047)
| ~ event(X11049)
| ~ hollywood(skc18)
| ~ city(skc18)
| ~ in(X11049,skc18)
| ~ young(skc15)
| ~ man(skc15)
| ~ fellow(skc15)
| ~ fellow(X11049)
| ~ man(X11049)
| ~ young(X11049)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| X11049 = skc15 ),
inference(resolution,[status(thm)],[c10195,c381]) ).
cnf(c10258,plain,
( ~ old(X11038)
| ~ dirty(X11038)
| ~ white(X11038)
| ~ car(X11038)
| ~ chevy(X11038)
| ~ street(X11039)
| ~ way(X11039)
| ~ lonely(X11039)
| ~ down(X11040,X11039)
| ~ barrel(X11040,X11038)
| ~ event(X11040)
| ~ hollywood(skc22)
| ~ city(skc22)
| ~ in(X11040,skc22)
| ~ young(skc21)
| ~ man(skc21)
| ~ fellow(skc21)
| ~ fellow(X11040)
| ~ man(X11040)
| ~ young(X11040)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| X11040 = skc21 ),
inference(resolution,[status(thm)],[c10193,c381]) ).
cnf(c10219,plain,
( ~ old(X11033)
| ~ dirty(X11033)
| ~ white(X11033)
| ~ car(X11033)
| ~ chevy(X11033)
| ~ street(X11034)
| ~ way(X11034)
| ~ lonely(X11034)
| ~ down(X11035,X11034)
| ~ barrel(X11035,X11033)
| ~ event(X11035)
| ~ hollywood(skc17)
| ~ city(skc17)
| ~ in(X11035,skc17)
| ~ young(skc16)
| ~ man(skc16)
| ~ fellow(skc16)
| ~ fellow(X11035)
| ~ man(X11035)
| ~ young(X11035)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| X11035 = skc16 ),
inference(resolution,[status(thm)],[c10182,c381]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c17,axiom,
( X75 != X77
| X76 != X78
| ~ down(X75,X76)
| down(X77,X78) ),
theory(equality) ).
cnf(clause49,negated_conjecture,
( ~ ssSkC0
| down(skc21,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c10199,plain,
down(skc21,skc19),
inference(resolution,[status(thm)],[c10179,clause49]) ).
cnf(c10320,plain,
( skc21 != X10415
| skc19 != X10414
| down(X10415,X10414) ),
inference(resolution,[status(thm)],[c10199,c17]) ).
cnf(c10329,plain,
( skc21 != X10416
| down(X10416,skc19) ),
inference(resolution,[status(thm)],[c10320,reflexivity]) ).
cnf(c19,axiom,
( X83 != X85
| X84 != X86
| ~ in(X83,X84)
| in(X85,X86) ),
theory(equality) ).
cnf(c10317,plain,
( skc15 != X10407
| skc18 != X10408
| in(X10407,X10408) ),
inference(resolution,[status(thm)],[c10195,c19]) ).
cnf(c10327,plain,
( skc15 != X10409
| in(X10409,skc18) ),
inference(resolution,[status(thm)],[c10317,reflexivity]) ).
cnf(c10279,plain,
( skc21 != X10400
| skc22 != X10401
| in(X10400,X10401) ),
inference(resolution,[status(thm)],[c10193,c19]) ).
cnf(c10325,plain,
( skc21 != X10406
| in(X10406,skc22) ),
inference(resolution,[status(thm)],[c10279,reflexivity]) ).
cnf(c18,axiom,
( X79 != X81
| X80 != X82
| ~ barrel(X79,X80)
| barrel(X81,X82) ),
theory(equality) ).
cnf(clause50,negated_conjecture,
( ~ ssSkC0
| barrel(skc21,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c10192,plain,
barrel(skc21,skc20),
inference(resolution,[status(thm)],[c10179,clause50]) ).
cnf(c10241,plain,
( skc21 != X10398
| skc20 != X10397
| barrel(X10398,X10397) ),
inference(resolution,[status(thm)],[c10192,c18]) ).
cnf(c10323,plain,
( skc21 != X10399
| barrel(X10399,skc20) ),
inference(resolution,[status(thm)],[c10241,reflexivity]) ).
cnf(c10238,plain,
( skc16 != X10390
| skc17 != X10391
| in(X10390,X10391) ),
inference(resolution,[status(thm)],[c10182,c19]) ).
cnf(c10321,plain,
( skc16 != X10392
| in(X10392,skc17) ),
inference(resolution,[status(thm)],[c10238,reflexivity]) ).
cnf(clause34,negated_conjecture,
( ~ ssSkC0
| dirty(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c10201,plain,
dirty(skc20),
inference(resolution,[status(thm)],[c10179,clause34]) ).
cnf(clause40,negated_conjecture,
( ~ ssSkC0
| young(skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c10200,plain,
young(skc16),
inference(resolution,[status(thm)],[c10179,clause40]) ).
cnf(clause43,negated_conjecture,
( ~ ssSkC0
| furniture(skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c10198,plain,
furniture(skc17),
inference(resolution,[status(thm)],[c10179,clause43]) ).
cnf(clause33,negated_conjecture,
( ~ ssSkC0
| white(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c10197,plain,
white(skc20),
inference(resolution,[status(thm)],[c10179,clause33]) ).
cnf(clause38,negated_conjecture,
( ~ ssSkC0
| front(skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c10196,plain,
front(skc18),
inference(resolution,[status(thm)],[c10179,clause38]) ).
cnf(clause31,negated_conjecture,
( ~ ssSkC0
| chevy(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c10194,plain,
chevy(skc20),
inference(resolution,[status(thm)],[c10179,clause31]) ).
cnf(clause42,negated_conjecture,
( ~ ssSkC0
| seat(skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c10191,plain,
seat(skc17),
inference(resolution,[status(thm)],[c10179,clause42]) ).
cnf(clause29,negated_conjecture,
( ~ ssSkC0
| lonely(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c10190,plain,
lonely(skc19),
inference(resolution,[status(thm)],[c10179,clause29]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| car(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c10189,plain,
car(skc20),
inference(resolution,[status(thm)],[c10179,clause32]) ).
cnf(clause37,negated_conjecture,
( ~ ssSkC0
| man(skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c10188,plain,
man(skc15),
inference(resolution,[status(thm)],[c10179,clause37]) ).
cnf(clause30,negated_conjecture,
( ~ ssSkC0
| way(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c10187,plain,
way(skc19),
inference(resolution,[status(thm)],[c10179,clause30]) ).
cnf(clause35,negated_conjecture,
( ~ ssSkC0
| hollywood(skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c10186,plain,
hollywood(skc22),
inference(resolution,[status(thm)],[c10179,clause35]) ).
cnf(clause36,negated_conjecture,
( ~ ssSkC0
| fellow(skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c10185,plain,
fellow(skc15),
inference(resolution,[status(thm)],[c10179,clause36]) ).
cnf(clause41,negated_conjecture,
( ~ ssSkC0
| man(skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c10184,plain,
man(skc16),
inference(resolution,[status(thm)],[c10179,clause41]) ).
cnf(clause39,negated_conjecture,
( ~ ssSkC0
| furniture(skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c10183,plain,
furniture(skc18),
inference(resolution,[status(thm)],[c10179,clause39]) ).
cnf(c16,axiom,
( X72 != X73
| ~ furniture(X72)
| furniture(X73) ),
theory(equality) ).
cnf(c15,axiom,
( X69 != X70
| ~ man(X69)
| man(X70) ),
theory(equality) ).
cnf(c14,axiom,
( X66 != X67
| ~ hollywood(X66)
| hollywood(X67) ),
theory(equality) ).
cnf(c13,axiom,
( X63 != X64
| ~ way(X63)
| way(X64) ),
theory(equality) ).
cnf(c12,axiom,
( X60 != X61
| ~ car(X60)
| car(X61) ),
theory(equality) ).
cnf(c11,axiom,
( X57 != X58
| ~ white(X57)
| white(X58) ),
theory(equality) ).
cnf(c10,axiom,
( X54 != X55
| ~ dirty(X54)
| dirty(X55) ),
theory(equality) ).
cnf(c9,axiom,
( X51 != X52
| ~ front(X51)
| front(X52) ),
theory(equality) ).
cnf(c8,axiom,
( X48 != X49
| ~ street(X48)
| street(X49) ),
theory(equality) ).
cnf(c7,axiom,
( X45 != X46
| ~ old(X45)
| old(X46) ),
theory(equality) ).
cnf(c6,axiom,
( X42 != X43
| ~ fellow(X42)
| fellow(X43) ),
theory(equality) ).
cnf(c5,axiom,
( X39 != X40
| ~ young(X39)
| young(X40) ),
theory(equality) ).
cnf(c4,axiom,
( X36 != X37
| ~ seat(X36)
| seat(X37) ),
theory(equality) ).
cnf(c3,axiom,
( X33 != X34
| ~ chevy(X33)
| chevy(X34) ),
theory(equality) ).
cnf(c2,axiom,
( X30 != X31
| ~ lonely(X30)
| lonely(X31) ),
theory(equality) ).
cnf(c1,axiom,
( X27 != X28
| ~ event(X27)
| event(X28) ),
theory(equality) ).
cnf(c0,axiom,
( X24 != X25
| ~ city(X24)
| city(X25) ),
theory(equality) ).
cnf(transitivity,axiom,
( X23 != X22
| X22 != X21
| X23 = X21 ),
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,
front(skc17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause12,negated_conjecture,
seat(skc18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(clause11,negated_conjecture,
street(skc19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,negated_conjecture,
old(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,
city(skc22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP008-1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n003.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 13:40:07 EDT 2024
% 0.13/0.33 % CPUTime :
% 35.67/35.91 % Version: 1.5
% 35.67/35.91 % SZS status Satisfiable
% 35.67/35.91 % SZS output start Saturation
% See solution above
% 35.67/35.91
% 35.67/35.91 % Initial clauses : 80
% 35.67/35.91 % Processed clauses : 1062
% 35.67/35.91 % Factors computed : 67
% 35.67/35.91 % Resolvents computed: 10256
% 35.67/35.91 % Tautologies deleted: 765
% 35.67/35.91 % Forward subsumed : 8576
% 35.67/35.91 % Backward subsumed : 981
% 35.67/35.91 % -------- CPU Time ---------
% 35.67/35.91 % User time : 35.495 s
% 35.67/35.91 % System time : 0.079 s
% 35.67/35.91 % Total time : 35.574 s
%------------------------------------------------------------------------------