%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP001-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:50:59 AM UTC 2026
% Result : Unsatisfiable 0.12s 16.23s
% Output : Proof 0.12s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
hollywood(skc15),
file('theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
event(skc14),
file('theBenchmark.p',clause2) ).
cnf(clause3,negated_conjecture,
street(skc13),
file('theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
old(skc12),
file('theBenchmark.p',clause4) ).
cnf(clause5,negated_conjecture,
hollywood(skc11),
file('theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
event(skc10),
file('theBenchmark.p',clause6) ).
cnf(clause7,negated_conjecture,
chevy(skc9),
file('theBenchmark.p',clause7) ).
cnf(clause8,negated_conjecture,
lonely(skc8),
file('theBenchmark.p',clause8) ).
cnf(clause9,negated_conjecture,
( chevy(skc12)
| ssSkC0 ),
file('theBenchmark.p',clause9) ).
cnf(clause10,negated_conjecture,
( car(skc12)
| ssSkC0 ),
file('theBenchmark.p',clause10) ).
cnf(clause11,negated_conjecture,
( white(skc12)
| ssSkC0 ),
file('theBenchmark.p',clause11) ).
cnf(clause12,negated_conjecture,
( dirty(skc12)
| ssSkC0 ),
file('theBenchmark.p',clause12) ).
cnf(clause13,negated_conjecture,
( lonely(skc13)
| ssSkC0 ),
file('theBenchmark.p',clause13) ).
cnf(clause14,negated_conjecture,
( way(skc13)
| ssSkC0 ),
file('theBenchmark.p',clause14) ).
cnf(clause15,negated_conjecture,
( city(skc15)
| ssSkC0 ),
file('theBenchmark.p',clause15) ).
cnf(clause16,negated_conjecture,
( street(skc8)
| ~ ssSkC0 ),
file('theBenchmark.p',clause16) ).
cnf(clause17,negated_conjecture,
( way(skc8)
| ~ ssSkC0 ),
file('theBenchmark.p',clause17) ).
cnf(clause18,negated_conjecture,
( old(skc9)
| ~ ssSkC0 ),
file('theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( dirty(skc9)
| ~ ssSkC0 ),
file('theBenchmark.p',clause19) ).
cnf(clause20,negated_conjecture,
( white(skc9)
| ~ ssSkC0 ),
file('theBenchmark.p',clause20) ).
cnf(clause21,negated_conjecture,
( car(skc9)
| ~ ssSkC0 ),
file('theBenchmark.p',clause21) ).
cnf(clause22,negated_conjecture,
( city(skc11)
| ~ ssSkC0 ),
file('theBenchmark.p',clause22) ).
cnf(clause23,negated_conjecture,
( barrel(skc14,skc12)
| ssSkC0 ),
file('theBenchmark.p',clause23) ).
cnf(clause24,negated_conjecture,
( down(skc14,skc13)
| ssSkC0 ),
file('theBenchmark.p',clause24) ).
cnf(clause25,negated_conjecture,
( in(skc14,skc15)
| ssSkC0 ),
file('theBenchmark.p',clause25) ).
cnf(clause26,negated_conjecture,
( barrel(skc10,skc9)
| ~ ssSkC0 ),
file('theBenchmark.p',clause26) ).
cnf(clause27,negated_conjecture,
( down(skc10,skc8)
| ~ ssSkC0 ),
file('theBenchmark.p',clause27) ).
cnf(clause28,negated_conjecture,
( in(skc10,skc11)
| ~ ssSkC0 ),
file('theBenchmark.p',clause28) ).
cnf(clause29,negated_conjecture,
( ssSkC0
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,U)
| ~ barrel(W,V)
| ~ event(W)
| ~ chevy(V)
| ~ car(V)
| ~ white(V)
| ~ dirty(V)
| ~ old(V)
| ~ lonely(U)
| ~ way(U)
| ~ street(U) ),
file('theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( ~ ssSkC0
| ~ hollywood(X)
| ~ city(X)
| ~ in(W,X)
| ~ down(W,V)
| ~ barrel(W,U)
| ~ event(W)
| ~ street(V)
| ~ way(V)
| ~ lonely(V)
| ~ old(U)
| ~ dirty(U)
| ~ white(U)
| ~ car(U)
| ~ chevy(U) ),
file('theBenchmark.p',clause30) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP001-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a CNF_UNS_EPR_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/16.19 % Computer : n008.cluster.edu
% 0.09/16.19 % Model : x86_64 x86_64
% 0.09/16.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/16.19 % Memory : 8046.5625MB
% 0.09/16.19 % OS : Linux 6.8.0-71-generic
% 0.09/16.19 % CPULimit : 300
% 0.09/16.19 % WCLimit : 300
% 0.09/16.19 % DateTime : Sat Sep 19 16:27:31 UTC 2026
% 0.12/16.20 % CPUTime :
% 0.12/16.23 % SZS status Unsatisfiable for theBenchmark
% 0.12/16.23 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------