%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ018-1 : TPTP v9.3.1. Bugfixed v1.2.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 : n002.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:18 AM UTC 2026
% Result : Unsatisfiable 8.35s 8.62s
% Output : Proof 8.35s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(all_on_a_on,axiom,
( on(a,X)
| ~ all_on(X) ),
file('theBenchmark.p',all_on_a_on) ).
cnf(all_on_b_on,axiom,
( on(b,X)
| ~ all_on(X) ),
file('theBenchmark.p',all_on_b_on) ).
cnf(all_on_c_on,axiom,
( on(c,X)
| ~ all_on(X) ),
file('theBenchmark.p',all_on_c_on) ).
cnf(all_on,axiom,
( ~ on(c,X)
| ~ on(b,X)
| ~ on(a,X)
| all_on(X) ),
file('theBenchmark.p',all_on) ).
cnf(all_on_well_defined,axiom,
( same_day(X,Y)
| ~ all_on(Y)
| ~ all_on(X) ),
file('theBenchmark.p',all_on_well_defined) ).
cnf(monday_follows_sunday,axiom,
consecutive(sunday,monday),
file('theBenchmark.p',monday_follows_sunday) ).
cnf(tuesday_follows_monday,axiom,
consecutive(monday,tuesday),
file('theBenchmark.p',tuesday_follows_monday) ).
cnf(wednesday_follows_tuesday,axiom,
consecutive(tuesday,wednesday),
file('theBenchmark.p',wednesday_follows_tuesday) ).
cnf(thursday_follows_wednesday,axiom,
consecutive(wednesday,thursday),
file('theBenchmark.p',thursday_follows_wednesday) ).
cnf(friday_follows_thursday,axiom,
consecutive(thursday,friday),
file('theBenchmark.p',friday_follows_thursday) ).
cnf(staurday_follows_friday,axiom,
consecutive(friday,saturday),
file('theBenchmark.p',staurday_follows_friday) ).
cnf(sunday_follows_saturday,axiom,
consecutive(saturday,sunday),
file('theBenchmark.p',sunday_follows_saturday) ).
cnf(reflexivity_for_same_person,axiom,
same_person(X,X),
file('theBenchmark.p',reflexivity_for_same_person) ).
cnf(a_not_b,axiom,
~ same_person(a,b),
file('theBenchmark.p',a_not_b) ).
cnf(a_not_c,axiom,
~ same_person(a,c),
file('theBenchmark.p',a_not_c) ).
cnf(b_not_c,axiom,
~ same_person(b,c),
file('theBenchmark.p',b_not_c) ).
cnf(reflexivity_for_same_day,axiom,
same_day(X,X),
file('theBenchmark.p',reflexivity_for_same_day) ).
cnf(sunday_not_monday,axiom,
~ same_day(sunday,monday),
file('theBenchmark.p',sunday_not_monday) ).
cnf(sunday_not_tuesday,axiom,
~ same_day(sunday,tuesday),
file('theBenchmark.p',sunday_not_tuesday) ).
cnf(sunday_not_wednesday,axiom,
~ same_day(sunday,wednesday),
file('theBenchmark.p',sunday_not_wednesday) ).
cnf(sunday_not_thursday,axiom,
~ same_day(sunday,thursday),
file('theBenchmark.p',sunday_not_thursday) ).
cnf(sunday_not_friday,axiom,
~ same_day(sunday,friday),
file('theBenchmark.p',sunday_not_friday) ).
cnf(sunday_not_saturday,axiom,
~ same_day(sunday,saturday),
file('theBenchmark.p',sunday_not_saturday) ).
cnf(monday_not_tuesday,axiom,
~ same_day(monday,tuesday),
file('theBenchmark.p',monday_not_tuesday) ).
cnf(monday_not_wednesday,axiom,
~ same_day(monday,wednesday),
file('theBenchmark.p',monday_not_wednesday) ).
cnf(monday_not_thursday,axiom,
~ same_day(monday,thursday),
file('theBenchmark.p',monday_not_thursday) ).
cnf(monday_not_friday,axiom,
~ same_day(monday,friday),
file('theBenchmark.p',monday_not_friday) ).
cnf(monday_not_saturday,axiom,
~ same_day(monday,saturday),
file('theBenchmark.p',monday_not_saturday) ).
cnf(tuesday_not_wednesday,axiom,
~ same_day(tuesday,wednesday),
file('theBenchmark.p',tuesday_not_wednesday) ).
cnf(tuesday_not_thursday,axiom,
~ same_day(tuesday,thursday),
file('theBenchmark.p',tuesday_not_thursday) ).
cnf(tuesday_not_friday,axiom,
~ same_day(tuesday,friday),
file('theBenchmark.p',tuesday_not_friday) ).
cnf(tuesday_not_saturday,axiom,
~ same_day(tuesday,saturday),
file('theBenchmark.p',tuesday_not_saturday) ).
cnf(wednesday_not_thursday,axiom,
~ same_day(wednesday,thursday),
file('theBenchmark.p',wednesday_not_thursday) ).
cnf(wednesday_not_friday,axiom,
~ same_day(wednesday,friday),
file('theBenchmark.p',wednesday_not_friday) ).
cnf(wednesday_not_saturday,axiom,
~ same_day(wednesday,saturday),
file('theBenchmark.p',wednesday_not_saturday) ).
cnf(thursday_not_friday,axiom,
~ same_day(thursday,friday),
file('theBenchmark.p',thursday_not_friday) ).
cnf(thursday_not_saturday,axiom,
~ same_day(thursday,saturday),
file('theBenchmark.p',thursday_not_saturday) ).
cnf(friday_not_saturday,axiom,
~ same_day(friday,saturday),
file('theBenchmark.p',friday_not_saturday) ).
cnf(all_on_one_day,hypothesis,
( all_on(saturday)
| all_on(friday)
| all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
file('theBenchmark.p',all_on_one_day) ).
cnf(not_on_for_3_days,hypothesis,
( ~ on(U,Z)
| ~ on(U,Y)
| ~ on(U,X)
| ~ consecutive(Z,W)
| ~ consecutive(Y,Z)
| ~ consecutive(X,Y) ),
file('theBenchmark.p',not_on_for_3_days) ).
cnf(no_two_off_twice_together,hypothesis,
( same_day(Y,Z)
| same_person(X,W)
| on(W,Z)
| on(W,Y)
| on(X,Z)
| on(X,Y) ),
file('theBenchmark.p',no_two_off_twice_together) ).
cnf(a_off_sunday,hypothesis,
~ on(a,sunday),
file('theBenchmark.p',a_off_sunday) ).
cnf(a_off_tuesday,hypothesis,
~ on(a,tuesday),
file('theBenchmark.p',a_off_tuesday) ).
cnf(a_off_thursday,hypothesis,
~ on(a,thursday),
file('theBenchmark.p',a_off_thursday) ).
cnf(b_off_thursday,hypothesis,
~ on(b,thursday),
file('theBenchmark.p',b_off_thursday) ).
cnf(b_off_saturday,hypothesis,
~ on(b,saturday),
file('theBenchmark.p',b_off_saturday) ).
cnf(c_off_sunday,hypothesis,
~ on(c,sunday),
file('theBenchmark.p',c_off_sunday) ).
cnf(prove_all_on_friday,negated_conjecture,
~ all_on(friday),
file('theBenchmark.p',prove_all_on_friday) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ018-1 : TPTP v9.3.1. Bugfixed v1.2.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.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 19 19:58:15 UTC 2026
% 0.09/0.37 % CPUTime :
% 8.35/8.62 % SZS status Unsatisfiable for theBenchmark
% 8.35/8.62 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------