%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:22:15 AM UTC 2026
% Result : Theorem 39.64s 5.68s
% Output : CNFRefutation 39.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 23
% Syntax : Number of formulae : 197 ( 40 unt; 0 def)
% Number of atoms : 572 ( 137 equ)
% Maximal formula atoms : 21 ( 2 avg)
% Number of connectives : 473 ( 98 ~; 337 |; 26 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 avg)
% Maximal term depth : 3 ( 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 : 53 ( 0 sgn 14 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(days_of_week,axiom,
! [X0] :
( X0 = sunday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = wednesday
| X0 = tuesday
| X0 = monday ) ).
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 ) ).
fof(truth_unique,axiom,
! [X0,X1] :
( ( truthday(X1)
& truthday(X0) )
=> X0 = X1 ) ).
fof(day1_unique,axiom,
! [X0,X1] :
( ( day1(X1)
& day1(X0) )
=> X0 = X1 ) ).
fof(day2_unique,axiom,
! [X0,X1] :
( ( day2(X1)
& day2(X0) )
=> X0 = X1 ) ).
fof(day3_unique,axiom,
! [X0,X1] :
( ( day3(X1)
& day3(X0) )
=> X0 = X1 ) ).
fof(truth_once,axiom,
? [X0] : truthday(X0) ).
fof(day1_once,axiom,
? [X0] : day1(X0) ).
fof(day2_once,axiom,
? [X0] : day2(X0) ).
fof(day3_once,axiom,
? [X0] : day3(X0) ).
fof(monday_follows_sunday,axiom,
consecutive(sunday) = monday ).
fof(tuesday_follows_monday,axiom,
consecutive(monday) = tuesday ).
fof(wednesday_follows_tuesday,axiom,
consecutive(tuesday) = wednesday ).
fof(thursday_follows_wednesday,axiom,
consecutive(wednesday) = thursday ).
fof(friday_follows_thursday,axiom,
consecutive(thursday) = friday ).
fof(saturday_follows_friday,axiom,
consecutive(friday) = saturday ).
fof(sunday_follows_saturday,axiom,
consecutive(saturday) = sunday ).
fof(day2_follows_day1,axiom,
! [X0] :
( day1(X0)
<=> day2(consecutive(X0)) ) ).
fof(day3_follows_day2,axiom,
! [X0] :
( day2(X0)
<=> day3(consecutive(X0)) ) ).
fof(statement1,axiom,
! [X0] :
( day1(X0)
=> ( truthday(X0)
<=> ( ~ truthday(tuesday)
& ~ truthday(monday) ) ) ) ).
fof(statement2,axiom,
! [X0] :
( day2(X0)
=> ( truthday(X0)
<=> ( day2(sunday)
| day2(saturday)
| day2(thursday) ) ) ) ).
fof(statement3,axiom,
! [X0] :
( day3(X0)
=> ( truthday(X0)
<=> ( ~ truthday(friday)
& ~ truthday(wednesday) ) ) ) ).
fof(tuesday_leo_tells_truths,conjecture,
truthday(tuesday) ).
fof(negated_conjecture,negated_conjecture,
~ truthday(tuesday),
inference(negate_conjecture,[status(cth)],[tuesday_leo_tells_truths]) ).
cnf(c0,plain,
( X0 = tuesday
| X0 = sunday
| X0 = monday
| X0 = wednesday
| X0 = saturday
| X0 = thursday
| X0 = friday ),
inference(clausification,[status(esa)],[days_of_week]) ).
cnf(c10,plain,
saturday != friday,
inference(clausification,[status(esa)],[uniquenames]) ).
cnf(c20,plain,
friday != monday,
inference(clausification,[status(esa)],[uniquenames]) ).
cnf(c21,plain,
wednesday != monday,
inference(clausification,[status(esa)],[uniquenames]) ).
cnf(c22,plain,
( X0 = X1
| ~ truthday(X1)
| ~ truthday(X0) ),
inference(clausification,[status(esa)],[truth_unique]) ).
cnf(c23,plain,
( X0 = X1
| ~ day1(X1)
| ~ day1(X0) ),
inference(clausification,[status(esa)],[day1_unique]) ).
cnf(c24,plain,
( X0 = X1
| ~ day2(X1)
| ~ day2(X0) ),
inference(clausification,[status(esa)],[day2_unique]) ).
cnf(c25,plain,
( X0 = X1
| ~ day3(X1)
| ~ day3(X0) ),
inference(clausification,[status(esa)],[day3_unique]) ).
cnf(c26,plain,
truthday(sK9),
inference(clausification,[status(esa)],[truth_once]) ).
cnf(c27,plain,
day1(sK10),
inference(clausification,[status(esa)],[day1_once]) ).
cnf(c28,plain,
day2(sK11),
inference(clausification,[status(esa)],[day2_once]) ).
cnf(c29,plain,
day3(sK12),
inference(clausification,[status(esa)],[day3_once]) ).
cnf(c30,plain,
consecutive(sunday) = monday,
inference(clausification,[status(esa)],[monday_follows_sunday]) ).
cnf(c31,plain,
consecutive(monday) = tuesday,
inference(clausification,[status(esa)],[tuesday_follows_monday]) ).
cnf(c32,plain,
consecutive(tuesday) = wednesday,
inference(clausification,[status(esa)],[wednesday_follows_tuesday]) ).
cnf(c33,plain,
consecutive(wednesday) = thursday,
inference(clausification,[status(esa)],[thursday_follows_wednesday]) ).
cnf(c34,plain,
consecutive(thursday) = friday,
inference(clausification,[status(esa)],[friday_follows_thursday]) ).
cnf(c35,plain,
consecutive(friday) = saturday,
inference(clausification,[status(esa)],[saturday_follows_friday]) ).
cnf(c36,plain,
consecutive(saturday) = sunday,
inference(clausification,[status(esa)],[sunday_follows_saturday]) ).
cnf(c37,plain,
( day2(consecutive(X0))
| ~ day1(X0) ),
inference(clausification,[status(esa)],[day2_follows_day1]) ).
cnf(c38,plain,
( ~ day2(consecutive(X0))
| day1(X0) ),
inference(clausification,[status(esa)],[day2_follows_day1]) ).
cnf(c39,plain,
( day3(consecutive(X0))
| ~ day2(X0) ),
inference(clausification,[status(esa)],[day3_follows_day2]) ).
cnf(c40,plain,
( ~ day3(consecutive(X0))
| day2(X0) ),
inference(clausification,[status(esa)],[day3_follows_day2]) ).
cnf(c41,plain,
( ~ truthday(monday)
| ~ truthday(X0)
| ~ day1(X0) ),
inference(clausification,[status(esa)],[statement1]) ).
cnf(c43,plain,
( truthday(monday)
| truthday(tuesday)
| truthday(X0)
| ~ day1(X0) ),
inference(clausification,[status(esa)],[statement1]) ).
cnf(c45,plain,
( ~ day2(thursday)
| truthday(X0)
| ~ day2(X0) ),
inference(clausification,[status(esa)],[statement2]) ).
cnf(c46,plain,
( ~ day2(sunday)
| truthday(X0)
| ~ day2(X0) ),
inference(clausification,[status(esa)],[statement2]) ).
cnf(c47,plain,
( ~ day2(saturday)
| truthday(X0)
| ~ day2(X0) ),
inference(clausification,[status(esa)],[statement2]) ).
cnf(c48,plain,
( ~ truthday(wednesday)
| ~ truthday(X0)
| ~ day3(X0) ),
inference(clausification,[status(esa)],[statement3]) ).
cnf(c49,plain,
( ~ truthday(friday)
| ~ truthday(X0)
| ~ day3(X0) ),
inference(clausification,[status(esa)],[statement3]) ).
cnf(c50,plain,
( truthday(wednesday)
| truthday(friday)
| truthday(X0)
| ~ day3(X0) ),
inference(clausification,[status(esa)],[statement3]) ).
cnf(c51,plain,
~ truthday(tuesday),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ day3(sK9)
| ~ truthday(friday) ),
inference(resolution,[status(thm)],[c49,c26]) ).
cnf(d1,plain,
( ~ truthday(X0)
| sK9 = X0 ),
inference(resolution,[status(thm)],[c22,c26]) ).
cnf(d2,plain,
( ~ day1(X0)
| truthday(monday)
| truthday(X0) ),
inference(resolution,[status(thm)],[c51,c43]) ).
cnf(d3,plain,
( ~ day1(sK9)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c41,c26]) ).
cnf(d4,plain,
( day1(sunday)
| ~ day2(monday) ),
inference(superposition,[status(thm)],[c30,c38]) ).
cnf(d5,plain,
( ~ day2(sunday)
| truthday(sK11) ),
inference(resolution,[status(thm)],[c46,c28]) ).
cnf(d6,plain,
( day2(sunday)
| ~ day3(monday) ),
inference(superposition,[status(thm)],[c30,c40]) ).
cnf(d7,plain,
( truthday(monday)
| truthday(sK10) ),
inference(resolution,[status(thm)],[d2,c27]) ).
cnf(d8,plain,
( ~ truthday(X0)
| monday = X0
| truthday(sK10) ),
inference(resolution,[status(thm)],[d7,c22]) ).
cnf(d9,plain,
( truthday(wednesday)
| truthday(friday)
| truthday(sK12) ),
inference(resolution,[status(thm)],[c50,c29]) ).
cnf(d10,plain,
( truthday(sK10)
| monday = friday
| truthday(sK12)
| truthday(wednesday) ),
inference(resolution,[status(thm)],[d9,d8]) ).
cnf(d11,plain,
( truthday(sK12)
| truthday(sK10)
| truthday(wednesday)
| friday != friday ),
inference(superposition,[status(thm)],[d10,c20]) ).
cnf(d12,plain,
( truthday(sK12)
| truthday(sK10)
| truthday(wednesday) ),
inference(equality_resolution,[status(thm)],[d11]) ).
cnf(d13,plain,
( truthday(sK10)
| monday = wednesday
| truthday(sK12)
| truthday(sK10) ),
inference(resolution,[status(thm)],[d12,d8]) ).
cnf(d14,plain,
( truthday(sK12)
| truthday(sK10)
| wednesday != wednesday ),
inference(superposition,[status(thm)],[d13,c21]) ).
cnf(d15,plain,
( truthday(sK12)
| truthday(sK10) ),
inference(equality_resolution,[status(thm)],[d14]) ).
cnf(d16,plain,
( sK9 = sK10
| truthday(sK12) ),
inference(resolution,[status(thm)],[d15,d1]) ).
cnf(d17,plain,
( truthday(sK12)
| day1(sK9) ),
inference(superposition,[status(thm)],[d16,c27]) ).
cnf(d18,plain,
( truthday(sK10)
| monday = sK12
| day1(sK9) ),
inference(resolution,[status(thm)],[d17,d8]) ).
cnf(d19,plain,
( day1(sK9)
| truthday(sK10)
| day3(monday) ),
inference(superposition,[status(thm)],[d18,c29]) ).
cnf(d20,plain,
( sK9 = sK10
| day3(monday)
| day1(sK9) ),
inference(resolution,[status(thm)],[d19,d1]) ).
cnf(d21,plain,
( day3(monday)
| day1(sK9)
| day1(sK9) ),
inference(superposition,[status(thm)],[d20,c27]) ).
cnf(d22,plain,
( day2(consecutive(sK9))
| day3(monday) ),
inference(resolution,[status(thm)],[d21,c37]) ).
cnf(d23,plain,
( day3(consecutive(consecutive(sK9)))
| day3(monday) ),
inference(resolution,[status(thm)],[d22,c39]) ).
cnf(d24,plain,
( day2(sunday)
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d23,d6]) ).
cnf(d25,plain,
( truthday(sK11)
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d24,d5]) ).
cnf(d26,plain,
( sK9 = sK11
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d25,d1]) ).
cnf(d27,plain,
( day3(consecutive(consecutive(sK9)))
| day2(sK9) ),
inference(superposition,[status(thm)],[d26,c28]) ).
cnf(d28,plain,
( sK9 = sK12
| day1(sK9) ),
inference(resolution,[status(thm)],[d17,d1]) ).
cnf(d29,plain,
( day1(sK9)
| day3(sK9) ),
inference(superposition,[status(thm)],[d28,c29]) ).
cnf(d30,plain,
( day2(consecutive(sK9))
| day3(sK9) ),
inference(resolution,[status(thm)],[d29,c37]) ).
cnf(d31,plain,
( day3(consecutive(consecutive(sK9)))
| day3(sK9) ),
inference(resolution,[status(thm)],[d30,c39]) ).
cnf(d32,plain,
( ~ day3(X0)
| sK9 = X0
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d31,c25]) ).
cnf(d33,plain,
( day3(consecutive(consecutive(sK9)))
| sK9 = monday
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d23,d32]) ).
cnf(d34,plain,
( day3(consecutive(consecutive(sK9)))
| day3(consecutive(consecutive(sK9)))
| day2(monday) ),
inference(superposition,[status(thm)],[d33,d27]) ).
cnf(d35,plain,
( day1(sunday)
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d34,d4]) ).
cnf(d36,plain,
( day3(consecutive(consecutive(sK9)))
| truthday(monday) ),
inference(superposition,[status(thm)],[d33,c26]) ).
cnf(d37,plain,
( ~ day1(sK9)
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d36,d3]) ).
cnf(d38,plain,
( ~ day2(X0)
| X0 = sK11 ),
inference(resolution,[status(thm)],[c24,c28]) ).
cnf(d39,plain,
( sunday = sK11
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d24,d38]) ).
cnf(d40,plain,
( day3(consecutive(consecutive(sK9)))
| day3(consecutive(consecutive(sK9)))
| truthday(sunday) ),
inference(superposition,[status(thm)],[d39,d25]) ).
cnf(d41,plain,
( sK9 = sunday
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d40,d1]) ).
cnf(d42,plain,
( day3(consecutive(consecutive(sK9)))
| day3(consecutive(consecutive(sK9)))
| ~ day1(sunday) ),
inference(superposition,[status(thm)],[d41,d37]) ).
cnf(d43,plain,
( day3(consecutive(consecutive(sK9)))
| day3(consecutive(consecutive(sK9))) ),
inference(resolution,[status(thm)],[d42,d35]) ).
cnf(d44,plain,
day2(consecutive(sK9)),
inference(resolution,[status(thm)],[d43,c40]) ).
cnf(d45,plain,
day1(sK9),
inference(resolution,[status(thm)],[d44,c38]) ).
cnf(d46,plain,
~ truthday(monday),
inference(resolution,[status(thm)],[d45,d3]) ).
cnf(d47,plain,
( ~ day1(X0)
| truthday(X0) ),
inference(resolution,[status(thm)],[d46,d2]) ).
cnf(d48,plain,
( day1(friday)
| ~ day2(saturday) ),
inference(superposition,[status(thm)],[c35,c38]) ).
cnf(d49,plain,
( day2(saturday)
| ~ day3(sunday) ),
inference(superposition,[status(thm)],[c36,c40]) ).
cnf(d50,plain,
( day1(tuesday)
| ~ day2(wednesday) ),
inference(superposition,[status(thm)],[c32,c38]) ).
cnf(d51,plain,
( ~ day2(thursday)
| truthday(sK11) ),
inference(resolution,[status(thm)],[c45,c28]) ).
cnf(d52,plain,
( ~ truthday(X0)
| sK10 = X0
| truthday(sK12) ),
inference(resolution,[status(thm)],[d15,c22]) ).
cnf(d53,plain,
( ~ truthday(X0)
| friday = X0
| truthday(sK12)
| truthday(wednesday) ),
inference(resolution,[status(thm)],[d9,c22]) ).
cnf(d54,plain,
( truthday(sK12)
| truthday(wednesday)
| friday = sK10
| truthday(sK12) ),
inference(resolution,[status(thm)],[d15,d53]) ).
cnf(d55,plain,
( truthday(sK12)
| truthday(wednesday)
| day1(friday) ),
inference(superposition,[status(thm)],[d54,c27]) ).
cnf(d56,plain,
( truthday(sK12)
| sK10 = wednesday
| day1(friday)
| truthday(sK12) ),
inference(resolution,[status(thm)],[d55,d52]) ).
cnf(d57,plain,
( day1(friday)
| truthday(sK12)
| day1(wednesday) ),
inference(superposition,[status(thm)],[d56,c27]) ).
cnf(d58,plain,
( sK9 = sK12
| day1(wednesday)
| day1(friday) ),
inference(resolution,[status(thm)],[d57,d1]) ).
cnf(d59,plain,
( day1(wednesday)
| day1(friday)
| day3(sK9) ),
inference(superposition,[status(thm)],[d58,c29]) ).
cnf(d60,plain,
( day2(consecutive(friday))
| day3(sK9)
| day1(wednesday) ),
inference(resolution,[status(thm)],[d59,c37]) ).
cnf(d61,plain,
( day3(sK9)
| day2(saturday)
| day1(wednesday) ),
inference(demodulation,[status(thm)],[d60,c35]) ).
cnf(d62,plain,
( day2(consecutive(wednesday))
| day3(sK9)
| day2(saturday) ),
inference(resolution,[status(thm)],[d61,c37]) ).
cnf(d63,plain,
( day3(sK9)
| day2(thursday)
| day2(saturday) ),
inference(demodulation,[status(thm)],[d62,c33]) ).
cnf(d64,plain,
( day3(consecutive(saturday))
| day3(sK9)
| day2(thursday) ),
inference(resolution,[status(thm)],[d63,c39]) ).
cnf(d65,plain,
( day3(sunday)
| day3(sK9)
| day2(thursday) ),
inference(demodulation,[status(thm)],[d64,c36]) ).
cnf(d66,plain,
( truthday(sK11)
| day3(sunday)
| day3(sK9) ),
inference(resolution,[status(thm)],[d65,d51]) ).
cnf(d67,plain,
( sK9 = sK11
| day3(sK9)
| day3(sunday) ),
inference(resolution,[status(thm)],[d66,d1]) ).
cnf(d68,plain,
( day3(sK9)
| day3(sunday)
| day2(sK9) ),
inference(superposition,[status(thm)],[d67,c28]) ).
cnf(d69,plain,
( ~ day1(X0)
| X0 = sK9 ),
inference(resolution,[status(thm)],[d45,c23]) ).
cnf(d70,plain,
( day1(wednesday)
| ~ day2(thursday) ),
inference(superposition,[status(thm)],[c33,c38]) ).
cnf(d71,plain,
( day1(wednesday)
| day3(sunday)
| day3(sK9) ),
inference(resolution,[status(thm)],[d65,d70]) ).
cnf(d72,plain,
( wednesday = sK9
| day3(sK9)
| day3(sunday) ),
inference(resolution,[status(thm)],[d71,d69]) ).
cnf(d73,plain,
( day3(sK9)
| day3(sunday)
| day3(sK9)
| day3(sunday)
| day2(wednesday) ),
inference(superposition,[status(thm)],[d72,d68]) ).
cnf(d74,plain,
( day1(tuesday)
| day3(sK9)
| day3(sunday) ),
inference(resolution,[status(thm)],[d73,d50]) ).
cnf(d75,plain,
( truthday(tuesday)
| day3(sK9)
| day3(sunday) ),
inference(resolution,[status(thm)],[d74,d47]) ).
cnf(d76,plain,
( day3(sK9)
| day3(sunday) ),
inference(resolution,[status(thm)],[c51,d75]) ).
cnf(d77,plain,
( day2(saturday)
| day3(sK9) ),
inference(resolution,[status(thm)],[d76,d49]) ).
cnf(d78,plain,
( day1(friday)
| day3(sK9) ),
inference(resolution,[status(thm)],[d77,d48]) ).
cnf(d79,plain,
( truthday(friday)
| day3(sK9) ),
inference(resolution,[status(thm)],[d78,d47]) ).
cnf(d80,plain,
( sK9 = friday
| day3(sK9) ),
inference(resolution,[status(thm)],[d79,d1]) ).
cnf(d81,plain,
( ~ day2(saturday)
| truthday(sK11) ),
inference(resolution,[status(thm)],[c47,c28]) ).
cnf(d82,plain,
( truthday(sK11)
| day3(sK9) ),
inference(resolution,[status(thm)],[d77,d81]) ).
cnf(d83,plain,
( saturday = sK11
| day3(sK9) ),
inference(resolution,[status(thm)],[d77,d38]) ).
cnf(d84,plain,
( day3(sK9)
| day3(sK9)
| truthday(saturday) ),
inference(superposition,[status(thm)],[d83,d82]) ).
cnf(d85,plain,
( sK9 = saturday
| day3(sK9) ),
inference(resolution,[status(thm)],[d84,d1]) ).
cnf(d86,plain,
( day3(sK9)
| day3(sK9)
| saturday = friday ),
inference(superposition,[status(thm)],[d85,d80]) ).
cnf(d87,plain,
day3(sK9),
inference(resolution,[status(thm)],[c10,d86]) ).
cnf(d88,plain,
~ truthday(friday),
inference(resolution,[status(thm)],[d87,d0]) ).
cnf(d89,plain,
( ~ day3(X0)
| truthday(wednesday)
| truthday(X0) ),
inference(resolution,[status(thm)],[d88,c50]) ).
cnf(d90,plain,
( ~ day3(sK9)
| ~ truthday(wednesday) ),
inference(resolution,[status(thm)],[c48,c26]) ).
cnf(d91,plain,
~ truthday(wednesday),
inference(resolution,[status(thm)],[d87,d90]) ).
cnf(d92,plain,
( ~ day3(X0)
| truthday(X0) ),
inference(resolution,[status(thm)],[d91,d89]) ).
cnf(d93,plain,
( day2(wednesday)
| ~ day3(thursday) ),
inference(superposition,[status(thm)],[c33,c40]) ).
cnf(d94,plain,
( day1(thursday)
| ~ day2(friday) ),
inference(superposition,[status(thm)],[c34,c38]) ).
cnf(d95,plain,
( day2(friday)
| ~ day3(saturday) ),
inference(superposition,[status(thm)],[c35,c40]) ).
cnf(d96,plain,
( day1(monday)
| ~ day2(tuesday) ),
inference(superposition,[status(thm)],[c31,c38]) ).
cnf(d97,plain,
( ~ day3(X0)
| sK12 = X0 ),
inference(resolution,[status(thm)],[c25,c29]) ).
cnf(d98,plain,
sK12 = sK9,
inference(resolution,[status(thm)],[d87,d97]) ).
cnf(d99,plain,
day3(consecutive(sK11)),
inference(resolution,[status(thm)],[c39,c28]) ).
cnf(d100,plain,
sK12 = consecutive(sK11),
inference(resolution,[status(thm)],[d97,d99]) ).
cnf(d101,plain,
( X0 = tuesday
| X0 = sunday
| X0 = monday
| X0 = wednesday
| X0 = saturday
| X0 = thursday
| consecutive(X0) = saturday ),
inference(superposition,[status(thm)],[c0,c35]) ).
cnf(d102,plain,
( consecutive(X0) = saturday
| X0 = tuesday
| X0 = sunday
| X0 = monday
| X0 = wednesday
| X0 = saturday
| day1(wednesday)
| ~ day2(X0) ),
inference(superposition,[status(thm)],[d101,d70]) ).
cnf(d103,plain,
( day1(wednesday)
| consecutive(sK11) = saturday
| sK11 = tuesday
| sK11 = sunday
| sK11 = monday
| sK11 = wednesday
| sK11 = saturday ),
inference(resolution,[status(thm)],[d102,c28]) ).
cnf(d104,plain,
( day1(wednesday)
| sK12 = saturday
| sK11 = tuesday
| sK11 = sunday
| sK11 = monday
| sK11 = wednesday
| sK11 = saturday ),
inference(demodulation,[status(thm)],[d103,d100]) ).
cnf(d105,plain,
( day1(wednesday)
| sK12 = saturday
| sK11 = tuesday
| sK11 = sunday
| sK11 = monday
| sK11 = wednesday
| day2(saturday) ),
inference(superposition,[status(thm)],[d104,c28]) ).
cnf(d106,plain,
( day2(saturday)
| day1(wednesday)
| sK12 = saturday
| sK11 = tuesday
| sK11 = sunday
| sK11 = monday
| day2(wednesday) ),
inference(superposition,[status(thm)],[d105,c28]) ).
cnf(d107,plain,
( day2(wednesday)
| day2(saturday)
| day1(wednesday)
| sK9 = saturday
| sK11 = tuesday
| sK11 = sunday
| sK11 = monday ),
inference(demodulation,[status(thm)],[d106,d98]) ).
cnf(d108,plain,
( day2(wednesday)
| day2(saturday)
| day1(wednesday)
| sK9 = saturday
| sK11 = tuesday
| sK11 = sunday
| day2(monday) ),
inference(superposition,[status(thm)],[d107,c28]) ).
cnf(d109,plain,
( day2(monday)
| day2(wednesday)
| day2(saturday)
| day1(wednesday)
| sK11 = tuesday
| sK11 = sunday
| day1(saturday) ),
inference(superposition,[status(thm)],[d108,d45]) ).
cnf(d110,plain,
( day2(monday)
| day2(wednesday)
| day2(saturday)
| day1(wednesday)
| day1(saturday)
| sK11 = tuesday
| day2(sunday) ),
inference(superposition,[status(thm)],[d109,c28]) ).
cnf(d111,plain,
( day2(sunday)
| day2(monday)
| day2(wednesday)
| day2(saturday)
| day1(wednesday)
| day1(saturday)
| day2(tuesday) ),
inference(superposition,[status(thm)],[d110,c28]) ).
cnf(d112,plain,
( saturday = sK9
| day2(tuesday)
| day2(sunday)
| day2(monday)
| day2(wednesday)
| day2(saturday)
| day1(wednesday) ),
inference(resolution,[status(thm)],[d111,d69]) ).
cnf(d113,plain,
( day2(tuesday)
| day2(sunday)
| day2(monday)
| day2(wednesday)
| day2(saturday)
| day1(wednesday)
| day3(saturday) ),
inference(superposition,[status(thm)],[d112,d87]) ).
cnf(d114,plain,
( truthday(wednesday)
| day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday)
| day2(wednesday)
| day2(saturday) ),
inference(resolution,[status(thm)],[d113,d47]) ).
cnf(d115,plain,
( day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday)
| day2(wednesday)
| day2(saturday) ),
inference(resolution,[status(thm)],[d91,d114]) ).
cnf(d116,plain,
( day1(friday)
| day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday)
| day2(wednesday) ),
inference(resolution,[status(thm)],[d115,d48]) ).
cnf(d117,plain,
( truthday(friday)
| day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday)
| day2(wednesday) ),
inference(resolution,[status(thm)],[d116,d47]) ).
cnf(d118,plain,
( day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday)
| day2(wednesday) ),
inference(resolution,[status(thm)],[d88,d117]) ).
cnf(d119,plain,
( day1(tuesday)
| day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday) ),
inference(resolution,[status(thm)],[d118,d50]) ).
cnf(d120,plain,
( truthday(tuesday)
| day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday) ),
inference(resolution,[status(thm)],[d119,d47]) ).
cnf(d121,plain,
( day3(saturday)
| day2(tuesday)
| day2(sunday)
| day2(monday) ),
inference(resolution,[status(thm)],[c51,d120]) ).
cnf(d122,plain,
( day3(consecutive(monday))
| day3(saturday)
| day2(tuesday)
| day2(sunday) ),
inference(resolution,[status(thm)],[d121,c39]) ).
cnf(d123,plain,
( day3(tuesday)
| day3(saturday)
| day2(tuesday)
| day2(sunday) ),
inference(demodulation,[status(thm)],[d122,c31]) ).
cnf(d124,plain,
( day3(consecutive(sunday))
| day3(tuesday)
| day3(saturday)
| day2(tuesday) ),
inference(resolution,[status(thm)],[d123,c39]) ).
cnf(d125,plain,
( day3(monday)
| day3(tuesday)
| day3(saturday)
| day2(tuesday) ),
inference(demodulation,[status(thm)],[d124,c30]) ).
cnf(d126,plain,
( day1(monday)
| day3(monday)
| day3(tuesday)
| day3(saturday) ),
inference(resolution,[status(thm)],[d125,d96]) ).
cnf(d127,plain,
( truthday(monday)
| day3(tuesday)
| day3(monday)
| day3(saturday) ),
inference(resolution,[status(thm)],[d126,d47]) ).
cnf(d128,plain,
( day3(tuesday)
| day3(monday)
| day3(saturday) ),
inference(resolution,[status(thm)],[d46,d127]) ).
cnf(d129,plain,
( day2(friday)
| day3(tuesday)
| day3(monday) ),
inference(resolution,[status(thm)],[d128,d95]) ).
cnf(d130,plain,
( day1(thursday)
| day3(tuesday)
| day3(monday) ),
inference(resolution,[status(thm)],[d129,d94]) ).
cnf(d131,plain,
( thursday = sK9
| day3(tuesday)
| day3(monday) ),
inference(resolution,[status(thm)],[d130,d69]) ).
cnf(d132,plain,
( day3(tuesday)
| day3(monday)
| day3(thursday) ),
inference(superposition,[status(thm)],[d131,d87]) ).
cnf(d133,plain,
( day2(wednesday)
| day3(tuesday)
| day3(monday) ),
inference(resolution,[status(thm)],[d132,d93]) ).
cnf(d134,plain,
( day1(tuesday)
| day3(tuesday)
| day3(monday) ),
inference(resolution,[status(thm)],[d133,d50]) ).
cnf(d135,plain,
( truthday(tuesday)
| day3(tuesday)
| day3(monday) ),
inference(resolution,[status(thm)],[d134,d47]) ).
cnf(d136,plain,
( day3(tuesday)
| day3(monday) ),
inference(resolution,[status(thm)],[c51,d135]) ).
cnf(d137,plain,
( truthday(monday)
| day3(tuesday) ),
inference(resolution,[status(thm)],[d136,d92]) ).
cnf(d138,plain,
day3(tuesday),
inference(resolution,[status(thm)],[d46,d137]) ).
cnf(d139,plain,
truthday(tuesday),
inference(resolution,[status(thm)],[d138,d92]) ).
cnf(d140,plain,
$false,
inference(resolution,[status(thm)],[c51,d139]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.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 26 05:15:49 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.64/5.68 % SZS status Theorem for theBenchmark.p
% 39.64/5.68 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------