%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ028-6 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:54:20 AM UTC 2026
% Result : Unsatisfiable 6.64s 21.98s
% Output : Proof 6.64s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(person_1,axiom,
person(n1),
file('theBenchmark.p',person_1) ).
cnf(person_2,axiom,
person(n2),
file('theBenchmark.p',person_2) ).
cnf(person_3,axiom,
person(n3),
file('theBenchmark.p',person_3) ).
cnf(person_4,axiom,
person(n4),
file('theBenchmark.p',person_4) ).
cnf(person_5,axiom,
person(n5),
file('theBenchmark.p',person_5) ).
cnf(person_6,axiom,
person(n6),
file('theBenchmark.p',person_6) ).
cnf(not_equal_1_2,axiom,
not_equal(n1,n2),
file('theBenchmark.p',not_equal_1_2) ).
cnf(not_equal_1_3,axiom,
not_equal(n1,n3),
file('theBenchmark.p',not_equal_1_3) ).
cnf(not_equal_1_4,axiom,
not_equal(n1,n4),
file('theBenchmark.p',not_equal_1_4) ).
cnf(not_equal_1_5,axiom,
not_equal(n1,n5),
file('theBenchmark.p',not_equal_1_5) ).
cnf(not_equal_1_6,axiom,
not_equal(n1,n6),
file('theBenchmark.p',not_equal_1_6) ).
cnf(not_equal_2_1,axiom,
not_equal(n2,n1),
file('theBenchmark.p',not_equal_2_1) ).
cnf(not_equal_2_3,axiom,
not_equal(n2,n3),
file('theBenchmark.p',not_equal_2_3) ).
cnf(not_equal_2_4,axiom,
not_equal(n2,n4),
file('theBenchmark.p',not_equal_2_4) ).
cnf(not_equal_2_5,axiom,
not_equal(n2,n5),
file('theBenchmark.p',not_equal_2_5) ).
cnf(not_equal_2_6,axiom,
not_equal(n2,n6),
file('theBenchmark.p',not_equal_2_6) ).
cnf(not_equal_3_1,axiom,
not_equal(n3,n1),
file('theBenchmark.p',not_equal_3_1) ).
cnf(not_equal_3_2,axiom,
not_equal(n3,n2),
file('theBenchmark.p',not_equal_3_2) ).
cnf(not_equal_3_4,axiom,
not_equal(n3,n4),
file('theBenchmark.p',not_equal_3_4) ).
cnf(not_equal_3_5,axiom,
not_equal(n3,n5),
file('theBenchmark.p',not_equal_3_5) ).
cnf(not_equal_3_6,axiom,
not_equal(n3,n6),
file('theBenchmark.p',not_equal_3_6) ).
cnf(not_equal_4_1,axiom,
not_equal(n4,n1),
file('theBenchmark.p',not_equal_4_1) ).
cnf(not_equal_4_2,axiom,
not_equal(n4,n2),
file('theBenchmark.p',not_equal_4_2) ).
cnf(not_equal_4_3,axiom,
not_equal(n4,n3),
file('theBenchmark.p',not_equal_4_3) ).
cnf(not_equal_4_5,axiom,
not_equal(n4,n5),
file('theBenchmark.p',not_equal_4_5) ).
cnf(not_equal_4_6,axiom,
not_equal(n4,n6),
file('theBenchmark.p',not_equal_4_6) ).
cnf(not_equal_5_1,axiom,
not_equal(n5,n1),
file('theBenchmark.p',not_equal_5_1) ).
cnf(not_equal_5_2,axiom,
not_equal(n5,n2),
file('theBenchmark.p',not_equal_5_2) ).
cnf(not_equal_5_3,axiom,
not_equal(n5,n3),
file('theBenchmark.p',not_equal_5_3) ).
cnf(not_equal_5_4,axiom,
not_equal(n5,n4),
file('theBenchmark.p',not_equal_5_4) ).
cnf(not_equal_5_6,axiom,
not_equal(n5,n6),
file('theBenchmark.p',not_equal_5_6) ).
cnf(not_equal_6_1,axiom,
not_equal(n6,n1),
file('theBenchmark.p',not_equal_6_1) ).
cnf(not_equal_6_2,axiom,
not_equal(n6,n2),
file('theBenchmark.p',not_equal_6_2) ).
cnf(not_equal_6_3,axiom,
not_equal(n6,n3),
file('theBenchmark.p',not_equal_6_3) ).
cnf(not_equal_6_4,axiom,
not_equal(n6,n4),
file('theBenchmark.p',not_equal_6_4) ).
cnf(not_equal_6_5,axiom,
not_equal(n6,n5),
file('theBenchmark.p',not_equal_6_5) ).
cnf(familiar_or_not,axiom,
( ~ not_equal(X,Y)
| ~ person(Y)
| ~ person(X)
| not_familiar(X,Y)
| familiar(X,Y) ),
file('theBenchmark.p',familiar_or_not) ).
cnf(symmetry_of_familiar,axiom,
( familiar(X2,X1)
| ~ familiar(X1,X2) ),
file('theBenchmark.p',symmetry_of_familiar) ).
cnf(symmetry_of_not_familiar,axiom,
( not_familiar(X2,X1)
| ~ not_familiar(X1,X2) ),
file('theBenchmark.p',symmetry_of_not_familiar) ).
cnf(three_familiar,negated_conjecture,
( ~ familiar(X3,X1)
| ~ familiar(X2,X3)
| ~ familiar(X1,X2) ),
file('theBenchmark.p',three_familiar) ).
cnf(three_not_familiar,negated_conjecture,
( ~ not_familiar(X3,X1)
| ~ not_familiar(X2,X3)
| ~ not_familiar(X1,X2) ),
file('theBenchmark.p',three_not_familiar) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ028-6 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.03 This is a CNF_UNS_EPR_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/15.58 % CPULimit : 300
% 0.08/15.58 % WCLimit : 300
% 0.08/15.58 % DateTime : Sat Sep 19 19:57:37 UTC 2026
% 0.08/15.58 % CPUTime :
% 6.64/21.98 % SZS status Unsatisfiable for theBenchmark
% 6.64/21.98 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------