%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP012-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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 96.87s 97.06s
% Output : Saturation 96.87s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause56,negated_conjecture,
( ~ street(X9)
| ~ way(X9)
| ~ lonely(X9)
| ~ old(X6)
| ~ dirty(X6)
| ~ white(X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ event(X11)
| ~ barrel(X11,X6)
| ~ down(X11,X9)
| ~ in(X11,X12)
| ~ city(X12)
| ~ hollywood(X12)
| ~ young(X8)
| ~ man(X8)
| ~ fellow(X8)
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| ~ in(X8,X10)
| ~ in(X7,X10)
| ~ front(X10)
| ~ furniture(X10)
| ~ seat(X10)
| ~ ssSkC0
| X7 = X8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(clause51,negated_conjecture,
( ~ ssSkC0
| in(skc21,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(clause54,negated_conjecture,
( skc24 != skc23
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(clause18,negated_conjecture,
( ssSkC0
| old(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( ssSkC0
| dirty(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
| car(skc27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(clause3,negated_conjecture,
chevy(skc27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause16,negated_conjecture,
( ssSkC0
| street(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,
lonely(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,
hollywood(skc29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause22,negated_conjecture,
( ssSkC0
| city(skc29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
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(clause45,negated_conjecture,
( ssSkC0
| down(skc28,skc26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(clause44,negated_conjecture,
( ssSkC0
| barrel(skc28,skc27) ),
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,
( ~ old(X16)
| ~ dirty(X16)
| ~ white(X16)
| ~ car(X16)
| ~ chevy(X16)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ down(X19,X13)
| ~ barrel(X19,X16)
| ~ event(X19)
| ~ hollywood(X20)
| ~ city(X20)
| ~ in(X19,X20)
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ in(X15,X14)
| ~ front(X14)
| ~ furniture(X14)
| ~ seat(X14)
| ~ young(X18)
| ~ man(X18)
| ~ fellow(X18)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| ~ in(X18,X17)
| ssSkC0
| X18 = X15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c388,plain,
( ~ old(X168)
| ~ dirty(X168)
| ~ white(X168)
| ~ car(X168)
| ~ chevy(X168)
| ~ street(X169)
| ~ way(X169)
| ~ lonely(X169)
| ~ down(X164,X169)
| ~ barrel(X164,X168)
| ~ event(X164)
| ~ hollywood(X166)
| ~ city(X166)
| ~ in(X164,X166)
| ~ fellow(X167)
| ~ man(X167)
| ~ young(X167)
| ~ in(X167,X165)
| ~ front(X165)
| ~ furniture(X165)
| ~ seat(X165)
| ~ young(skc24)
| ~ man(skc24)
| ~ fellow(skc24)
| ~ seat(skc25)
| ~ furniture(skc25)
| ~ front(skc25)
| ssSkC0
| skc24 = X167 ),
inference(resolution,[status(thm)],[clause57,clause48]) ).
cnf(c1187,plain,
( ~ old(X9497)
| ~ dirty(X9497)
| ~ white(X9497)
| ~ car(X9497)
| ~ chevy(X9497)
| ~ street(X9499)
| ~ way(X9499)
| ~ lonely(X9499)
| ~ down(X9496,X9499)
| ~ barrel(X9496,X9497)
| ~ event(X9496)
| ~ hollywood(X9498)
| ~ city(X9498)
| ~ in(X9496,X9498)
| ~ 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(c13519,plain,
( ~ old(X11995)
| ~ dirty(X11995)
| ~ white(X11995)
| ~ car(X11995)
| ~ chevy(X11995)
| ~ street(X11994)
| ~ way(X11994)
| ~ lonely(X11994)
| ~ down(skc28,X11994)
| ~ barrel(skc28,X11995)
| ~ 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)],[c1187,clause46]) ).
cnf(c20204,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(X12008)
| ~ way(X12008)
| ~ lonely(X12008)
| ~ down(skc28,X12008)
| ~ 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)],[c13519,clause44]) ).
cnf(c20356,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)],[c20204,clause45]) ).
cnf(c20373,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)],[c20356,clause25]) ).
cnf(c20392,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)],[c20373,clause26]) ).
cnf(c20413,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)],[c20392,clause6]) ).
cnf(c20414,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)],[c20413,clause5]) ).
cnf(c20427,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)],[c20414,clause28]) ).
cnf(c20565,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)],[c20427,clause27]) ).
cnf(c20584,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)],[c20565,clause23]) ).
cnf(c20601,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)],[c20584,clause24]) ).
cnf(c20616,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)],[c20601,clause7]) ).
cnf(c20634,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)],[c20616,clause22]) ).
cnf(c20638,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)],[c20634,clause1]) ).
cnf(c20639,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ~ lonely(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20638,clause2]) ).
cnf(c20640,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ~ way(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20639,clause4]) ).
cnf(c20657,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ~ street(skc26)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20640,clause17]) ).
cnf(c20679,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ~ chevy(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20657,clause16]) ).
cnf(c20683,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ~ car(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20679,clause3]) ).
cnf(c20700,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ~ white(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20683,clause21]) ).
cnf(c20713,plain,
( ~ old(skc27)
| ~ dirty(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20700,clause20]) ).
cnf(c20732,plain,
( ~ old(skc27)
| ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20713,clause19]) ).
cnf(c20757,plain,
( ssSkC0
| skc24 = skc23 ),
inference(resolution,[status(thm)],[c20732,clause18]) ).
cnf(c20827,plain,
ssSkC0,
inference(resolution,[status(thm)],[c20757,clause54]) ).
cnf(c20845,plain,
in(skc21,skc22),
inference(resolution,[status(thm)],[c20827,clause51]) ).
cnf(c20944,plain,
( ~ street(X12865)
| ~ way(X12865)
| ~ lonely(X12865)
| ~ old(X12864)
| ~ dirty(X12864)
| ~ white(X12864)
| ~ car(X12864)
| ~ chevy(X12864)
| ~ event(X12867)
| ~ barrel(X12867,X12864)
| ~ down(X12867,X12865)
| ~ in(X12867,X12863)
| ~ city(X12863)
| ~ hollywood(X12863)
| ~ young(X12866)
| ~ man(X12866)
| ~ fellow(X12866)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ in(X12866,skc22)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X12866 ),
inference(resolution,[status(thm)],[c20845,clause56]) ).
cnf(c21041,plain,
( ~ street(X12874)
| ~ way(X12874)
| ~ lonely(X12874)
| ~ old(X12875)
| ~ dirty(X12875)
| ~ white(X12875)
| ~ car(X12875)
| ~ chevy(X12875)
| ~ event(X12876)
| ~ barrel(X12876,X12875)
| ~ down(X12876,X12874)
| ~ in(X12876,skc22)
| ~ city(skc22)
| ~ hollywood(skc22)
| ~ young(X12876)
| ~ man(X12876)
| ~ fellow(X12876)
| ~ fellow(skc21)
| ~ man(skc21)
| ~ young(skc21)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| skc21 = X12876 ),
inference(factor,[status(thm)],[c20944]) ).
cnf(clause53,negated_conjecture,
( ~ ssSkC0
| in(skc16,skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
cnf(c20843,plain,
in(skc16,skc17),
inference(resolution,[status(thm)],[c20827,clause53]) ).
cnf(c20905,plain,
( ~ street(X12851)
| ~ way(X12851)
| ~ lonely(X12851)
| ~ old(X12850)
| ~ dirty(X12850)
| ~ white(X12850)
| ~ car(X12850)
| ~ chevy(X12850)
| ~ event(X12853)
| ~ barrel(X12853,X12850)
| ~ down(X12853,X12851)
| ~ in(X12853,X12849)
| ~ city(X12849)
| ~ hollywood(X12849)
| ~ young(X12852)
| ~ man(X12852)
| ~ fellow(X12852)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ in(X12852,skc17)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X12852 ),
inference(resolution,[status(thm)],[c20843,clause56]) ).
cnf(c21038,plain,
( ~ street(X12860)
| ~ way(X12860)
| ~ lonely(X12860)
| ~ old(X12859)
| ~ dirty(X12859)
| ~ white(X12859)
| ~ car(X12859)
| ~ chevy(X12859)
| ~ event(X12858)
| ~ barrel(X12858,X12859)
| ~ down(X12858,X12860)
| ~ in(X12858,skc17)
| ~ city(skc17)
| ~ hollywood(skc17)
| ~ young(X12858)
| ~ man(X12858)
| ~ fellow(X12858)
| ~ fellow(skc16)
| ~ man(skc16)
| ~ young(skc16)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| skc16 = X12858 ),
inference(factor,[status(thm)],[c20905]) ).
cnf(clause52,negated_conjecture,
( ~ ssSkC0
| in(skc15,skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c20842,plain,
in(skc15,skc18),
inference(resolution,[status(thm)],[c20827,clause52]) ).
cnf(c20867,plain,
( ~ street(X12835)
| ~ way(X12835)
| ~ lonely(X12835)
| ~ old(X12834)
| ~ dirty(X12834)
| ~ white(X12834)
| ~ car(X12834)
| ~ chevy(X12834)
| ~ event(X12837)
| ~ barrel(X12837,X12834)
| ~ down(X12837,X12835)
| ~ in(X12837,X12833)
| ~ city(X12833)
| ~ hollywood(X12833)
| ~ young(X12836)
| ~ man(X12836)
| ~ fellow(X12836)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ in(X12836,skc18)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X12836 ),
inference(resolution,[status(thm)],[c20842,clause56]) ).
cnf(c21035,plain,
( ~ street(X12844)
| ~ way(X12844)
| ~ lonely(X12844)
| ~ old(X12843)
| ~ dirty(X12843)
| ~ white(X12843)
| ~ car(X12843)
| ~ chevy(X12843)
| ~ event(X12842)
| ~ barrel(X12842,X12843)
| ~ down(X12842,X12844)
| ~ in(X12842,skc18)
| ~ city(skc18)
| ~ hollywood(skc18)
| ~ young(X12842)
| ~ man(X12842)
| ~ fellow(X12842)
| ~ fellow(skc15)
| ~ man(skc15)
| ~ young(skc15)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| skc15 = X12842 ),
inference(factor,[status(thm)],[c20867]) ).
cnf(c381,plain,
( ~ street(X93)
| ~ way(X93)
| ~ lonely(X93)
| ~ old(X92)
| ~ dirty(X92)
| ~ white(X92)
| ~ car(X92)
| ~ chevy(X92)
| ~ event(X96)
| ~ barrel(X96,X92)
| ~ down(X96,X93)
| ~ in(X96,X95)
| ~ city(X95)
| ~ hollywood(X95)
| ~ young(X94)
| ~ man(X94)
| ~ fellow(X94)
| ~ fellow(X96)
| ~ man(X96)
| ~ young(X96)
| ~ in(X94,X95)
| ~ front(X95)
| ~ furniture(X95)
| ~ seat(X95)
| ~ ssSkC0
| X96 = X94 ),
inference(factor,[status(thm)],[clause56]) ).
cnf(c20945,plain,
( ~ street(X12824)
| ~ way(X12824)
| ~ lonely(X12824)
| ~ old(X12825)
| ~ dirty(X12825)
| ~ white(X12825)
| ~ car(X12825)
| ~ chevy(X12825)
| ~ event(X12823)
| ~ barrel(X12823,X12825)
| ~ down(X12823,X12824)
| ~ in(X12823,skc22)
| ~ city(skc22)
| ~ hollywood(skc22)
| ~ young(skc21)
| ~ man(skc21)
| ~ fellow(skc21)
| ~ fellow(X12823)
| ~ man(X12823)
| ~ young(X12823)
| ~ front(skc22)
| ~ furniture(skc22)
| ~ seat(skc22)
| ~ ssSkC0
| X12823 = skc21 ),
inference(resolution,[status(thm)],[c20845,c381]) ).
cnf(c20906,plain,
( ~ street(X12819)
| ~ way(X12819)
| ~ lonely(X12819)
| ~ old(X12820)
| ~ dirty(X12820)
| ~ white(X12820)
| ~ car(X12820)
| ~ chevy(X12820)
| ~ event(X12818)
| ~ barrel(X12818,X12820)
| ~ down(X12818,X12819)
| ~ in(X12818,skc17)
| ~ city(skc17)
| ~ hollywood(skc17)
| ~ young(skc16)
| ~ man(skc16)
| ~ fellow(skc16)
| ~ fellow(X12818)
| ~ man(X12818)
| ~ young(X12818)
| ~ front(skc17)
| ~ furniture(skc17)
| ~ seat(skc17)
| ~ ssSkC0
| X12818 = skc16 ),
inference(resolution,[status(thm)],[c20843,c381]) ).
cnf(c20868,plain,
( ~ street(X12812)
| ~ way(X12812)
| ~ lonely(X12812)
| ~ old(X12813)
| ~ dirty(X12813)
| ~ white(X12813)
| ~ car(X12813)
| ~ chevy(X12813)
| ~ event(X12811)
| ~ barrel(X12811,X12813)
| ~ down(X12811,X12812)
| ~ in(X12811,skc18)
| ~ city(skc18)
| ~ hollywood(skc18)
| ~ young(skc15)
| ~ man(skc15)
| ~ fellow(skc15)
| ~ fellow(X12811)
| ~ man(X12811)
| ~ young(X12811)
| ~ front(skc18)
| ~ furniture(skc18)
| ~ seat(skc18)
| ~ ssSkC0
| X12811 = skc15 ),
inference(resolution,[status(thm)],[c20842,c381]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c19,axiom,
( X83 != X85
| X84 != X86
| ~ in(X83,X84)
| in(X85,X86) ),
theory(equality) ).
cnf(c20956,plain,
( skc21 != X12130
| skc22 != X12131
| in(X12130,X12131) ),
inference(resolution,[status(thm)],[c20845,c19]) ).
cnf(c20976,plain,
( skc21 != X12136
| in(X12136,skc22) ),
inference(resolution,[status(thm)],[c20956,reflexivity]) ).
cnf(c20917,plain,
( skc16 != X12127
| skc17 != X12128
| in(X12127,X12128) ),
inference(resolution,[status(thm)],[c20843,c19]) ).
cnf(c20974,plain,
( skc16 != X12129
| in(X12129,skc17) ),
inference(resolution,[status(thm)],[c20917,reflexivity]) ).
cnf(c20879,plain,
( skc15 != X12120
| skc18 != X12121
| in(X12120,X12121) ),
inference(resolution,[status(thm)],[c20842,c19]) ).
cnf(c20972,plain,
( skc15 != X12122
| in(X12122,skc18) ),
inference(resolution,[status(thm)],[c20879,reflexivity]) ).
cnf(c17,axiom,
( X75 != X77
| X76 != X78
| ~ barrel(X75,X76)
| barrel(X77,X78) ),
theory(equality) ).
cnf(clause50,negated_conjecture,
( ~ ssSkC0
| barrel(skc21,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c20840,plain,
barrel(skc21,skc19),
inference(resolution,[status(thm)],[c20827,clause50]) ).
cnf(c20850,plain,
( skc21 != X12117
| skc19 != X12118
| barrel(X12117,X12118) ),
inference(resolution,[status(thm)],[c20840,c17]) ).
cnf(c20970,plain,
( skc21 != X12119
| barrel(X12119,skc19) ),
inference(resolution,[status(thm)],[c20850,reflexivity]) ).
cnf(c18,axiom,
( X79 != X81
| X80 != X82
| ~ down(X79,X80)
| down(X81,X82) ),
theory(equality) ).
cnf(clause49,negated_conjecture,
( ~ ssSkC0
| down(skc21,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c20829,plain,
down(skc21,skc20),
inference(resolution,[status(thm)],[c20827,clause49]) ).
cnf(c20849,plain,
( skc21 != X12110
| skc20 != X12111
| down(X12110,X12111) ),
inference(resolution,[status(thm)],[c20829,c18]) ).
cnf(c20968,plain,
( skc21 != X12112
| down(X12112,skc20) ),
inference(resolution,[status(thm)],[c20849,reflexivity]) ).
cnf(clause30,negated_conjecture,
( ~ ssSkC0
| dirty(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c20848,plain,
dirty(skc19),
inference(resolution,[status(thm)],[c20827,clause30]) ).
cnf(clause35,negated_conjecture,
( ~ ssSkC0
| hollywood(skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c20847,plain,
hollywood(skc22),
inference(resolution,[status(thm)],[c20827,clause35]) ).
cnf(clause38,negated_conjecture,
( ~ ssSkC0
| front(skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c20846,plain,
front(skc18),
inference(resolution,[status(thm)],[c20827,clause38]) ).
cnf(clause39,negated_conjecture,
( ~ ssSkC0
| furniture(skc18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c20844,plain,
furniture(skc18),
inference(resolution,[status(thm)],[c20827,clause39]) ).
cnf(clause42,negated_conjecture,
( ~ ssSkC0
| seat(skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c20841,plain,
seat(skc17),
inference(resolution,[status(thm)],[c20827,clause42]) ).
cnf(clause32,negated_conjecture,
( ~ ssSkC0
| car(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c20839,plain,
car(skc19),
inference(resolution,[status(thm)],[c20827,clause32]) ).
cnf(clause37,negated_conjecture,
( ~ ssSkC0
| man(skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c20838,plain,
man(skc15),
inference(resolution,[status(thm)],[c20827,clause37]) ).
cnf(clause43,negated_conjecture,
( ~ ssSkC0
| furniture(skc17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c20837,plain,
furniture(skc17),
inference(resolution,[status(thm)],[c20827,clause43]) ).
cnf(clause33,negated_conjecture,
( ~ ssSkC0
| street(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c20836,plain,
street(skc20),
inference(resolution,[status(thm)],[c20827,clause33]) ).
cnf(clause36,negated_conjecture,
( ~ ssSkC0
| fellow(skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c20835,plain,
fellow(skc15),
inference(resolution,[status(thm)],[c20827,clause36]) ).
cnf(clause29,negated_conjecture,
( ~ ssSkC0
| old(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c20834,plain,
old(skc19),
inference(resolution,[status(thm)],[c20827,clause29]) ).
cnf(clause41,negated_conjecture,
( ~ ssSkC0
| man(skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c20833,plain,
man(skc16),
inference(resolution,[status(thm)],[c20827,clause41]) ).
cnf(clause31,negated_conjecture,
( ~ ssSkC0
| white(skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c20832,plain,
white(skc19),
inference(resolution,[status(thm)],[c20827,clause31]) ).
cnf(clause34,negated_conjecture,
( ~ ssSkC0
| way(skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c20831,plain,
way(skc20),
inference(resolution,[status(thm)],[c20827,clause34]) ).
cnf(clause40,negated_conjecture,
( ~ ssSkC0
| young(skc16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c20830,plain,
young(skc16),
inference(resolution,[status(thm)],[c20827,clause40]) ).
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
| ~ car(X66)
| car(X67) ),
theory(equality) ).
cnf(c13,axiom,
( X63 != X64
| ~ white(X63)
| white(X64) ),
theory(equality) ).
cnf(c12,axiom,
( X60 != X61
| ~ dirty(X60)
| dirty(X61) ),
theory(equality) ).
cnf(c11,axiom,
( X57 != X58
| ~ old(X57)
| old(X58) ),
theory(equality) ).
cnf(c10,axiom,
( X54 != X55
| ~ way(X54)
| way(X55) ),
theory(equality) ).
cnf(c9,axiom,
( X51 != X52
| ~ street(X51)
| street(X52) ),
theory(equality) ).
cnf(c8,axiom,
( X48 != X49
| ~ front(X48)
| front(X49) ),
theory(equality) ).
cnf(c7,axiom,
( X45 != X46
| ~ city(X45)
| city(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
| ~ lonely(X33)
| lonely(X34) ),
theory(equality) ).
cnf(c2,axiom,
( X30 != X31
| ~ chevy(X30)
| chevy(X31) ),
theory(equality) ).
cnf(c1,axiom,
( X27 != X28
| ~ event(X27)
| event(X28) ),
theory(equality) ).
cnf(c0,axiom,
( X24 != X25
| ~ hollywood(X24)
| hollywood(X25) ),
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,
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,
chevy(skc19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,negated_conjecture,
lonely(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.09/0.13 % Problem : NLP012-1 : TPTP v8.1.2. Released v2.4.0.
% 0.09/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n025.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 13:37:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 96.87/97.06 % Version: 1.5
% 96.87/97.06 % SZS status Satisfiable
% 96.87/97.06 % SZS output start Saturation
% See solution above
% 96.87/97.07
% 96.87/97.07 % Initial clauses : 80
% 96.87/97.07 % Processed clauses : 1207
% 96.87/97.07 % Factors computed : 67
% 96.87/97.07 % Resolvents computed: 20957
% 96.87/97.07 % Tautologies deleted: 2015
% 96.87/97.07 % Forward subsumed : 17882
% 96.87/97.07 % Backward subsumed : 1126
% 96.87/97.07 % -------- CPU Time ---------
% 96.87/97.07 % User time : 96.518 s
% 96.87/97.07 % System time : 0.178 s
% 96.87/97.07 % Total time : 96.696 s
%------------------------------------------------------------------------------