%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ005-1 : TPTP v9.3.1. Released v1.0.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 : n026.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:16 AM UTC 2026
% Result : Unsatisfiable 0.38s 0.64s
% Output : Proof 0.38s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(it_is_a_day,axiom,
( sunday(X)
| saturday(X)
| friday(X)
| thursday(X)
| wednesday(X)
| tuesday(X)
| monday(X) ),
file('theBenchmark.p',it_is_a_day) ).
cnf(monday_not_tuesday,axiom,
( ~ tuesday(X)
| ~ monday(X) ),
file('theBenchmark.p',monday_not_tuesday) ).
cnf(monday_not_wednesday,axiom,
( ~ wednesday(X)
| ~ monday(X) ),
file('theBenchmark.p',monday_not_wednesday) ).
cnf(monday_not_thursday,axiom,
( ~ thursday(X)
| ~ monday(X) ),
file('theBenchmark.p',monday_not_thursday) ).
cnf(monday_not_friday,axiom,
( ~ friday(X)
| ~ monday(X) ),
file('theBenchmark.p',monday_not_friday) ).
cnf(monday_not_saturday,axiom,
( ~ saturday(X)
| ~ monday(X) ),
file('theBenchmark.p',monday_not_saturday) ).
cnf(monday_not_sunday,axiom,
( ~ sunday(X)
| ~ monday(X) ),
file('theBenchmark.p',monday_not_sunday) ).
cnf(tuesday_not_wednesday,axiom,
( ~ wednesday(X)
| ~ tuesday(X) ),
file('theBenchmark.p',tuesday_not_wednesday) ).
cnf(tuesday_not_thursday,axiom,
( ~ thursday(X)
| ~ tuesday(X) ),
file('theBenchmark.p',tuesday_not_thursday) ).
cnf(tuesday_not_friday,axiom,
( ~ friday(X)
| ~ tuesday(X) ),
file('theBenchmark.p',tuesday_not_friday) ).
cnf(tuesday_not_saturday,axiom,
( ~ saturday(X)
| ~ tuesday(X) ),
file('theBenchmark.p',tuesday_not_saturday) ).
cnf(tuesday_not_sunday,axiom,
( ~ sunday(X)
| ~ tuesday(X) ),
file('theBenchmark.p',tuesday_not_sunday) ).
cnf(wednesday_not_thursday,axiom,
( ~ thursday(X)
| ~ wednesday(X) ),
file('theBenchmark.p',wednesday_not_thursday) ).
cnf(wednesday_not_friday,axiom,
( ~ friday(X)
| ~ wednesday(X) ),
file('theBenchmark.p',wednesday_not_friday) ).
cnf(wednesday_not_saturday,axiom,
( ~ saturday(X)
| ~ wednesday(X) ),
file('theBenchmark.p',wednesday_not_saturday) ).
cnf(wednesday_not_sunday,axiom,
( ~ sunday(X)
| ~ wednesday(X) ),
file('theBenchmark.p',wednesday_not_sunday) ).
cnf(thursday_not_friday,axiom,
( ~ friday(X)
| ~ thursday(X) ),
file('theBenchmark.p',thursday_not_friday) ).
cnf(thursday_not_saturday,axiom,
( ~ saturday(X)
| ~ thursday(X) ),
file('theBenchmark.p',thursday_not_saturday) ).
cnf(thursday_not_sunday,axiom,
( ~ sunday(X)
| ~ thursday(X) ),
file('theBenchmark.p',thursday_not_sunday) ).
cnf(friday_not_saturday,axiom,
( ~ saturday(X)
| ~ friday(X) ),
file('theBenchmark.p',friday_not_saturday) ).
cnf(friday_not_sunday,axiom,
( ~ sunday(X)
| ~ friday(X) ),
file('theBenchmark.p',friday_not_sunday) ).
cnf(saturday_not_sunday,axiom,
( ~ sunday(X)
| ~ saturday(X) ),
file('theBenchmark.p',saturday_not_sunday) ).
cnf(monday_yesterday,axiom,
( tuesday(X)
| ~ monday(yesterday(X)) ),
file('theBenchmark.p',monday_yesterday) ).
cnf(tuesday_yesterday,axiom,
( wednesday(X)
| ~ tuesday(yesterday(X)) ),
file('theBenchmark.p',tuesday_yesterday) ).
cnf(wednesday_yesterday,axiom,
( thursday(X)
| ~ wednesday(yesterday(X)) ),
file('theBenchmark.p',wednesday_yesterday) ).
cnf(thursday_yesterday,axiom,
( friday(X)
| ~ thursday(yesterday(X)) ),
file('theBenchmark.p',thursday_yesterday) ).
cnf(friday_yesterday,axiom,
( saturday(X)
| ~ friday(yesterday(X)) ),
file('theBenchmark.p',friday_yesterday) ).
cnf(saturday_yesterday,axiom,
( sunday(X)
| ~ saturday(yesterday(X)) ),
file('theBenchmark.p',saturday_yesterday) ).
cnf(sunday_yesterday,axiom,
( monday(X)
| ~ sunday(yesterday(X)) ),
file('theBenchmark.p',sunday_yesterday) ).
cnf(yesterday_monday,axiom,
( ~ tuesday(X)
| monday(yesterday(X)) ),
file('theBenchmark.p',yesterday_monday) ).
cnf(yesterday_tuesday,axiom,
( ~ wednesday(X)
| tuesday(yesterday(X)) ),
file('theBenchmark.p',yesterday_tuesday) ).
cnf(yesterday_wednesday,axiom,
( ~ thursday(X)
| wednesday(yesterday(X)) ),
file('theBenchmark.p',yesterday_wednesday) ).
cnf(yesterday_thursday,axiom,
( ~ friday(X)
| thursday(yesterday(X)) ),
file('theBenchmark.p',yesterday_thursday) ).
cnf(yesterday_friday,axiom,
( ~ saturday(X)
| friday(yesterday(X)) ),
file('theBenchmark.p',yesterday_friday) ).
cnf(yesterday_saturday,axiom,
( ~ sunday(X)
| saturday(yesterday(X)) ),
file('theBenchmark.p',yesterday_saturday) ).
cnf(yesterday_sunday,axiom,
( ~ monday(X)
| sunday(yesterday(X)) ),
file('theBenchmark.p',yesterday_sunday) ).
cnf(lions_lying_days,axiom,
( wednesday(X)
| tuesday(X)
| monday(X)
| ~ member(X,lying_days(lion)) ),
file('theBenchmark.p',lions_lying_days) ).
cnf(unicorns_lying_days,axiom,
( saturday(X)
| friday(X)
| thursday(X)
| ~ member(X,lying_days(unicorn)) ),
file('theBenchmark.p',unicorns_lying_days) ).
cnf(lion_lies_on_monday,axiom,
( member(X,lying_days(lion))
| ~ monday(X) ),
file('theBenchmark.p',lion_lies_on_monday) ).
cnf(lion_lies_on_tuesday,axiom,
( member(X,lying_days(lion))
| ~ tuesday(X) ),
file('theBenchmark.p',lion_lies_on_tuesday) ).
cnf(lion_lies_on_wednesday,axiom,
( member(X,lying_days(lion))
| ~ wednesday(X) ),
file('theBenchmark.p',lion_lies_on_wednesday) ).
cnf(unicorn_lies_on_thursday,axiom,
( member(X,lying_days(unicorn))
| ~ thursday(X) ),
file('theBenchmark.p',unicorn_lies_on_thursday) ).
cnf(unicorn_lies_on_friday,axiom,
( member(X,lying_days(unicorn))
| ~ friday(X) ),
file('theBenchmark.p',unicorn_lies_on_friday) ).
cnf(unicorn_lies_on_saturday,axiom,
( member(X,lying_days(unicorn))
| ~ saturday(X) ),
file('theBenchmark.p',unicorn_lies_on_saturday) ).
cnf(admissions1,axiom,
( member(Y,lying_days(T))
| ~ admits(T,X,Y)
| member(X,lying_days(T)) ),
file('theBenchmark.p',admissions1) ).
cnf(admissions2,axiom,
( ~ member(Y,lying_days(T))
| admits(T,X,Y)
| member(X,lying_days(T)) ),
file('theBenchmark.p',admissions2) ).
cnf(admissions3,axiom,
( ~ member(Y,lying_days(T))
| ~ admits(T,X,Y)
| ~ member(X,lying_days(T)) ),
file('theBenchmark.p',admissions3) ).
cnf(admissions4,axiom,
( member(Y,lying_days(T))
| admits(T,X,Y)
| ~ member(X,lying_days(T)) ),
file('theBenchmark.p',admissions4) ).
cnf(admissions5,axiom,
admits(lion,today,yesterday(today)),
file('theBenchmark.p',admissions5) ).
cnf(admissions6,axiom,
admits(unicorn,today,yesterday(today)),
file('theBenchmark.p',admissions6) ).
cnf(prove_today_is_thursday,negated_conjecture,
~ thursday(today),
file('theBenchmark.p',prove_today_is_thursday) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ005-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 This is a CNF_UNS_RFO_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/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 19 19:57:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.38/0.64 % SZS status Unsatisfiable for theBenchmark
% 0.38/0.64 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------