%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 : Sun Sep 27 08:23:17 AM UTC 2026
% Result : Theorem 0.14s 11.01s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 21
% Syntax : Number of formulae : 196 ( 68 unt; 0 def)
% Number of atoms : 520 ( 343 equ)
% Maximal formula atoms : 21 ( 2 avg)
% Number of connectives : 425 ( 101 ~; 288 |; 25 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-1 aty)
% Number of variables : 50 ( 0 sgn 12 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(days_of_week,axiom,
! [X] :
( X = sunday
| X = saturday
| X = friday
| X = thursday
| X = wednesday
| X = tuesday
| X = monday ),
file('theBenchmark.p',days_of_week) ).
fof(uniquenames,axiom,
( saturday != sunday
& friday != sunday
& friday != saturday
& thursday != sunday
& thursday != saturday
& thursday != friday
& wednesday != sunday
& wednesday != saturday
& wednesday != friday
& wednesday != thursday
& tuesday != sunday
& tuesday != saturday
& tuesday != friday
& tuesday != thursday
& tuesday != wednesday
& monday != sunday
& monday != saturday
& monday != friday
& monday != thursday
& monday != wednesday
& monday != tuesday ),
file('theBenchmark.p',uniquenames) ).
fof(truth_unique,axiom,
! [X,Y] :
( ( truthday(Y)
& truthday(X) )
=> X = Y ),
file('theBenchmark.p',truth_unique) ).
fof(day2_unique,axiom,
! [X,Y] :
( ( day2(Y)
& day2(X) )
=> X = Y ),
file('theBenchmark.p',day2_unique) ).
fof(day3_unique,axiom,
! [X,Y] :
( ( day3(Y)
& day3(X) )
=> X = Y ),
file('theBenchmark.p',day3_unique) ).
fof(truth_once,axiom,
? [X] : truthday(X),
file('theBenchmark.p',truth_once) ).
fof(day1_once,axiom,
? [X] : day1(X),
file('theBenchmark.p',day1_once) ).
fof(day2_once,axiom,
? [X] : day2(X),
file('theBenchmark.p',day2_once) ).
fof(day3_once,axiom,
? [X] : day3(X),
file('theBenchmark.p',day3_once) ).
fof(day2_follows_day1,axiom,
! [X] :
( day1(X)
<=> day2(consecutive(X)) ),
file('theBenchmark.p',day2_follows_day1) ).
fof(day3_follows_day2,axiom,
! [X] :
( day2(X)
<=> day3(consecutive(X)) ),
file('theBenchmark.p',day3_follows_day2) ).
fof(statement1,axiom,
! [X] :
( day1(X)
=> ( truthday(X)
<=> ( ~ truthday(tuesday)
& ~ truthday(monday) ) ) ),
file('theBenchmark.p',statement1) ).
fof(statement2,axiom,
! [X] :
( day2(X)
=> ( truthday(X)
<=> ( day2(sunday)
| day2(saturday)
| day2(thursday) ) ) ),
file('theBenchmark.p',statement2) ).
fof(statement3,axiom,
! [X] :
( day3(X)
=> ( truthday(X)
<=> ( ~ truthday(friday)
& ~ truthday(wednesday) ) ) ),
file('theBenchmark.p',statement3) ).
fof(tuesday_leo_tells_truths,conjecture,
truthday(tuesday),
file('theBenchmark.p',tuesday_leo_tells_truths) ).
fof(tuesday_leo_tells_truths_neg,negated_conjecture,
~ truthday(tuesday),
inference(assume_negation,[status(cth)],[tuesday_leo_tells_truths]) ).
cnf(c_17,plain,
( sunday = A
| saturday = A
| friday = A
| thursday = A
| wednesday = A
| tuesday = A
| monday = A ),
inference(clausify,[status(thm)],[days_of_week]) ).
cnf(c_19,plain,
wednesday != monday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_22,plain,
friday != monday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_23,plain,
monday != friday,
inference(copy,[status(thm)],[c_22]) ).
cnf(c_24,plain,
saturday != monday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_25,plain,
monday != saturday,
inference(copy,[status(thm)],[c_24]) ).
cnf(c_26,plain,
sunday != monday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_27,plain,
monday != sunday,
inference(copy,[status(thm)],[c_26]) ).
cnf(c_37,plain,
thursday != wednesday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_38,plain,
wednesday != thursday,
inference(copy,[status(thm)],[c_37]) ).
cnf(c_41,plain,
saturday != wednesday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_42,plain,
wednesday != saturday,
inference(copy,[status(thm)],[c_41]) ).
cnf(c_43,plain,
sunday != wednesday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_44,plain,
wednesday != sunday,
inference(copy,[status(thm)],[c_43]) ).
cnf(c_45,plain,
friday != thursday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_50,plain,
saturday != friday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_51,plain,
friday != saturday,
inference(copy,[status(thm)],[c_50]) ).
cnf(c_52,plain,
sunday != friday,
inference(clausify,[status(thm)],[uniquenames]) ).
cnf(c_53,plain,
friday != sunday,
inference(copy,[status(thm)],[c_52]) ).
cnf(c_55,plain,
( B = A
| ~ truthday(B)
| ~ truthday(A) ),
inference(clausify,[status(thm)],[truth_unique]) ).
cnf(c_57,plain,
( B = A
| ~ day2(B)
| ~ day2(A) ),
inference(clausify,[status(thm)],[day2_unique]) ).
cnf(c_58,plain,
( B = A
| ~ day3(B)
| ~ day3(A) ),
inference(clausify,[status(thm)],[day3_unique]) ).
fof(nnf_7,plain,
? [X] : truthday(X),
inference(fof_nnf,[status(thm)],[truth_once]) ).
fof(sk_truth_once,plain,
truthday(sK0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X,sK0)],[nnf_7]) ).
cnf(c_59,plain,
truthday(sK0),
inference(split_conjunct,[status(thm)],[sk_truth_once]) ).
fof(nnf_8,plain,
? [X] : day1(X),
inference(fof_nnf,[status(thm)],[day1_once]) ).
fof(sk_day1_once,plain,
day1(sK1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X,sK1)],[nnf_8]) ).
cnf(c_60,plain,
day1(sK1),
inference(split_conjunct,[status(thm)],[sk_day1_once]) ).
fof(nnf_9,plain,
? [X] : day2(X),
inference(fof_nnf,[status(thm)],[day2_once]) ).
fof(sk_day2_once,plain,
day2(sK2),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X,sK2)],[nnf_9]) ).
cnf(c_61,plain,
day2(sK2),
inference(split_conjunct,[status(thm)],[sk_day2_once]) ).
fof(nnf_10,plain,
? [X] : day3(X),
inference(fof_nnf,[status(thm)],[day3_once]) ).
fof(sk_day3_once,plain,
day3(sK3),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X,sK3)],[nnf_10]) ).
cnf(c_62,plain,
day3(sK3),
inference(split_conjunct,[status(thm)],[sk_day3_once]) ).
fof(monday_follows_sunday,axiom,
consecutive(sunday) = monday,
file('theBenchmark.p',monday_follows_sunday) ).
cnf(c_63,plain,
consecutive(sunday) = monday,
inference(clausify,[status(thm)],[monday_follows_sunday]) ).
fof(tuesday_follows_monday,axiom,
consecutive(monday) = tuesday,
file('theBenchmark.p',tuesday_follows_monday) ).
cnf(c_64,plain,
consecutive(monday) = tuesday,
inference(clausify,[status(thm)],[tuesday_follows_monday]) ).
fof(thursday_follows_wednesday,axiom,
consecutive(wednesday) = thursday,
file('theBenchmark.p',thursday_follows_wednesday) ).
cnf(c_66,plain,
consecutive(wednesday) = thursday,
inference(clausify,[status(thm)],[thursday_follows_wednesday]) ).
fof(friday_follows_thursday,axiom,
consecutive(thursday) = friday,
file('theBenchmark.p',friday_follows_thursday) ).
cnf(c_67,plain,
consecutive(thursday) = friday,
inference(clausify,[status(thm)],[friday_follows_thursday]) ).
fof(saturday_follows_friday,axiom,
consecutive(friday) = saturday,
file('theBenchmark.p',saturday_follows_friday) ).
cnf(c_68,plain,
consecutive(friday) = saturday,
inference(clausify,[status(thm)],[saturday_follows_friday]) ).
fof(sunday_follows_saturday,axiom,
consecutive(saturday) = sunday,
file('theBenchmark.p',sunday_follows_saturday) ).
cnf(c_69,plain,
consecutive(saturday) = sunday,
inference(clausify,[status(thm)],[sunday_follows_saturday]) ).
cnf(c_70,plain,
( day2(consecutive(A))
| ~ day1(A) ),
inference(clausify,[status(thm)],[day2_follows_day1]) ).
cnf(c_72,plain,
( day3(consecutive(A))
| ~ day2(A) ),
inference(clausify,[status(thm)],[day3_follows_day2]) ).
cnf(c_73,plain,
( ~ day3(consecutive(A))
| day2(A) ),
inference(clausify,[status(thm)],[day3_follows_day2]) ).
cnf(c_74,plain,
( ~ truthday(monday)
| ~ truthday(A)
| ~ day1(A) ),
inference(clausify,[status(thm)],[statement1]) ).
cnf(c_76,plain,
( truthday(tuesday)
| truthday(monday)
| truthday(A)
| ~ day1(A) ),
inference(clausify,[status(thm)],[statement1]) ).
cnf(c_78,plain,
( ~ day2(thursday)
| truthday(A)
| ~ day2(A) ),
inference(clausify,[status(thm)],[statement2]) ).
cnf(c_79,plain,
( ~ day2(saturday)
| truthday(A)
| ~ day2(A) ),
inference(clausify,[status(thm)],[statement2]) ).
cnf(c_80,plain,
( ~ day2(sunday)
| truthday(A)
| ~ day2(A) ),
inference(clausify,[status(thm)],[statement2]) ).
cnf(c_81,plain,
( ~ truthday(wednesday)
| ~ truthday(A)
| ~ day3(A) ),
inference(clausify,[status(thm)],[statement3]) ).
cnf(c_82,plain,
( ~ truthday(friday)
| ~ truthday(A)
| ~ day3(A) ),
inference(clausify,[status(thm)],[statement3]) ).
cnf(c_83,plain,
( truthday(friday)
| truthday(wednesday)
| truthday(A)
| ~ day3(A) ),
inference(clausify,[status(thm)],[statement3]) ).
cnf(c_84,negated_conjecture,
~ truthday(tuesday),
inference(clausify,[status(thm)],[tuesday_leo_tells_truths_neg]) ).
cnf(c_88,plain,
( truthday(thursday)
| ~ day2(thursday) ),
inference(factor,[status(thm)],[c_78]) ).
cnf(c_89,plain,
( truthday(saturday)
| ~ day2(saturday) ),
inference(factor,[status(thm)],[c_79]) ).
cnf(c_90,plain,
( truthday(sunday)
| ~ day2(sunday) ),
inference(factor,[status(thm)],[c_80]) ).
cnf(c_95,negated_conjecture,
( truthday(monday)
| truthday(A)
| ~ day1(A) ),
inference(resolve,[status(thm)],[c_84,c_76]) ).
cnf(c_97,plain,
( sK0 = A
| ~ truthday(A) ),
inference(resolve,[status(thm)],[c_59,c_55]) ).
cnf(c_101,plain,
( sK2 = A
| ~ day2(A) ),
inference(resolve,[status(thm)],[c_61,c_57]) ).
cnf(c_103,plain,
( sK3 = A
| ~ day3(A) ),
inference(resolve,[status(thm)],[c_62,c_58]) ).
cnf(c_105,plain,
( consecutive(A) = thursday
| sunday = A
| saturday = A
| friday = A
| thursday = A
| tuesday = A
| monday = A ),
inference(paramod,[status(thm)],[c_17,c_66]) ).
cnf(c_106,plain,
day2(consecutive(sK1)),
inference(resolve,[status(thm)],[c_70,c_60]) ).
cnf(c_115,plain,
day3(consecutive(sK2)),
inference(resolve,[status(thm)],[c_72,c_61]) ).
cnf(c_117,plain,
( ~ day3(monday)
| day2(sunday) ),
inference(paramod,[status(thm)],[c_63,c_73]) ).
cnf(c_124,plain,
( ~ truthday(monday)
| ~ truthday(sK1) ),
inference(resolve,[status(thm)],[c_74,c_60]) ).
cnf(c_129,plain,
( ~ truthday(wednesday)
| ~ truthday(sK3) ),
inference(resolve,[status(thm)],[c_81,c_62]) ).
cnf(c_130,plain,
( ~ truthday(friday)
| ~ truthday(sK3) ),
inference(resolve,[status(thm)],[c_82,c_62]) ).
cnf(c_131,plain,
( truthday(friday)
| truthday(wednesday)
| truthday(sK3) ),
inference(resolve,[status(thm)],[c_83,c_62]) ).
cnf(c_134,plain,
( truthday(monday)
| truthday(sK1) ),
inference(resolve,[status(thm)],[c_95,c_60]) ).
cnf(c_640,plain,
( sK0 = sK1
| truthday(monday) ),
inference(resolve,[status(thm)],[c_134,c_97]) ).
cnf(c_174,plain,
( sK1 = sK0
| truthday(monday) ),
inference(copy,[status(thm)],[c_640]) ).
cnf(c_183,plain,
( monday = A
| ~ truthday(A)
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_174,c_55]) ).
cnf(c_641,plain,
( sK0 = sK3
| truthday(friday)
| truthday(wednesday) ),
inference(resolve,[status(thm)],[c_131,c_97]) ).
cnf(c_184,plain,
( sK3 = sK0
| truthday(friday)
| truthday(wednesday) ),
inference(copy,[status(thm)],[c_641]) ).
cnf(c_642,plain,
( sK1 = sK0
| A = monday
| ~ truthday(A) ),
inference(resolve,[status(thm)],[c_55,c_174]) ).
cnf(c_187,plain,
( truthday(friday)
| truthday(wednesday)
| sK1 = sK0
| sK3 = monday ),
inference(resolve,[status(thm)],[c_642,c_131]) ).
cnf(c_204,plain,
( sK0 = wednesday
| sK3 = sK0
| truthday(friday) ),
inference(resolve,[status(thm)],[c_184,c_97]) ).
cnf(c_206,plain,
( wednesday = A
| ~ truthday(A)
| sK3 = sK0
| truthday(friday) ),
inference(resolve,[status(thm)],[c_184,c_55]) ).
cnf(c_643,plain,
( sK1 = sK0
| A = monday
| ~ truthday(A) ),
inference(resolve,[status(thm)],[c_55,c_174]) ).
cnf(c_644,plain,
( sK3 = sK0
| truthday(friday)
| sK1 = sK0
| wednesday = monday ),
inference(resolve,[status(thm)],[c_643,c_184]) ).
cnf(c_208,plain,
( sK3 = sK0
| truthday(friday)
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_19,c_644]) ).
cnf(c_645,plain,
sK2 = consecutive(sK1),
inference(resolve,[status(thm)],[c_106,c_101]) ).
cnf(c_210,plain,
consecutive(sK1) = sK2,
inference(copy,[status(thm)],[c_645]) ).
cnf(c_646,plain,
sK3 = consecutive(sK2),
inference(resolve,[status(thm)],[c_115,c_103]) ).
cnf(c_213,plain,
consecutive(sK2) = sK3,
inference(copy,[status(thm)],[c_646]) ).
cnf(c_225,plain,
( sK0 = friday
| sK0 = wednesday
| sK3 = sK0 ),
inference(resolve,[status(thm)],[c_204,c_97]) ).
cnf(c_647,plain,
( monday = friday
| sK1 = sK0
| sK3 = sK0
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_208,c_183]) ).
cnf(c_648,plain,
( monday = friday
| sK3 = sK0
| sK1 = sK0 ),
inference(copy,[status(thm)],[c_647]) ).
cnf(c_228,plain,
( sK3 = sK0
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_23,c_648]) ).
cnf(c_649,plain,
( ~ truthday(wednesday)
| ~ truthday(sK0)
| sK1 = sK0 ),
inference(paramod,[status(thm)],[c_228,c_129]) ).
cnf(c_230,plain,
( ~ truthday(wednesday)
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_59,c_649]) ).
cnf(c_650,plain,
( ~ truthday(friday)
| ~ truthday(sK0)
| sK1 = sK0 ),
inference(paramod,[status(thm)],[c_228,c_130]) ).
cnf(c_231,plain,
( ~ truthday(friday)
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_59,c_650]) ).
cnf(c_651,plain,
( truthday(tuesday)
| consecutive(sK0) = thursday
| sunday = sK0
| saturday = sK0
| friday = sK0
| thursday = sK0
| monday = sK0 ),
inference(paramod,[status(thm)],[c_105,c_59]) ).
cnf(c_652,plain,
( truthday(tuesday)
| consecutive(sK0) = thursday
| sunday = sK0
| saturday = sK0
| friday = sK0
| thursday = sK0
| sK0 = monday ),
inference(copy,[status(thm)],[c_651]) ).
cnf(c_653,plain,
( truthday(tuesday)
| consecutive(sK0) = thursday
| sunday = sK0
| saturday = sK0
| friday = sK0
| sK0 = thursday
| sK0 = monday ),
inference(copy,[status(thm)],[c_652]) ).
cnf(c_654,plain,
( truthday(tuesday)
| consecutive(sK0) = thursday
| sunday = sK0
| saturday = sK0
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(copy,[status(thm)],[c_653]) ).
cnf(c_655,plain,
( truthday(tuesday)
| consecutive(sK0) = thursday
| sunday = sK0
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(copy,[status(thm)],[c_654]) ).
cnf(c_656,plain,
( truthday(tuesday)
| consecutive(sK0) = thursday
| sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(copy,[status(thm)],[c_655]) ).
cnf(c_259,negated_conjecture,
( consecutive(sK0) = thursday
| sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(resolve,[status(thm)],[c_84,c_656]) ).
cnf(c_657,plain,
( sK1 = sK0
| truthday(friday)
| sK1 = sK0
| sK3 = monday ),
inference(resolve,[status(thm)],[c_187,c_230]) ).
cnf(c_312,plain,
( truthday(friday)
| sK1 = sK0
| sK3 = monday ),
inference(copy,[status(thm)],[c_657]) ).
cnf(c_658,plain,
( sK1 = sK0
| sK1 = sK0
| sK3 = monday ),
inference(resolve,[status(thm)],[c_312,c_231]) ).
cnf(c_313,plain,
( sK1 = sK0
| sK3 = monday ),
inference(copy,[status(thm)],[c_658]) ).
cnf(c_314,plain,
( day3(monday)
| sK1 = sK0 ),
inference(paramod,[status(thm)],[c_313,c_62]) ).
cnf(c_317,plain,
( day2(sunday)
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_314,c_117]) ).
cnf(c_322,plain,
( truthday(sunday)
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_317,c_90]) ).
cnf(c_659,plain,
( monday = sunday
| sK1 = sK0
| sK1 = sK0 ),
inference(resolve,[status(thm)],[c_322,c_183]) ).
cnf(c_660,plain,
( monday = sunday
| sK1 = sK0 ),
inference(copy,[status(thm)],[c_659]) ).
cnf(c_333,plain,
sK1 = sK0,
inference(resolve,[status(thm)],[c_27,c_660]) ).
cnf(c_345,plain,
consecutive(sK0) = sK2,
inference(paramod,[status(thm)],[c_333,c_210]) ).
cnf(c_661,plain,
( ~ truthday(monday)
| ~ truthday(sK0) ),
inference(paramod,[status(thm)],[c_333,c_124]) ).
cnf(c_348,plain,
~ truthday(monday),
inference(resolve,[status(thm)],[c_59,c_661]) ).
cnf(c_350,plain,
day1(sK0),
inference(paramod,[status(thm)],[c_333,c_60]) ).
cnf(c_351,negated_conjecture,
( sK2 = thursday
| sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(paramod,[status(thm)],[c_345,c_259]) ).
cnf(c_387,plain,
( day2(thursday)
| sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(paramod,[status(thm)],[c_351,c_61]) ).
cnf(c_391,plain,
( truthday(thursday)
| sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(resolve,[status(thm)],[c_387,c_88]) ).
cnf(c_662,plain,
( sK0 = thursday
| sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(resolve,[status(thm)],[c_391,c_97]) ).
cnf(c_412,plain,
( sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday
| sK0 = monday ),
inference(copy,[status(thm)],[c_662]) ).
cnf(c_663,plain,
( truthday(monday)
| sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday ),
inference(paramod,[status(thm)],[c_412,c_59]) ).
cnf(c_413,plain,
( sK0 = sunday
| sK0 = saturday
| sK0 = friday
| sK0 = thursday ),
inference(resolve,[status(thm)],[c_348,c_663]) ).
cnf(c_416,plain,
( day1(friday)
| sK0 = sunday
| sK0 = saturday
| sK0 = thursday ),
inference(paramod,[status(thm)],[c_413,c_350]) ).
cnf(c_664,plain,
( day2(consecutive(friday))
| sK0 = sunday
| sK0 = saturday
| sK0 = thursday ),
inference(resolve,[status(thm)],[c_416,c_70]) ).
cnf(c_480,plain,
( day2(saturday)
| sK0 = sunday
| sK0 = saturday
| sK0 = thursday ),
inference(paramod,[status(thm)],[c_68,c_664]) ).
cnf(c_483,plain,
( truthday(saturday)
| sK0 = sunday
| sK0 = saturday
| sK0 = thursday ),
inference(resolve,[status(thm)],[c_480,c_89]) ).
cnf(c_665,plain,
( sK0 = saturday
| sK0 = sunday
| sK0 = saturday
| sK0 = thursday ),
inference(resolve,[status(thm)],[c_483,c_97]) ).
cnf(c_492,plain,
( sK0 = sunday
| sK0 = saturday
| sK0 = thursday ),
inference(copy,[status(thm)],[c_665]) ).
cnf(c_493,plain,
( truthday(thursday)
| sK0 = sunday
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_492,c_59]) ).
cnf(c_497,plain,
( day1(thursday)
| sK0 = sunday
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_492,c_350]) ).
cnf(c_666,plain,
( wednesday = thursday
| sK3 = sK0
| truthday(friday)
| sK0 = sunday
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_493,c_206]) ).
cnf(c_500,plain,
( sK3 = sK0
| truthday(friday)
| sK0 = sunday
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_38,c_666]) ).
cnf(c_667,plain,
( day2(consecutive(thursday))
| sK0 = sunday
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_497,c_70]) ).
cnf(c_542,plain,
( day2(friday)
| sK0 = sunday
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_67,c_667]) ).
cnf(c_668,plain,
( day3(consecutive(friday))
| sK0 = sunday
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_542,c_72]) ).
cnf(c_548,plain,
( day3(saturday)
| sK0 = sunday
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_68,c_668]) ).
cnf(c_550,plain,
( sK3 = saturday
| sK0 = sunday
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_548,c_103]) ).
cnf(c_669,plain,
( sK0 = sunday
| sK0 = saturday
| A = thursday
| ~ truthday(A) ),
inference(resolve,[status(thm)],[c_55,c_493]) ).
cnf(c_670,plain,
( sK3 = sK0
| sK0 = sunday
| sK0 = saturday
| sK0 = sunday
| sK0 = saturday
| friday = thursday ),
inference(resolve,[status(thm)],[c_669,c_500]) ).
cnf(c_671,plain,
( sK3 = sK0
| sK0 = sunday
| sK0 = sunday
| sK0 = saturday
| friday = thursday ),
inference(copy,[status(thm)],[c_670]) ).
cnf(c_672,plain,
( sK3 = sK0
| sK0 = sunday
| sK0 = saturday
| friday = thursday ),
inference(copy,[status(thm)],[c_671]) ).
cnf(c_570,plain,
( sK3 = sK0
| sK0 = sunday
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_45,c_672]) ).
cnf(c_673,plain,
( sK0 = saturday
| sK0 = sunday
| sK0 = saturday
| sK0 = sunday
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_570,c_550]) ).
cnf(c_674,plain,
( sK0 = saturday
| sK0 = sunday
| sK0 = sunday
| sK0 = saturday ),
inference(copy,[status(thm)],[c_673]) ).
cnf(c_675,plain,
( sK0 = saturday
| sK0 = sunday
| sK0 = saturday ),
inference(copy,[status(thm)],[c_674]) ).
cnf(c_576,plain,
( sK0 = sunday
| sK0 = saturday ),
inference(copy,[status(thm)],[c_675]) ).
cnf(c_577,plain,
( truthday(sunday)
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_576,c_59]) ).
cnf(c_580,plain,
( day1(sunday)
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_576,c_350]) ).
cnf(c_676,plain,
( day2(consecutive(sunday))
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_580,c_70]) ).
cnf(c_587,plain,
( day2(monday)
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_63,c_676]) ).
cnf(c_677,plain,
( day3(consecutive(monday))
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_587,c_72]) ).
cnf(c_592,plain,
( day3(tuesday)
| sK0 = saturday ),
inference(paramod,[status(thm)],[c_64,c_677]) ).
cnf(c_678,plain,
( truthday(friday)
| truthday(wednesday)
| truthday(tuesday)
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_592,c_83]) ).
cnf(c_598,negated_conjecture,
( truthday(friday)
| truthday(wednesday)
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_84,c_678]) ).
cnf(c_679,plain,
( sK0 = saturday
| A = sunday
| ~ truthday(A) ),
inference(resolve,[status(thm)],[c_55,c_577]) ).
cnf(c_680,plain,
( truthday(friday)
| sK0 = saturday
| sK0 = saturday
| wednesday = sunday ),
inference(resolve,[status(thm)],[c_679,c_598]) ).
cnf(c_681,plain,
( truthday(friday)
| sK0 = saturday
| wednesday = sunday ),
inference(copy,[status(thm)],[c_680]) ).
cnf(c_614,plain,
( truthday(friday)
| sK0 = saturday ),
inference(resolve,[status(thm)],[c_44,c_681]) ).
cnf(c_682,plain,
( sK0 = saturday
| A = sunday
| ~ truthday(A) ),
inference(resolve,[status(thm)],[c_55,c_577]) ).
cnf(c_683,plain,
( sK0 = saturday
| sK0 = saturday
| friday = sunday ),
inference(resolve,[status(thm)],[c_682,c_614]) ).
cnf(c_684,plain,
( sK0 = saturday
| friday = sunday ),
inference(copy,[status(thm)],[c_683]) ).
cnf(c_618,plain,
sK0 = saturday,
inference(resolve,[status(thm)],[c_53,c_684]) ).
cnf(c_685,plain,
consecutive(saturday) = sK2,
inference(paramod,[status(thm)],[c_618,c_345]) ).
cnf(c_686,plain,
sunday = sK2,
inference(paramod,[status(thm)],[c_69,c_685]) ).
cnf(c_627,plain,
sK2 = sunday,
inference(copy,[status(thm)],[c_686]) ).
cnf(c_687,plain,
( sK0 = friday
| sK0 = wednesday
| sK3 = saturday ),
inference(paramod,[status(thm)],[c_618,c_225]) ).
cnf(c_688,plain,
( sK0 = friday
| saturday = wednesday
| sK3 = saturday ),
inference(paramod,[status(thm)],[c_618,c_687]) ).
cnf(c_689,plain,
( saturday = friday
| saturday = wednesday
| sK3 = saturday ),
inference(paramod,[status(thm)],[c_618,c_688]) ).
cnf(c_690,plain,
( saturday = friday
| wednesday = saturday
| sK3 = saturday ),
inference(copy,[status(thm)],[c_689]) ).
cnf(c_691,plain,
( friday = saturday
| wednesday = saturday
| sK3 = saturday ),
inference(copy,[status(thm)],[c_690]) ).
cnf(c_692,plain,
( friday = saturday
| sK3 = saturday ),
inference(resolve,[status(thm)],[c_42,c_691]) ).
cnf(c_635,plain,
sK3 = saturday,
inference(resolve,[status(thm)],[c_51,c_692]) ).
cnf(c_693,plain,
consecutive(sunday) = sK3,
inference(paramod,[status(thm)],[c_627,c_213]) ).
cnf(c_694,plain,
monday = sK3,
inference(paramod,[status(thm)],[c_63,c_693]) ).
cnf(c_695,plain,
monday = saturday,
inference(paramod,[status(thm)],[c_635,c_694]) ).
cnf(c_639,plain,
$false,
inference(resolve,[status(thm)],[c_25,c_695]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/10.38 % Computer : n014.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Sat Sep 26 05:13:58 UTC 2026
% 0.11/10.38 % CPUTime :
% 0.11/10.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/10.38 % Process 2216642 was started by sandbox2 on n014,
% 0.11/10.38 % Sat Sep 26 05:13:58 2026
% 0.11/10.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/10.39
% 0.11/10.39 % From the command line: assign(max_seconds, 300).
% 0.14/11.01
% 0.14/11.01 % Assigning unary symbol consecutive kb_weight 0 and highest precedence (17).
% 0.14/11.01
% 0.14/11.01 % SZS status Theorem for theBenchmark
% 0.14/11.01
% 0.14/11.01 % Proof 1 at 0.50 (+ 0.10) seconds.
% 0.14/11.01 % Length of proof is 125.
% 0.14/11.01 % Level of proof is 36.
% 0.14/11.01 % Maximum clause weight is 32.000.
% 0.14/11.01 % Given clauses 201.
% 0.14/11.01
% 0.14/11.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------