%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ028-5 : 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 : n012.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 12.90s 24.05s
% Output : Proof 12.90s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(person1,axiom,
person(one),
file('theBenchmark.p',person1) ).
cnf(person2,axiom,
person(two),
file('theBenchmark.p',person2) ).
cnf(person3,axiom,
person(three),
file('theBenchmark.p',person3) ).
cnf(person4,axiom,
person(four),
file('theBenchmark.p',person4) ).
cnf(person5,axiom,
person(five),
file('theBenchmark.p',person5) ).
cnf(person6,axiom,
person(six),
file('theBenchmark.p',person6) ).
cnf(order1,axiom,
after(one,two),
file('theBenchmark.p',order1) ).
cnf(order2,axiom,
after(two,three),
file('theBenchmark.p',order2) ).
cnf(order3,axiom,
after(three,four),
file('theBenchmark.p',order3) ).
cnf(order4,axiom,
after(four,five),
file('theBenchmark.p',order4) ).
cnf(order5,axiom,
after(five,six),
file('theBenchmark.p',order5) ).
cnf(transitivity_of_order,axiom,
( ~ after(Medium,Small)
| ~ after(Large,Medium)
| after(Large,Small) ),
file('theBenchmark.p',transitivity_of_order) ).
cnf(familiar_or_not,axiom,
( ~ after(X,Y)
| ~ person(Y)
| ~ person(X)
| not_familiar(X,Y)
| familiar(X,Y) ),
file('theBenchmark.p',familiar_or_not) ).
cnf(three_familiar,negated_conjecture,
( ~ familiar(X1,X3)
| ~ familiar(X2,X3)
| ~ familiar(X1,X2) ),
file('theBenchmark.p',three_familiar) ).
cnf(three_not_familiar,negated_conjecture,
( ~ not_familiar(X1,X3)
| ~ 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.01 % Problem : PUZ028-5 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.01 This is a CNF_UNS_EPR_NEQ_NHN problem
% 0.00/0.02 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/11.15 % Computer : n012.cluster.edu
% 0.04/11.15 % Model : x86_64 x86_64
% 0.04/11.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/11.15 % Memory : 8046.5625MB
% 0.04/11.15 % OS : Linux 6.8.0-71-generic
% 0.04/11.15 % CPULimit : 300
% 0.04/11.15 % WCLimit : 300
% 0.04/11.15 % DateTime : Sat Sep 19 19:57:25 UTC 2026
% 0.04/11.16 % CPUTime :
% 12.90/24.05 % SZS status Unsatisfiable for theBenchmark
% 12.90/24.05 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------