%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP001-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:30 EDT 2024
% Result : Unsatisfiable 0.60s 0.81s
% Output : Refutation 0.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 30
% Syntax : Number of clauses : 69 ( 21 unt; 10 nHn; 69 RR)
% Number of literals : 299 ( 0 equ; 235 neg)
% Maximal clause size : 15 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 2 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 14 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause3,negated_conjecture,
street(skc13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause14,negated_conjecture,
( ssSkC0
| way(skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,negated_conjecture,
( ssSkC0
| lonely(skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause4,negated_conjecture,
old(skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause12,negated_conjecture,
( ssSkC0
| dirty(skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(clause11,negated_conjecture,
( ssSkC0
| white(skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,negated_conjecture,
( ssSkC0
| car(skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause9,negated_conjecture,
( ssSkC0
| chevy(skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause2,negated_conjecture,
event(skc14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause15,negated_conjecture,
( ssSkC0
| city(skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(clause1,negated_conjecture,
hollywood(skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause23,negated_conjecture,
( ssSkC0
| barrel(skc14,skc12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(clause24,negated_conjecture,
( ssSkC0
| down(skc14,skc13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(clause25,negated_conjecture,
( ssSkC0
| in(skc14,skc15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause29,negated_conjecture,
( ~ street(X4)
| ~ way(X4)
| ~ lonely(X4)
| ~ old(X3)
| ~ dirty(X3)
| ~ white(X3)
| ~ car(X3)
| ~ chevy(X3)
| ~ event(X5)
| ~ barrel(X5,X3)
| ~ down(X5,X4)
| ~ in(X5,X2)
| ~ city(X2)
| ~ hollywood(X2)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c100,plain,
( ~ street(X10)
| ~ way(X10)
| ~ lonely(X10)
| ~ old(X11)
| ~ dirty(X11)
| ~ white(X11)
| ~ car(X11)
| ~ chevy(X11)
| ~ event(skc14)
| ~ barrel(skc14,X11)
| ~ down(skc14,X10)
| ~ city(skc15)
| ~ hollywood(skc15)
| ssSkC0 ),
inference(resolution,[status(thm)],[clause29,clause25]) ).
cnf(c144,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(X14)
| ~ dirty(X14)
| ~ white(X14)
| ~ car(X14)
| ~ chevy(X14)
| ~ event(skc14)
| ~ barrel(skc14,X14)
| ~ city(skc15)
| ~ hollywood(skc15)
| ssSkC0 ),
inference(resolution,[status(thm)],[c100,clause24]) ).
cnf(c158,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ~ dirty(skc12)
| ~ white(skc12)
| ~ car(skc12)
| ~ chevy(skc12)
| ~ event(skc14)
| ~ city(skc15)
| ~ hollywood(skc15)
| ssSkC0 ),
inference(resolution,[status(thm)],[c144,clause23]) ).
cnf(c164,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ~ dirty(skc12)
| ~ white(skc12)
| ~ car(skc12)
| ~ chevy(skc12)
| ~ event(skc14)
| ~ city(skc15)
| ssSkC0 ),
inference(resolution,[status(thm)],[c158,clause1]) ).
cnf(c173,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ~ dirty(skc12)
| ~ white(skc12)
| ~ car(skc12)
| ~ chevy(skc12)
| ~ event(skc14)
| ssSkC0 ),
inference(resolution,[status(thm)],[c164,clause15]) ).
cnf(c176,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ~ dirty(skc12)
| ~ white(skc12)
| ~ car(skc12)
| ~ chevy(skc12)
| ssSkC0 ),
inference(resolution,[status(thm)],[c173,clause2]) ).
cnf(c180,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ~ dirty(skc12)
| ~ white(skc12)
| ~ car(skc12)
| ssSkC0 ),
inference(resolution,[status(thm)],[c176,clause9]) ).
cnf(c197,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ~ dirty(skc12)
| ~ white(skc12)
| ssSkC0 ),
inference(resolution,[status(thm)],[c180,clause10]) ).
cnf(c203,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ~ dirty(skc12)
| ssSkC0 ),
inference(resolution,[status(thm)],[c197,clause11]) ).
cnf(c214,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ~ old(skc12)
| ssSkC0 ),
inference(resolution,[status(thm)],[c203,clause12]) ).
cnf(c221,plain,
( ~ street(skc13)
| ~ way(skc13)
| ~ lonely(skc13)
| ssSkC0 ),
inference(resolution,[status(thm)],[c214,clause4]) ).
cnf(c231,plain,
( ~ street(skc13)
| ~ way(skc13)
| ssSkC0 ),
inference(resolution,[status(thm)],[c221,clause13]) ).
cnf(c241,plain,
( ~ street(skc13)
| ssSkC0 ),
inference(resolution,[status(thm)],[c231,clause14]) ).
cnf(c244,plain,
ssSkC0,
inference(resolution,[status(thm)],[c241,clause3]) ).
cnf(clause7,negated_conjecture,
chevy(skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause21,negated_conjecture,
( ~ ssSkC0
| car(skc9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c253,plain,
car(skc9),
inference(resolution,[status(thm)],[c244,clause21]) ).
cnf(clause20,negated_conjecture,
( ~ ssSkC0
| white(skc9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c249,plain,
white(skc9),
inference(resolution,[status(thm)],[c244,clause20]) ).
cnf(clause19,negated_conjecture,
( ~ ssSkC0
| dirty(skc9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c246,plain,
dirty(skc9),
inference(resolution,[status(thm)],[c244,clause19]) ).
cnf(clause18,negated_conjecture,
( ~ ssSkC0
| old(skc9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c251,plain,
old(skc9),
inference(resolution,[status(thm)],[c244,clause18]) ).
cnf(clause8,negated_conjecture,
lonely(skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(clause17,negated_conjecture,
( ~ ssSkC0
| way(skc8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c247,plain,
way(skc8),
inference(resolution,[status(thm)],[c244,clause17]) ).
cnf(clause16,negated_conjecture,
( ~ ssSkC0
| street(skc8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c252,plain,
street(skc8),
inference(resolution,[status(thm)],[c244,clause16]) ).
cnf(clause6,negated_conjecture,
event(skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(clause22,negated_conjecture,
( ~ ssSkC0
| city(skc11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c245,plain,
city(skc11),
inference(resolution,[status(thm)],[c244,clause22]) ).
cnf(clause5,negated_conjecture,
hollywood(skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(clause26,negated_conjecture,
( ~ ssSkC0
| barrel(skc10,skc9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c254,plain,
barrel(skc10,skc9),
inference(resolution,[status(thm)],[c244,clause26]) ).
cnf(clause27,negated_conjecture,
( ~ ssSkC0
| down(skc10,skc8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c250,plain,
down(skc10,skc8),
inference(resolution,[status(thm)],[c244,clause27]) ).
cnf(clause30,negated_conjecture,
( ~ chevy(X8)
| ~ car(X8)
| ~ white(X8)
| ~ dirty(X8)
| ~ old(X8)
| ~ lonely(X7)
| ~ way(X7)
| ~ street(X7)
| ~ event(X9)
| ~ barrel(X9,X8)
| ~ down(X9,X7)
| ~ in(X9,X6)
| ~ city(X6)
| ~ hollywood(X6)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(clause28,negated_conjecture,
( ~ ssSkC0
| in(skc10,skc11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c248,plain,
in(skc10,skc11),
inference(resolution,[status(thm)],[c244,clause28]) ).
cnf(c255,plain,
( ~ chevy(X52)
| ~ car(X52)
| ~ white(X52)
| ~ dirty(X52)
| ~ old(X52)
| ~ lonely(X51)
| ~ way(X51)
| ~ street(X51)
| ~ event(skc10)
| ~ barrel(skc10,X52)
| ~ down(skc10,X51)
| ~ city(skc11)
| ~ hollywood(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c248,clause30]) ).
cnf(c258,plain,
( ~ chevy(X53)
| ~ car(X53)
| ~ white(X53)
| ~ dirty(X53)
| ~ old(X53)
| ~ lonely(skc8)
| ~ way(skc8)
| ~ street(skc8)
| ~ event(skc10)
| ~ barrel(skc10,X53)
| ~ city(skc11)
| ~ hollywood(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c255,c250]) ).
cnf(c259,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ old(skc9)
| ~ lonely(skc8)
| ~ way(skc8)
| ~ street(skc8)
| ~ event(skc10)
| ~ city(skc11)
| ~ hollywood(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c258,c254]) ).
cnf(c260,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ old(skc9)
| ~ lonely(skc8)
| ~ way(skc8)
| ~ street(skc8)
| ~ event(skc10)
| ~ city(skc11)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c259,clause5]) ).
cnf(c261,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ old(skc9)
| ~ lonely(skc8)
| ~ way(skc8)
| ~ street(skc8)
| ~ event(skc10)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c260,c245]) ).
cnf(c262,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ old(skc9)
| ~ lonely(skc8)
| ~ way(skc8)
| ~ street(skc8)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c261,clause6]) ).
cnf(c263,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ old(skc9)
| ~ lonely(skc8)
| ~ way(skc8)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c262,c252]) ).
cnf(c264,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ old(skc9)
| ~ lonely(skc8)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c263,c247]) ).
cnf(c265,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ old(skc9)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c264,clause8]) ).
cnf(c266,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ dirty(skc9)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c265,c251]) ).
cnf(c267,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ white(skc9)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c266,c246]) ).
cnf(c268,plain,
( ~ chevy(skc9)
| ~ car(skc9)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c267,c249]) ).
cnf(c269,plain,
( ~ chevy(skc9)
| ~ ssSkC0 ),
inference(resolution,[status(thm)],[c268,c253]) ).
cnf(c270,plain,
~ ssSkC0,
inference(resolution,[status(thm)],[c269,clause7]) ).
cnf(c271,plain,
$false,
inference(resolution,[status(thm)],[c270,c244]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : NLP001-1 : TPTP v8.1.2. Released v2.4.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n021.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:49:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.60/0.81 % Version: 1.5
% 0.60/0.81 % SZS status Unsatisfiable
% 0.60/0.81 % SZS output start CNFRefutation
% See solution above
% 0.60/0.81
% 0.60/0.81 % Initial clauses : 30
% 0.60/0.81 % Processed clauses : 170
% 0.60/0.81 % Factors computed : 0
% 0.60/0.81 % Resolvents computed: 272
% 0.60/0.81 % Tautologies deleted: 1
% 0.60/0.81 % Forward subsumed : 89
% 0.60/0.81 % Backward subsumed : 150
% 0.60/0.81 % -------- CPU Time ---------
% 0.60/0.81 % User time : 0.422 s
% 0.60/0.81 % System time : 0.017 s
% 0.60/0.81 % Total time : 0.439 s
%------------------------------------------------------------------------------