%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP004-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 : n010.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:51:00 AM UTC 2026
% Result : Unsatisfiable 1.04s 1.32s
% Output : Proof 1.04s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
hollywood(skc31),
file('theBenchmark.p',clause1) ).
cnf(clause2,negated_conjecture,
event(skc30),
file('theBenchmark.p',clause2) ).
cnf(clause3,negated_conjecture,
street(skc29),
file('theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
old(skc28),
file('theBenchmark.p',clause4) ).
cnf(clause5,negated_conjecture,
front(skc27),
file('theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
seat(skc26),
file('theBenchmark.p',clause6) ).
cnf(clause7,negated_conjecture,
fellow(skc25),
file('theBenchmark.p',clause7) ).
cnf(clause8,negated_conjecture,
young(skc24),
file('theBenchmark.p',clause8) ).
cnf(clause9,negated_conjecture,
hollywood(skc23),
file('theBenchmark.p',clause9) ).
cnf(clause10,negated_conjecture,
event(skc22),
file('theBenchmark.p',clause10) ).
cnf(clause11,negated_conjecture,
chevy(skc21),
file('theBenchmark.p',clause11) ).
cnf(clause12,negated_conjecture,
lonely(skc20),
file('theBenchmark.p',clause12) ).
cnf(clause13,negated_conjecture,
front(skc19),
file('theBenchmark.p',clause13) ).
cnf(clause14,negated_conjecture,
seat(skc18),
file('theBenchmark.p',clause14) ).
cnf(clause15,negated_conjecture,
fellow(skc17),
file('theBenchmark.p',clause15) ).
cnf(clause16,negated_conjecture,
young(skc16),
file('theBenchmark.p',clause16) ).
cnf(clause17,negated_conjecture,
( chevy(skc28)
| ssSkC0 ),
file('theBenchmark.p',clause17) ).
cnf(clause18,negated_conjecture,
( car(skc28)
| ssSkC0 ),
file('theBenchmark.p',clause18) ).
cnf(clause19,negated_conjecture,
( white(skc28)
| ssSkC0 ),
file('theBenchmark.p',clause19) ).
cnf(clause20,negated_conjecture,
( dirty(skc28)
| ssSkC0 ),
file('theBenchmark.p',clause20) ).
cnf(clause21,negated_conjecture,
( lonely(skc29)
| ssSkC0 ),
file('theBenchmark.p',clause21) ).
cnf(clause22,negated_conjecture,
( way(skc29)
| ssSkC0 ),
file('theBenchmark.p',clause22) ).
cnf(clause23,negated_conjecture,
( city(skc31)
| ssSkC0 ),
file('theBenchmark.p',clause23) ).
cnf(clause24,negated_conjecture,
( seat(skc27)
| ssSkC0 ),
file('theBenchmark.p',clause24) ).
cnf(clause25,negated_conjecture,
( furniture(skc27)
| ssSkC0 ),
file('theBenchmark.p',clause25) ).
cnf(clause26,negated_conjecture,
( fellow(skc24)
| ssSkC0 ),
file('theBenchmark.p',clause26) ).
cnf(clause27,negated_conjecture,
( man(skc24)
| ssSkC0 ),
file('theBenchmark.p',clause27) ).
cnf(clause28,negated_conjecture,
( front(skc26)
| ssSkC0 ),
file('theBenchmark.p',clause28) ).
cnf(clause29,negated_conjecture,
( furniture(skc26)
| ssSkC0 ),
file('theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( young(skc25)
| ssSkC0 ),
file('theBenchmark.p',clause30) ).
cnf(clause31,negated_conjecture,
( man(skc25)
| ssSkC0 ),
file('theBenchmark.p',clause31) ).
cnf(clause32,negated_conjecture,
( street(skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause32) ).
cnf(clause33,negated_conjecture,
( way(skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause33) ).
cnf(clause34,negated_conjecture,
( old(skc21)
| ~ ssSkC0 ),
file('theBenchmark.p',clause34) ).
cnf(clause35,negated_conjecture,
( dirty(skc21)
| ~ ssSkC0 ),
file('theBenchmark.p',clause35) ).
cnf(clause36,negated_conjecture,
( white(skc21)
| ~ ssSkC0 ),
file('theBenchmark.p',clause36) ).
cnf(clause37,negated_conjecture,
( car(skc21)
| ~ ssSkC0 ),
file('theBenchmark.p',clause37) ).
cnf(clause38,negated_conjecture,
( city(skc23)
| ~ ssSkC0 ),
file('theBenchmark.p',clause38) ).
cnf(clause39,negated_conjecture,
( seat(skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause39) ).
cnf(clause40,negated_conjecture,
( furniture(skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause40) ).
cnf(clause41,negated_conjecture,
( fellow(skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause41) ).
cnf(clause42,negated_conjecture,
( man(skc16)
| ~ ssSkC0 ),
file('theBenchmark.p',clause42) ).
cnf(clause43,negated_conjecture,
( front(skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause43) ).
cnf(clause44,negated_conjecture,
( furniture(skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause44) ).
cnf(clause45,negated_conjecture,
( young(skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause45) ).
cnf(clause46,negated_conjecture,
( man(skc17)
| ~ ssSkC0 ),
file('theBenchmark.p',clause46) ).
cnf(clause47,negated_conjecture,
( barrel(skc30,skc28)
| ssSkC0 ),
file('theBenchmark.p',clause47) ).
cnf(clause48,negated_conjecture,
( down(skc30,skc29)
| ssSkC0 ),
file('theBenchmark.p',clause48) ).
cnf(clause49,negated_conjecture,
( in(skc30,skc31)
| ssSkC0 ),
file('theBenchmark.p',clause49) ).
cnf(clause50,negated_conjecture,
( in(skc24,skc27)
| ssSkC0 ),
file('theBenchmark.p',clause50) ).
cnf(clause51,negated_conjecture,
( in(skc25,skc26)
| ssSkC0 ),
file('theBenchmark.p',clause51) ).
cnf(clause52,negated_conjecture,
( barrel(skc22,skc21)
| ~ ssSkC0 ),
file('theBenchmark.p',clause52) ).
cnf(clause53,negated_conjecture,
( down(skc22,skc20)
| ~ ssSkC0 ),
file('theBenchmark.p',clause53) ).
cnf(clause54,negated_conjecture,
( in(skc22,skc23)
| ~ ssSkC0 ),
file('theBenchmark.p',clause54) ).
cnf(clause55,negated_conjecture,
( in(skc16,skc19)
| ~ ssSkC0 ),
file('theBenchmark.p',clause55) ).
cnf(clause56,negated_conjecture,
( in(skc17,skc18)
| ~ ssSkC0 ),
file('theBenchmark.p',clause56) ).
cnf(clause57,negated_conjecture,
( ssSkC0
| skc25 != skc24 ),
file('theBenchmark.p',clause57) ).
cnf(clause58,negated_conjecture,
( ~ ssSkC0
| skc17 != skc16 ),
file('theBenchmark.p',clause58) ).
cnf(clause59,negated_conjecture,
( X1 = Z
| ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ in(Z,Y)
| ~ front(Y)
| ~ furniture(Y)
| ~ seat(Y)
| ~ 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',clause59) ).
cnf(clause60,negated_conjecture,
( X1 = Z
| ~ ssSkC0
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ furniture(X2)
| ~ front(X2)
| ~ in(X1,X2)
| ~ young(Z)
| ~ man(Z)
| ~ fellow(Z)
| ~ in(Z,Y)
| ~ front(Y)
| ~ furniture(Y)
| ~ seat(Y)
| ~ 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',clause60) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( hollywood(Eq_y_0)
| ~ hollywood(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_5,axiom,
( event(Eq_y_0)
| ~ event(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_6,axiom,
( street(Eq_y_0)
| ~ street(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_7,axiom,
( old(Eq_y_0)
| ~ old(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_8,axiom,
( front(Eq_y_0)
| ~ front(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_9,axiom,
( seat(Eq_y_0)
| ~ seat(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( fellow(Eq_y_0)
| ~ fellow(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( young(Eq_y_0)
| ~ young(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( chevy(Eq_y_0)
| ~ chevy(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( lonely(Eq_y_0)
| ~ lonely(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( car(Eq_y_0)
| ~ car(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( white(Eq_y_0)
| ~ white(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( dirty(Eq_y_0)
| ~ dirty(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( way(Eq_y_0)
| ~ way(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( city(Eq_y_0)
| ~ city(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( furniture(Eq_y_0)
| ~ furniture(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( man(Eq_y_0)
| ~ man(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( barrel(Eq_y_0,Eq_y_1)
| ~ barrel(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( down(Eq_y_0,Eq_y_1)
| ~ down(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( in(Eq_y_0,Eq_y_1)
| ~ in(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP004-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a CNF_UNS_EPR_SEQ_NHN problem
% 0.00/0.03 % 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/0.35 % Computer : n010.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 19 16:27:55 UTC 2026
% 0.09/0.35 % CPUTime :
% 1.04/1.32 % SZS status Unsatisfiable for theBenchmark
% 1.04/1.32 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------