%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.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 : Fri Sep 25 02:32:56 PM UTC 2026
% Result : Theorem 2.79s 1.36s
% Output : CNFRefutation 2.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 29
% Syntax : Number of formulae : 321 ( 93 unt; 0 def)
% Number of atoms : 789 ( 230 equ)
% Maximal formula atoms : 21 ( 2 avg)
% Number of connectives : 914 ( 446 ~; 409 |; 44 &)
% ( 8 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-1 aty)
% Number of variables : 166 ( 0 sgn 162 !; 4 ?; 99 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( X0 = sunday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = wednesday
| X0 = tuesday
| X0 = monday ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',days_of_week) ).
fof(f2,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',uniquenames) ).
fof(f3,axiom,
! [X0,X1] :
( ( truthday(X1)
& truthday(X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',truth_unique) ).
fof(f4,axiom,
! [X0,X1] :
( ( day1(X1)
& day1(X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day1_unique) ).
fof(f5,axiom,
! [X0,X1] :
( ( day2(X1)
& day2(X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day2_unique) ).
fof(f6,axiom,
! [X0,X1] :
( ( day3(X1)
& day3(X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day3_unique) ).
fof(f7,axiom,
? [X0] : truthday(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',truth_once) ).
fof(f8,axiom,
? [X0] : day1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day1_once) ).
fof(f9,axiom,
? [X0] : day2(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day2_once) ).
fof(f10,axiom,
? [X0] : day3(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day3_once) ).
fof(f11,axiom,
consecutive(sunday) = monday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monday_follows_sunday) ).
fof(f12,axiom,
consecutive(monday) = tuesday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuesday_follows_monday) ).
fof(f13,axiom,
consecutive(tuesday) = wednesday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wednesday_follows_tuesday) ).
fof(f14,axiom,
consecutive(wednesday) = thursday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thursday_follows_wednesday) ).
fof(f15,axiom,
consecutive(thursday) = friday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',friday_follows_thursday) ).
fof(f16,axiom,
consecutive(friday) = saturday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',saturday_follows_friday) ).
fof(f17,axiom,
consecutive(saturday) = sunday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sunday_follows_saturday) ).
fof(f18,axiom,
! [X0] :
( day1(X0)
<=> day2(consecutive(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day2_follows_day1) ).
fof(f19,axiom,
! [X0] :
( day2(X0)
<=> day3(consecutive(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',day3_follows_day2) ).
fof(f20,axiom,
! [X0] :
( day1(X0)
=> ( truthday(X0)
<=> ( ~ truthday(tuesday)
& ~ truthday(monday) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',statement1) ).
fof(f21,axiom,
! [X0] :
( day2(X0)
=> ( truthday(X0)
<=> ( day2(sunday)
| day2(saturday)
| day2(thursday) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',statement2) ).
fof(f22,axiom,
! [X0] :
( day3(X0)
=> ( truthday(X0)
<=> ( ~ truthday(friday)
& ~ truthday(wednesday) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',statement3) ).
fof(f23,conjecture,
truthday(tuesday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuesday_leo_tells_truths) ).
fof(f24,negated_conjecture,
~ truthday(tuesday),
inference(negated_conjecture,[status(cth)],[f23]) ).
fof(f25,plain,
~ truthday(tuesday),
inference(flattening,[],[f24]) ).
fof(f26,plain,
! [X0,X1] :
( ~ truthday(X1)
| ~ truthday(X0)
| X0 = X1 ),
inference(ennf_transformation,[],[f3]) ).
fof(f27,plain,
! [X0,X1] :
( ~ truthday(X1)
| ~ truthday(X0)
| X0 = X1 ),
inference(flattening,[],[f26]) ).
fof(f28,plain,
! [X0,X1] :
( ~ day1(X1)
| ~ day1(X0)
| X0 = X1 ),
inference(ennf_transformation,[],[f4]) ).
fof(f29,plain,
! [X0,X1] :
( ~ day1(X1)
| ~ day1(X0)
| X0 = X1 ),
inference(flattening,[],[f28]) ).
fof(f30,plain,
! [X0,X1] :
( ~ day2(X1)
| ~ day2(X0)
| X0 = X1 ),
inference(ennf_transformation,[],[f5]) ).
fof(f31,plain,
! [X0,X1] :
( ~ day2(X1)
| ~ day2(X0)
| X0 = X1 ),
inference(flattening,[],[f30]) ).
fof(f32,plain,
! [X0,X1] :
( ~ day3(X1)
| ~ day3(X0)
| X0 = X1 ),
inference(ennf_transformation,[],[f6]) ).
fof(f33,plain,
! [X0,X1] :
( ~ day3(X1)
| ~ day3(X0)
| X0 = X1 ),
inference(flattening,[],[f32]) ).
fof(f34,plain,
! [X0] :
( ~ day1(X0)
| ( truthday(X0)
<=> ( ~ truthday(tuesday)
& ~ truthday(monday) ) ) ),
inference(ennf_transformation,[],[f20]) ).
fof(f35,plain,
! [X0] :
( ~ day2(X0)
| ( truthday(X0)
<=> ( day2(sunday)
| day2(saturday)
| day2(thursday) ) ) ),
inference(ennf_transformation,[],[f21]) ).
fof(f36,plain,
! [X0] :
( ~ day3(X0)
| ( truthday(X0)
<=> ( ~ truthday(friday)
& ~ truthday(wednesday) ) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f37,plain,
truthday(sK0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f7]) ).
fof(f38,plain,
day1(sK1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1)],[f8]) ).
fof(f39,plain,
day2(sK2),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f9]) ).
fof(f40,plain,
day3(sK3),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f10]) ).
fof(f41,plain,
! [X0] :
( ( ~ day1(X0)
| day2(consecutive(X0)) )
& ( ~ day2(consecutive(X0))
| day1(X0) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f42,plain,
! [X0] :
( ( ~ day2(X0)
| day3(consecutive(X0)) )
& ( ~ day3(consecutive(X0))
| day2(X0) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f43,plain,
! [X0] :
( ~ day1(X0)
| ( ( ~ truthday(X0)
| ( ~ truthday(tuesday)
& ~ truthday(monday) ) )
& ( truthday(tuesday)
| truthday(monday)
| truthday(X0) ) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f44,plain,
! [X0] :
( ~ day1(X0)
| ( ( ~ truthday(X0)
| ( ~ truthday(tuesday)
& ~ truthday(monday) ) )
& ( truthday(tuesday)
| truthday(monday)
| truthday(X0) ) ) ),
inference(flattening,[],[f43]) ).
fof(f45,plain,
! [X0] :
( ~ day2(X0)
| ( ( ~ truthday(X0)
| day2(sunday)
| day2(saturday)
| day2(thursday) )
& ( ( ~ day2(sunday)
& ~ day2(saturday)
& ~ day2(thursday) )
| truthday(X0) ) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f46,plain,
! [X0] :
( ~ day2(X0)
| ( ( ~ truthday(X0)
| day2(sunday)
| day2(saturday)
| day2(thursday) )
& ( ( ~ day2(sunday)
& ~ day2(saturday)
& ~ day2(thursday) )
| truthday(X0) ) ) ),
inference(flattening,[],[f45]) ).
fof(f47,plain,
! [X0] :
( ~ day3(X0)
| ( ( ~ truthday(X0)
| ( ~ truthday(friday)
& ~ truthday(wednesday) ) )
& ( truthday(friday)
| truthday(wednesday)
| truthday(X0) ) ) ),
inference(nnf_transformation,[],[f36]) ).
fof(f48,plain,
! [X0] :
( ~ day3(X0)
| ( ( ~ truthday(X0)
| ( ~ truthday(friday)
& ~ truthday(wednesday) ) )
& ( truthday(friday)
| truthday(wednesday)
| truthday(X0) ) ) ),
inference(flattening,[],[f47]) ).
fof(f49,plain,
! [X0] :
( sunday = X0
| saturday = X0
| friday = X0
| thursday = X0
| wednesday = X0
| tuesday = X0
| monday = X0 ),
inference(cnf_transformation,[],[f1]) ).
fof(f51,plain,
friday != sunday,
inference(cnf_transformation,[],[f2]) ).
fof(f52,plain,
friday != saturday,
inference(cnf_transformation,[],[f2]) ).
fof(f53,plain,
thursday != sunday,
inference(cnf_transformation,[],[f2]) ).
fof(f55,plain,
thursday != friday,
inference(cnf_transformation,[],[f2]) ).
fof(f56,plain,
wednesday != sunday,
inference(cnf_transformation,[],[f2]) ).
fof(f57,plain,
wednesday != saturday,
inference(cnf_transformation,[],[f2]) ).
fof(f59,plain,
wednesday != thursday,
inference(cnf_transformation,[],[f2]) ).
fof(f65,plain,
monday != sunday,
inference(cnf_transformation,[],[f2]) ).
fof(f66,plain,
monday != saturday,
inference(cnf_transformation,[],[f2]) ).
fof(f67,plain,
monday != friday,
inference(cnf_transformation,[],[f2]) ).
fof(f68,plain,
monday != thursday,
inference(cnf_transformation,[],[f2]) ).
fof(f69,plain,
monday != wednesday,
inference(cnf_transformation,[],[f2]) ).
fof(f70,plain,
monday != tuesday,
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
! [X0,X1] :
( ~ truthday(X1)
| ~ truthday(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f27]) ).
fof(f72,plain,
! [X0,X1] :
( ~ day1(X1)
| ~ day1(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f29]) ).
fof(f73,plain,
! [X0,X1] :
( ~ day2(X1)
| ~ day2(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f31]) ).
fof(f74,plain,
! [X0,X1] :
( ~ day3(X1)
| ~ day3(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f33]) ).
fof(f75,plain,
truthday(sK0),
inference(cnf_transformation,[],[f37]) ).
fof(f76,plain,
day1(sK1),
inference(cnf_transformation,[],[f38]) ).
fof(f77,plain,
day2(sK2),
inference(cnf_transformation,[],[f39]) ).
fof(f78,plain,
day3(sK3),
inference(cnf_transformation,[],[f40]) ).
fof(f79,plain,
monday = consecutive(sunday),
inference(cnf_transformation,[],[f11]) ).
fof(f80,plain,
tuesday = consecutive(monday),
inference(cnf_transformation,[],[f12]) ).
fof(f81,plain,
wednesday = consecutive(tuesday),
inference(cnf_transformation,[],[f13]) ).
fof(f82,plain,
thursday = consecutive(wednesday),
inference(cnf_transformation,[],[f14]) ).
fof(f83,plain,
friday = consecutive(thursday),
inference(cnf_transformation,[],[f15]) ).
fof(f84,plain,
saturday = consecutive(friday),
inference(cnf_transformation,[],[f16]) ).
fof(f85,plain,
sunday = consecutive(saturday),
inference(cnf_transformation,[],[f17]) ).
fof(f86,plain,
! [X0] :
( ~ day1(X0)
| day2(consecutive(X0)) ),
inference(cnf_transformation,[],[f41]) ).
fof(f87,plain,
! [X0] :
( ~ day2(consecutive(X0))
| day1(X0) ),
inference(cnf_transformation,[],[f41]) ).
fof(f88,plain,
! [X0] :
( ~ day2(X0)
| day3(consecutive(X0)) ),
inference(cnf_transformation,[],[f42]) ).
fof(f89,plain,
! [X0] :
( ~ day3(consecutive(X0))
| day2(X0) ),
inference(cnf_transformation,[],[f42]) ).
fof(f91,plain,
! [X0] :
( ~ day1(X0)
| ~ truthday(X0)
| ~ truthday(monday) ),
inference(cnf_transformation,[],[f44]) ).
fof(f92,plain,
! [X0] :
( ~ day1(X0)
| truthday(tuesday)
| truthday(monday)
| truthday(X0) ),
inference(cnf_transformation,[],[f44]) ).
fof(f93,plain,
! [X0] :
( ~ day2(X0)
| ~ truthday(X0)
| day2(sunday)
| day2(saturday)
| day2(thursday) ),
inference(cnf_transformation,[],[f46]) ).
fof(f94,plain,
! [X0] :
( ~ day2(X0)
| ~ day2(sunday)
| truthday(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f95,plain,
! [X0] :
( ~ day2(X0)
| ~ day2(saturday)
| truthday(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f96,plain,
! [X0] :
( ~ day2(X0)
| ~ day2(thursday)
| truthday(X0) ),
inference(cnf_transformation,[],[f46]) ).
fof(f97,plain,
! [X0] :
( ~ day3(X0)
| ~ truthday(X0)
| ~ truthday(friday) ),
inference(cnf_transformation,[],[f48]) ).
fof(f98,plain,
! [X0] :
( ~ day3(X0)
| ~ truthday(X0)
| ~ truthday(wednesday) ),
inference(cnf_transformation,[],[f48]) ).
fof(f99,plain,
! [X0] :
( ~ day3(X0)
| truthday(friday)
| truthday(wednesday)
| truthday(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f100,plain,
~ truthday(tuesday),
inference(cnf_transformation,[],[f25]) ).
tcf(c_49,plain,
! [X0: $i] :
( ( X0 = sunday )
| ( X0 = saturday )
| ( X0 = friday )
| ( X0 = thursday )
| ( X0 = wednesday )
| ( X0 = tuesday )
| ( X0 = monday ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_50,plain,
monday != tuesday,
inference(cnf_transformation,[],[f70]) ).
tcf(c_51,plain,
monday != wednesday,
inference(cnf_transformation,[],[f69]) ).
tcf(c_52,plain,
monday != thursday,
inference(cnf_transformation,[],[f68]) ).
tcf(c_53,plain,
monday != friday,
inference(cnf_transformation,[],[f67]) ).
tcf(c_54,plain,
monday != saturday,
inference(cnf_transformation,[],[f66]) ).
tcf(c_55,plain,
monday != sunday,
inference(cnf_transformation,[],[f65]) ).
tcf(c_61,plain,
wednesday != thursday,
inference(cnf_transformation,[],[f59]) ).
tcf(c_63,plain,
wednesday != saturday,
inference(cnf_transformation,[],[f57]) ).
tcf(c_64,plain,
wednesday != sunday,
inference(cnf_transformation,[],[f56]) ).
tcf(c_65,plain,
thursday != friday,
inference(cnf_transformation,[],[f55]) ).
tcf(c_67,plain,
thursday != sunday,
inference(cnf_transformation,[],[f53]) ).
tcf(c_68,plain,
friday != saturday,
inference(cnf_transformation,[],[f52]) ).
tcf(c_69,plain,
friday != sunday,
inference(cnf_transformation,[],[f51]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ truthday(X1)
| ~ truthday(X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ day1(X1)
| ~ day1(X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ day2(X1)
| ~ day2(X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ day3(X1)
| ~ day3(X0) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_75,plain,
truthday(sK0),
inference(cnf_transformation,[],[f75]) ).
tcf(c_76,plain,
day1(sK1),
inference(cnf_transformation,[],[f76]) ).
tcf(c_77,plain,
day2(sK2),
inference(cnf_transformation,[],[f77]) ).
tcf(c_78,plain,
day3(sK3),
inference(cnf_transformation,[],[f78]) ).
tcf(c_79,plain,
consecutive(sunday) = monday,
inference(cnf_transformation,[],[f79]) ).
tcf(c_80,plain,
consecutive(monday) = tuesday,
inference(cnf_transformation,[],[f80]) ).
tcf(c_81,plain,
consecutive(tuesday) = wednesday,
inference(cnf_transformation,[],[f81]) ).
tcf(c_82,plain,
consecutive(wednesday) = thursday,
inference(cnf_transformation,[],[f82]) ).
tcf(c_83,plain,
consecutive(thursday) = friday,
inference(cnf_transformation,[],[f83]) ).
tcf(c_84,plain,
consecutive(friday) = saturday,
inference(cnf_transformation,[],[f84]) ).
tcf(c_85,plain,
consecutive(saturday) = sunday,
inference(cnf_transformation,[],[f85]) ).
tcf(c_86,plain,
! [X0: $i] :
( day1(X0)
| ~ day2(consecutive(X0)) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_87,plain,
! [X0: $i] :
( day2(consecutive(X0))
| ~ day1(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_88,plain,
! [X0: $i] :
( day2(X0)
| ~ day3(consecutive(X0)) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_89,plain,
! [X0: $i] :
( day3(consecutive(X0))
| ~ day2(X0) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_90,plain,
! [X0: $i] :
( truthday(tuesday)
| truthday(monday)
| truthday(X0)
| ~ day1(X0) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_91,plain,
! [X0: $i] :
( ~ truthday(monday)
| ~ day1(X0)
| ~ truthday(X0) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_93,plain,
! [X0: $i] :
( truthday(X0)
| ~ day2(thursday)
| ~ day2(X0) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_94,plain,
! [X0: $i] :
( truthday(X0)
| ~ day2(saturday)
| ~ day2(X0) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_95,plain,
! [X0: $i] :
( truthday(X0)
| ~ day2(sunday)
| ~ day2(X0) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_96,plain,
! [X0: $i] :
( day2(sunday)
| day2(saturday)
| day2(thursday)
| ~ day2(X0)
| ~ truthday(X0) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_97,plain,
! [X0: $i] :
( truthday(friday)
| truthday(wednesday)
| truthday(X0)
| ~ day3(X0) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_98,plain,
! [X0: $i] :
( ~ truthday(wednesday)
| ~ day3(X0)
| ~ truthday(X0) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_99,plain,
! [X0: $i] :
( ~ truthday(friday)
| ~ day3(X0)
| ~ truthday(X0) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_100,negated_conjecture,
~ truthday(tuesday),
inference(cnf_transformation,[],[f100]) ).
tcf(c_109,plain,
( truthday(tuesday)
| truthday(monday)
| ~ day1(tuesday) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_116,plain,
! [X0: $i] :
( ~ day1(X0)
| truthday(X0)
| truthday(monday) ),
inference(global_subsumption_just,[status(thm)],[c_90,c_100,c_90]) ).
tcf(c_117,plain,
! [X0: $i] :
( truthday(monday)
| truthday(X0)
| ~ day1(X0) ),
inference(renaming,[status(thm)],[c_116]) ).
tcf(c_654,plain,
! [X0: $i] :
( ~ iPr_def_10
| truthday(X0)
| ~ day3(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_97]) ).
tcf(c_655,plain,
( iPr_def_10
| truthday(friday)
| truthday(wednesday) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_97]) ).
tcf(c_656,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ truthday(X0)
| ~ day2(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_96]) ).
tcf(c_657,plain,
( iPr_def_11
| day2(sunday)
| day2(saturday)
| day2(thursday) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_96]) ).
tcf(c_658,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_660,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_661,plain,
! [X0: $i,X1: $i] :
( truthday(X0)
| ~ truthday(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_662,plain,
! [X0: $i,X1: $i] :
( day1(X0)
| ~ day1(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_663,plain,
! [X0: $i,X1: $i] :
( day2(X0)
| ~ day2(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_664,plain,
! [X0: $i,X1: $i] :
( day3(X0)
| ~ day3(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1357,plain,
( ~ truthday(wednesday)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_71,c_51]) ).
tcf(c_1358,plain,
( ~ truthday(thursday)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_71,c_52]) ).
tcf(c_1359,plain,
( ~ truthday(friday)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_71,c_53]) ).
tcf(c_1361,plain,
( ~ truthday(sunday)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_71,c_55]) ).
tcf(c_1367,plain,
( ~ truthday(thursday)
| ~ truthday(wednesday) ),
inference(resolution,[status(thm)],[c_71,c_61]) ).
tcf(c_1369,plain,
( ~ truthday(saturday)
| ~ truthday(wednesday) ),
inference(resolution,[status(thm)],[c_71,c_63]) ).
tcf(c_1370,plain,
( ~ truthday(sunday)
| ~ truthday(wednesday) ),
inference(resolution,[status(thm)],[c_71,c_64]) ).
tcf(c_1374,plain,
( ~ truthday(saturday)
| ~ truthday(friday) ),
inference(resolution,[status(thm)],[c_71,c_68]) ).
tcf(c_1375,plain,
( ~ truthday(sunday)
| ~ truthday(friday) ),
inference(resolution,[status(thm)],[c_71,c_69]) ).
tcf(c_1427,plain,
! [X0: $i] :
( ( X0 = sK0 )
| ~ truthday(sK0)
| ~ truthday(X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_1428,plain,
! [X0: $i] :
( ( X0 = friday )
| ~ truthday(friday)
| ~ truthday(X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_1429,plain,
! [X0: $i] :
( truthday(X0)
| ~ truthday(sK0)
| ( X0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_661]) ).
tcf(c_1430,plain,
( truthday(tuesday)
| ~ truthday(sK0)
| ( tuesday != sK0 ) ),
inference(instantiation,[status(thm)],[c_1429]) ).
tcf(c_1432,plain,
( ( monday = sunday )
| ( monday = saturday )
| ( monday = friday )
| ( monday = thursday )
| ( monday = wednesday )
| ( monday = tuesday )
| ( monday = monday ) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1436,plain,
( truthday(sunday)
| ~ day2(sunday) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_1474,plain,
! [X0: $i] :
( day1(X0)
| ~ day1(sK1)
| ( X0 != sK1 ) ),
inference(instantiation,[status(thm)],[c_662]) ).
tcf(c_1482,plain,
! [X0: $i] :
( day2(X0)
| ~ day2(sK2)
| ( X0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_663]) ).
tcf(c_1552,plain,
( day1(tuesday)
| ~ day2(wednesday) ),
inference(superposition,[status(thm)],[c_81,c_86]) ).
tcf(c_1556,plain,
( day1(saturday)
| ~ day2(sunday) ),
inference(superposition,[status(thm)],[c_85,c_86]) ).
tcf(c_1597,plain,
( day2(monday)
| ~ day1(sunday) ),
inference(superposition,[status(thm)],[c_79,c_87]) ).
tcf(c_1600,plain,
( day2(thursday)
| ~ day1(wednesday) ),
inference(superposition,[status(thm)],[c_82,c_87]) ).
tcf(c_1602,plain,
( day2(saturday)
| ~ day1(friday) ),
inference(superposition,[status(thm)],[c_84,c_87]) ).
tcf(c_1603,plain,
( day2(sunday)
| ~ day1(saturday) ),
inference(superposition,[status(thm)],[c_85,c_87]) ).
tcf(c_1645,plain,
( day2(sunday)
| ~ day3(monday) ),
inference(superposition,[status(thm)],[c_79,c_88]) ).
tcf(c_1648,plain,
( day2(wednesday)
| ~ day3(thursday) ),
inference(superposition,[status(thm)],[c_82,c_88]) ).
tcf(c_1651,plain,
( day2(saturday)
| ~ day3(sunday) ),
inference(superposition,[status(thm)],[c_85,c_88]) ).
tcf(c_1675,plain,
! [X0: $i] :
( ( X0 = sK2 )
| ~ truthday(sK2)
| ~ truthday(X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_1742,plain,
( ~ day2(thursday)
| ~ day2(monday) ),
inference(resolution,[status(thm)],[c_73,c_52]) ).
tcf(c_1744,plain,
( ~ day2(saturday)
| ~ day2(monday) ),
inference(resolution,[status(thm)],[c_73,c_54]) ).
tcf(c_1745,plain,
( ~ day2(sunday)
| ~ day2(monday) ),
inference(resolution,[status(thm)],[c_73,c_55]) ).
tcf(c_1751,plain,
( ~ day2(thursday)
| ~ day2(wednesday) ),
inference(resolution,[status(thm)],[c_73,c_61]) ).
tcf(c_1753,plain,
( ~ day2(saturday)
| ~ day2(wednesday) ),
inference(resolution,[status(thm)],[c_73,c_63]) ).
tcf(c_1754,plain,
( ~ day2(sunday)
| ~ day2(wednesday) ),
inference(resolution,[status(thm)],[c_73,c_64]) ).
tcf(c_1755,plain,
( ~ day2(friday)
| ~ day2(thursday) ),
inference(resolution,[status(thm)],[c_73,c_65]) ).
tcf(c_1758,plain,
( ~ day2(saturday)
| ~ day2(friday) ),
inference(resolution,[status(thm)],[c_73,c_68]) ).
tcf(c_1759,plain,
( ~ day2(sunday)
| ~ day2(friday) ),
inference(resolution,[status(thm)],[c_73,c_69]) ).
tcf(c_1762,plain,
( ( monday = sK0 )
| ~ truthday(sK0)
| ~ truthday(monday) ),
inference(instantiation,[status(thm)],[c_1427]) ).
tcf(c_1764,plain,
! [X0: $i] :
( ( X0 = monday )
| ~ truthday(monday)
| ~ truthday(X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_1774,plain,
! [X0: $i,X1: $i] :
( ( monday = X0 )
| ( monday != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_660]) ).
tcf(c_1776,plain,
( day3(monday)
| ~ day2(sunday) ),
inference(superposition,[status(thm)],[c_79,c_89]) ).
tcf(c_1780,plain,
( day3(friday)
| ~ day2(thursday) ),
inference(superposition,[status(thm)],[c_83,c_89]) ).
tcf(c_1782,plain,
( day3(sunday)
| ~ day2(saturday) ),
inference(superposition,[status(thm)],[c_85,c_89]) ).
tcf(c_1801,plain,
! [X0: $i,X1: $i] :
( ( friday = X0 )
| ( friday != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_660]) ).
tcf(c_1805,plain,
( truthday(sK2)
| ~ day2(thursday) ),
inference(superposition,[status(thm)],[c_77,c_93]) ).
tcf(c_1817,plain,
( iPr_def_11
| day2(saturday)
| day2(thursday)
| ~ day2(monday) ),
inference(resolution,[status(thm)],[c_1745,c_657]) ).
tcf(c_1818,plain,
( iPr_def_11
| ~ day2(monday) ),
inference(global_subsumption_just,[status(thm)],[c_1817,c_1742,c_1744,c_1817]) ).
tcf(c_1830,plain,
( truthday(sK2)
| ~ day2(saturday) ),
inference(superposition,[status(thm)],[c_77,c_94]) ).
tcf(c_1876,plain,
( iPr_def_11
| day2(saturday)
| day2(thursday)
| ~ day2(wednesday) ),
inference(resolution,[status(thm)],[c_1754,c_657]) ).
tcf(c_1877,plain,
( iPr_def_11
| ~ day2(wednesday) ),
inference(global_subsumption_just,[status(thm)],[c_1876,c_1751,c_1753,c_1876]) ).
tcf(c_1901,plain,
( iPr_def_11
| day2(saturday)
| day2(thursday)
| ~ day2(friday) ),
inference(resolution,[status(thm)],[c_1759,c_657]) ).
tcf(c_1902,plain,
( iPr_def_11
| ~ day2(friday) ),
inference(global_subsumption_just,[status(thm)],[c_1901,c_1755,c_1758,c_1901]) ).
tcf(c_1905,plain,
( iPr_def_10
| truthday(wednesday)
| ~ day3(friday)
| ~ truthday(friday) ),
inference(superposition,[status(thm)],[c_655,c_99]) ).
tcf(c_1909,plain,
( ~ iPr_def_11
| ~ day2(sK2)
| ~ truthday(sK2) ),
inference(instantiation,[status(thm)],[c_656]) ).
tcf(c_1911,plain,
! [X0: $i] :
( ( X0 = sK0 )
| ~ truthday(X0) ),
inference(superposition,[status(thm)],[c_75,c_71]) ).
tcf(c_1912,plain,
! [X0: $i] :
( iPr_def_10
| truthday(wednesday)
| ( X0 = friday )
| ~ truthday(X0) ),
inference(superposition,[status(thm)],[c_655,c_71]) ).
tcf(c_2111,plain,
( truthday(sK1)
| truthday(monday) ),
inference(superposition,[status(thm)],[c_76,c_117]) ).
tcf(c_2116,plain,
! [X0: $i] :
( truthday(monday)
| ( X0 = sK1 )
| ~ truthday(X0) ),
inference(superposition,[status(thm)],[c_2111,c_71]) ).
tcf(c_2117,plain,
( truthday(monday)
| ~ day3(sK1)
| ~ truthday(friday) ),
inference(superposition,[status(thm)],[c_2111,c_99]) ).
tcf(c_2118,plain,
( truthday(monday)
| ~ day3(sK1)
| ~ truthday(wednesday) ),
inference(superposition,[status(thm)],[c_2111,c_98]) ).
tcf(c_2125,plain,
( truthday(sK3)
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_78,c_654]) ).
tcf(c_2126,plain,
! [X0: $i] :
( truthday(consecutive(X0))
| ~ iPr_def_10
| ~ day2(X0) ),
inference(superposition,[status(thm)],[c_89,c_654]) ).
tcf(c_2180,plain,
( ~ truthday(sK1)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_91,c_76]) ).
tcf(c_2182,plain,
( ~ iPr_def_10
| ~ day3(sK3)
| ~ truthday(friday) ),
inference(superposition,[status(thm)],[c_2125,c_99]) ).
tcf(c_2305,plain,
( iPr_def_11
| day2(saturday)
| day2(thursday)
| day1(saturday) ),
inference(superposition,[status(thm)],[c_657,c_1556]) ).
tcf(c_2315,plain,
( truthday(monday)
| ~ truthday(sK0)
| ( monday != sK0 ) ),
inference(instantiation,[status(thm)],[c_1429]) ).
tcf(c_2394,plain,
! [X0: $i] :
( iPr_def_11
| ~ day2(X0)
| ( monday != X0 ) ),
inference(resolution,[status(thm)],[c_663,c_1818]) ).
tcf(c_2395,plain,
! [X0: $i] :
( iPr_def_11
| ~ day2(X0)
| ( wednesday != X0 ) ),
inference(resolution,[status(thm)],[c_663,c_1877]) ).
tcf(c_2400,plain,
! [X0: $i] :
( iPr_def_11
| ~ day2(X0)
| ( friday != X0 ) ),
inference(resolution,[status(thm)],[c_663,c_1902]) ).
tcf(c_2449,plain,
( truthday(sunday)
| ( saturday = sK0 )
| ( friday = sK0 )
| ( thursday = sK0 )
| ( wednesday = sK0 )
| ( tuesday = sK0 )
| ( monday = sK0 ) ),
inference(superposition,[status(thm)],[c_49,c_75]) ).
tcf(c_2496,plain,
! [X0: $i] :
( ( monday = X0 )
| ( monday != monday )
| ( X0 != monday ) ),
inference(instantiation,[status(thm)],[c_1774]) ).
tcf(c_2497,plain,
! [X0: $i] :
( ( monday = X0 )
| ( monday != sK0 )
| ( X0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_1774]) ).
tcf(c_2529,plain,
( ~ truthday(friday)
| ~ day3(sK1) ),
inference(global_subsumption_just,[status(thm)],[c_2117,c_1359,c_2117]) ).
tcf(c_2530,plain,
( ~ day3(sK1)
| ~ truthday(friday) ),
inference(renaming,[status(thm)],[c_2529]) ).
tcf(c_2531,plain,
( iPr_def_10
| truthday(wednesday)
| ~ day3(sK1) ),
inference(superposition,[status(thm)],[c_655,c_2530]) ).
tcf(c_2539,plain,
! [X0: $i] :
( ( friday = X0 )
| ( friday != friday )
| ( X0 != friday ) ),
inference(instantiation,[status(thm)],[c_1801]) ).
tcf(c_2540,plain,
friday = friday,
inference(instantiation,[status(thm)],[c_658]) ).
tcf(c_2543,plain,
( ~ truthday(wednesday)
| ~ day3(sK1) ),
inference(global_subsumption_just,[status(thm)],[c_2118,c_1357,c_2118]) ).
tcf(c_2544,plain,
( ~ day3(sK1)
| ~ truthday(wednesday) ),
inference(renaming,[status(thm)],[c_2543]) ).
tcf(c_2548,plain,
( truthday(monday)
| ~ iPr_def_10
| ~ day2(sunday) ),
inference(superposition,[status(thm)],[c_79,c_2126]) ).
tcf(c_2549,plain,
( truthday(tuesday)
| ~ iPr_def_10
| ~ day2(monday) ),
inference(superposition,[status(thm)],[c_80,c_2126]) ).
tcf(c_2551,plain,
( truthday(thursday)
| ~ iPr_def_10
| ~ day2(wednesday) ),
inference(superposition,[status(thm)],[c_82,c_2126]) ).
tcf(c_2552,plain,
( truthday(friday)
| ~ iPr_def_10
| ~ day2(thursday) ),
inference(superposition,[status(thm)],[c_83,c_2126]) ).
tcf(c_2580,plain,
( ~ day2(thursday)
| ~ truthday(wednesday) ),
inference(resolution,[status(thm)],[c_93,c_1367]) ).
tcf(c_2629,plain,
( ~ day2(saturday)
| ~ truthday(friday) ),
inference(resolution,[status(thm)],[c_94,c_1374]) ).
tcf(c_2631,plain,
( ~ day2(saturday)
| ~ truthday(wednesday) ),
inference(resolution,[status(thm)],[c_94,c_1369]) ).
tcf(c_2674,plain,
! [X0: $i] :
( iPr_def_11
| ~ day3(monday)
| ~ day3(X0)
| ~ day2(X0) ),
inference(resolution,[status(thm)],[c_2394,c_74]) ).
tcf(c_2682,plain,
~ day3(monday),
inference(global_subsumption_just,[status(thm)],[c_2674,c_655,c_1361,c_1370,c_1375,c_1436,c_1645,c_2548]) ).
tcf(c_2730,plain,
( ~ day2(sunday)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_95,c_1361]) ).
tcf(c_2731,plain,
~ day2(sunday),
inference(global_subsumption_just,[status(thm)],[c_2730,c_1776,c_2682]) ).
tcf(c_2735,plain,
! [X0: $i] :
( ~ day2(X0)
| ( sunday != X0 ) ),
inference(resolution,[status(thm)],[c_2731,c_663]) ).
tcf(c_2737,plain,
( iPr_def_11
| day2(saturday)
| day2(thursday) ),
inference(resolution,[status(thm)],[c_2731,c_657]) ).
tcf(c_2747,plain,
! [X0: $i] :
( ~ day3(sunday)
| ~ day3(X0)
| ~ day2(X0) ),
inference(resolution,[status(thm)],[c_2735,c_74]) ).
tcf(c_2751,plain,
! [X0: $i] :
( ~ day3(sunday)
| ~ day3(X0) ),
inference(global_subsumption_just,[status(thm)],[c_2747,c_77,c_97,c_1482,c_1651,c_1675,c_1830,c_2631,c_2629,c_2747]) ).
tcf(c_2756,plain,
~ day3(sunday),
inference(factoring,[status(thm)],[c_2751]) ).
tcf(c_2772,plain,
( ~ truthday(sK3)
| ~ truthday(friday) ),
inference(resolution,[status(thm)],[c_99,c_78]) ).
tcf(c_2786,plain,
( iPr_def_11
| day2(thursday)
| ~ day2(monday) ),
inference(resolution,[status(thm)],[c_2737,c_1744]) ).
tcf(c_2787,plain,
( iPr_def_11
| day2(thursday) ),
inference(global_subsumption_just,[status(thm)],[c_2786,c_1603,c_1782,c_1776,c_2305,c_2682,c_2756]) ).
tcf(c_2792,plain,
( iPr_def_11
| ~ truthday(wednesday) ),
inference(resolution,[status(thm)],[c_2787,c_2580]) ).
tcf(c_2801,plain,
! [X0: $i] :
( iPr_def_11
| ~ day1(wednesday)
| ~ day2(X0)
| ~ day1(X0) ),
inference(resolution,[status(thm)],[c_2395,c_72]) ).
tcf(c_2803,plain,
! [X0: $i] :
( iPr_def_11
| ~ day2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_2801,c_93,c_1428,c_1912,c_2400,c_2539,c_2540,c_2552,c_2787,c_2792]) ).
tcf(c_2811,plain,
( ~ day2(sK3)
| ~ day2(thursday)
| ~ truthday(friday) ),
inference(resolution,[status(thm)],[c_2772,c_93]) ).
tcf(c_2812,plain,
( ~ day2(sK3)
| ~ day2(thursday) ),
inference(global_subsumption_just,[status(thm)],[c_2811,c_78,c_655,c_1780,c_1905,c_2182,c_2552,c_2580]) ).
tcf(c_2822,plain,
iPr_def_11,
inference(resolution,[status(thm)],[c_2803,c_77]) ).
tcf(c_2827,plain,
( ~ day2(thursday)
| ~ day3(consecutive(sK3)) ),
inference(resolution,[status(thm)],[c_2812,c_88]) ).
tcf(c_2828,plain,
~ day2(thursday),
inference(global_subsumption_just,[status(thm)],[c_2827,c_77,c_1805,c_1909,c_2822]) ).
tcf(c_2831,plain,
! [X0: $i] :
( ~ day2(X0)
| ( thursday != X0 ) ),
inference(resolution,[status(thm)],[c_2828,c_663]) ).
tcf(c_2837,plain,
! [X0: $i] :
( ~ day3(thursday)
| ~ day3(X0)
| ~ day2(X0) ),
inference(resolution,[status(thm)],[c_2831,c_74]) ).
tcf(c_2843,plain,
~ day3(thursday),
inference(global_subsumption_just,[status(thm)],[c_2837,c_100,c_109,c_655,c_1357,c_1358,c_1359,c_1552,c_1648,c_2551]) ).
tcf(c_3058,plain,
( ~ iPr_def_10
| ~ day3(sK1)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_654,c_2180]) ).
tcf(c_3059,plain,
( ~ truthday(monday)
| ~ day3(sK1) ),
inference(global_subsumption_just,[status(thm)],[c_3058,c_2531,c_2544,c_3058]) ).
tcf(c_3060,plain,
( ~ day3(sK1)
| ~ truthday(monday) ),
inference(renaming,[status(thm)],[c_3059]) ).
tcf(c_3100,plain,
( iPr_def_10
| truthday(wednesday)
| ~ truthday(monday) ),
inference(resolution,[status(thm)],[c_655,c_1359]) ).
tcf(c_3101,plain,
( iPr_def_10
| ~ truthday(monday) ),
inference(global_subsumption_just,[status(thm)],[c_3100,c_1357,c_3100]) ).
tcf(c_3108,plain,
! [X0: $i] :
( iPr_def_10
| truthday(X0)
| ~ day1(X0) ),
inference(resolution,[status(thm)],[c_3101,c_117]) ).
tcf(c_3117,plain,
! [X0: $i] :
( ( wednesday != X0 )
| ( monday != X0 ) ),
inference(resolution,[status(thm)],[c_660,c_51]) ).
tcf(c_3119,plain,
! [X0: $i] :
( ( friday != X0 )
| ( monday != X0 ) ),
inference(resolution,[status(thm)],[c_660,c_53]) ).
tcf(c_3132,plain,
! [X0: $i] :
( ( thursday != X0 )
| ( wednesday != X0 ) ),
inference(resolution,[status(thm)],[c_660,c_61]) ).
tcf(c_3140,plain,
! [X0: $i] :
( ( friday != X0 )
| ( thursday != X0 ) ),
inference(resolution,[status(thm)],[c_660,c_65]) ).
tcf(c_3144,plain,
! [X0: $i] :
( ( sunday != X0 )
| ( thursday != X0 ) ),
inference(resolution,[status(thm)],[c_660,c_67]) ).
tcf(c_3190,plain,
! [X0: $i] :
( ~ day1(wednesday)
| ~ day1(X0)
| ( monday != X0 ) ),
inference(resolution,[status(thm)],[c_3117,c_72]) ).
tcf(c_3192,plain,
~ day1(wednesday),
inference(global_subsumption_just,[status(thm)],[c_3190,c_77,c_1600,c_1805,c_1909,c_2822]) ).
tcf(c_3199,plain,
! [X0: $i] :
( ~ day1(X0)
| ( wednesday != X0 ) ),
inference(resolution,[status(thm)],[c_3192,c_662]) ).
tcf(c_3225,plain,
! [X0: $i] :
( ~ day1(friday)
| ~ day1(X0)
| ( monday != X0 ) ),
inference(resolution,[status(thm)],[c_3119,c_72]) ).
tcf(c_3227,plain,
~ day1(friday),
inference(global_subsumption_just,[status(thm)],[c_3225,c_1602,c_1782,c_2756]) ).
tcf(c_3232,plain,
! [X0: $i] :
( ~ day1(X0)
| ( friday != X0 ) ),
inference(resolution,[status(thm)],[c_3227,c_662]) ).
tcf(c_3307,plain,
! [X0: $i] :
( ~ truthday(thursday)
| ~ truthday(X0)
| ( wednesday != X0 ) ),
inference(resolution,[status(thm)],[c_3132,c_71]) ).
tcf(c_3308,plain,
! [X0: $i] :
( ( wednesday != X0 )
| ~ truthday(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3307,c_76,c_75,c_1427,c_1474,c_1762,c_2116,c_2497,c_3117,c_3199]) ).
tcf(c_3309,plain,
! [X0: $i] :
( ~ truthday(X0)
| ( wednesday != X0 ) ),
inference(renaming,[status(thm)],[c_3308]) ).
tcf(c_3325,plain,
! [X0: $i] :
( ~ truthday(wednesday)
| ~ day1(X0)
| ~ truthday(X0) ),
inference(resolution,[status(thm)],[c_3199,c_71]) ).
tcf(c_3326,plain,
! [X0: $i] :
( ~ truthday(wednesday)
| ~ day1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3325,c_100,c_90,c_1357,c_3325]) ).
tcf(c_3364,plain,
! [X0: $i] :
( ~ truthday(friday)
| ~ truthday(X0)
| ( thursday != X0 ) ),
inference(resolution,[status(thm)],[c_3140,c_71]) ).
tcf(c_3365,plain,
! [X0: $i] :
( ~ truthday(friday)
| ~ truthday(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3364,c_76,c_1359,c_1428,c_1474,c_2116,c_2539,c_2540,c_3232]) ).
tcf(c_3382,plain,
! [X0: $i] :
( ~ day1(sunday)
| ~ day1(X0)
| ( thursday != X0 ) ),
inference(resolution,[status(thm)],[c_3144,c_72]) ).
tcf(c_3384,plain,
! [X0: $i] :
( ~ day1(sunday)
| ~ day1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3382,c_100,c_1597,c_1912,c_2539,c_2540,c_2549,c_3108,c_3232,c_3326]) ).
tcf(c_3480,plain,
~ day1(sunday),
inference(factoring,[status(thm)],[c_3384]) ).
tcf(c_3487,plain,
! [X0: $i] :
( ~ day1(X0)
| ( sunday != X0 ) ),
inference(resolution,[status(thm)],[c_3480,c_662]) ).
tcf(c_3504,plain,
~ truthday(wednesday),
inference(resolution,[status(thm)],[c_3309,c_658]) ).
tcf(c_3510,plain,
~ truthday(friday),
inference(factoring,[status(thm)],[c_3365]) ).
tcf(c_3567,plain,
! [X0: $i] :
( ~ truthday(sunday)
| ~ day1(X0)
| ~ truthday(X0) ),
inference(resolution,[status(thm)],[c_3487,c_71]) ).
tcf(c_3568,plain,
! [X0: $i] :
( ~ truthday(sunday)
| ~ day1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3567,c_100,c_90,c_1361,c_3567]) ).
tcf(c_3600,plain,
~ truthday(sunday),
inference(resolution,[status(thm)],[c_3568,c_76]) ).
tcf(c_3701,plain,
! [X0: $i] :
( ~ day3(X0)
| ( monday != X0 ) ),
inference(resolution,[status(thm)],[c_664,c_2682]) ).
tcf(c_3703,plain,
! [X0: $i] :
( ~ day3(X0)
| ( thursday != X0 ) ),
inference(resolution,[status(thm)],[c_664,c_2843]) ).
tcf(c_3714,plain,
! [X0: $i] :
( ~ truthday(monday)
| ~ day3(X0)
| ( sK1 != X0 ) ),
inference(resolution,[status(thm)],[c_664,c_3060]) ).
tcf(c_3715,plain,
! [X0: $i] :
( ~ truthday(monday)
| ~ day3(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3714,c_55,c_54,c_53,c_52,c_51,c_50,c_97,c_1432,c_1764,c_2496,c_3504,c_3510,c_3701]) ).
tcf(c_3868,plain,
! [X0: $i] :
( ~ truthday(thursday)
| ~ day3(X0)
| ~ truthday(X0) ),
inference(resolution,[status(thm)],[c_3703,c_71]) ).
tcf(c_3869,plain,
! [X0: $i] :
( ~ truthday(thursday)
| ~ day3(X0) ),
inference(global_subsumption_just,[status(thm)],[c_3868,c_97,c_3504,c_3510,c_3868]) ).
tcf(c_4175,plain,
~ truthday(monday),
inference(resolution,[status(thm)],[c_3715,c_78]) ).
tcf(c_4931,plain,
~ truthday(thursday),
inference(resolution,[status(thm)],[c_3869,c_78]) ).
tcf(c_5049,plain,
! [X0: $i] :
( ~ day1(X0)
| truthday(X0) ),
inference(global_subsumption_just,[status(thm)],[c_117,c_100,c_90,c_4175]) ).
tcf(c_5050,plain,
! [X0: $i] :
( truthday(X0)
| ~ day1(X0) ),
inference(renaming,[status(thm)],[c_5049]) ).
tcf(c_5051,plain,
truthday(sK1),
inference(superposition,[status(thm)],[c_76,c_5050]) ).
tcf(c_5053,plain,
! [X0: $i] :
( ~ day3(X0)
| truthday(X0) ),
inference(global_subsumption_just,[status(thm)],[c_654,c_97,c_3504,c_3510]) ).
tcf(c_5054,plain,
! [X0: $i] :
( truthday(X0)
| ~ day3(X0) ),
inference(renaming,[status(thm)],[c_5053]) ).
tcf(c_5055,plain,
truthday(sK3),
inference(superposition,[status(thm)],[c_78,c_5054]) ).
tcf(c_5067,plain,
sK0 = sK1,
inference(superposition,[status(thm)],[c_5051,c_1911]) ).
tcf(c_5068,plain,
sK0 = sK3,
inference(superposition,[status(thm)],[c_5055,c_1911]) ).
tcf(c_5091,plain,
( truthday(sunday)
| ( saturday = sK0 )
| ( friday = sK0 )
| ( thursday = sK0 )
| ( wednesday = sK0 )
| ( tuesday = sK0 )
| ( monday = sK0 ) ),
inference(superposition,[status(thm)],[c_49,c_75]) ).
tcf(c_5124,plain,
day1(sK0),
inference(superposition,[status(thm)],[c_5067,c_76]) ).
tcf(c_5125,plain,
( day1(sunday)
| ( saturday = sK0 )
| ( friday = sK0 )
| ( thursday = sK0 )
| ( wednesday = sK0 )
| ( tuesday = sK0 )
| ( monday = sK0 ) ),
inference(superposition,[status(thm)],[c_49,c_5124]) ).
tcf(c_5133,plain,
day3(sK0),
inference(superposition,[status(thm)],[c_5068,c_78]) ).
tcf(c_5134,plain,
( day3(sunday)
| ( saturday = sK0 )
| ( friday = sK0 )
| ( thursday = sK0 )
| ( wednesday = sK0 )
| ( tuesday = sK0 )
| ( monday = sK0 ) ),
inference(superposition,[status(thm)],[c_49,c_5133]) ).
tcf(c_5177,plain,
( ( wednesday = sK0 )
| ( thursday = sK0 )
| ( friday = sK0 )
| ( saturday = sK0 ) ),
inference(global_subsumption_just,[status(thm)],[c_5091,c_75,c_100,c_1430,c_2315,c_2449,c_3600,c_4175]) ).
tcf(c_5178,plain,
( ( saturday = sK0 )
| ( friday = sK0 )
| ( thursday = sK0 )
| ( wednesday = sK0 ) ),
inference(renaming,[status(thm)],[c_5177]) ).
tcf(c_5181,plain,
( day1(saturday)
| ( friday = sK0 )
| ( thursday = sK0 )
| ( wednesday = sK0 ) ),
inference(superposition,[status(thm)],[c_5178,c_5124]) ).
tcf(c_5183,plain,
( ( friday = sK0 )
| ( thursday = sK0 )
| ( wednesday = sK0 ) ),
inference(global_subsumption_just,[status(thm)],[c_5125,c_655,c_1361,c_1370,c_1375,c_1436,c_1603,c_2548,c_5181]) ).
tcf(c_5187,plain,
( day1(friday)
| ( thursday = sK0 )
| ( wednesday = sK0 ) ),
inference(superposition,[status(thm)],[c_5183,c_5124]) ).
tcf(c_5189,plain,
( ( wednesday = sK0 )
| ( thursday = sK0 ) ),
inference(global_subsumption_just,[status(thm)],[c_5134,c_1602,c_1782,c_2756,c_5187]) ).
tcf(c_5190,plain,
( ( thursday = sK0 )
| ( wednesday = sK0 ) ),
inference(renaming,[status(thm)],[c_5189]) ).
tcf(c_5192,plain,
( day3(thursday)
| ( wednesday = sK0 ) ),
inference(superposition,[status(thm)],[c_5190,c_5133]) ).
tcf(c_5194,plain,
( truthday(thursday)
| ( wednesday = sK0 ) ),
inference(superposition,[status(thm)],[c_5190,c_75]) ).
tcf(c_5195,plain,
wednesday = sK0,
inference(global_subsumption_just,[status(thm)],[c_5192,c_4931,c_5194]) ).
tcf(c_5200,plain,
truthday(wednesday),
inference(superposition,[status(thm)],[c_5195,c_75]) ).
tcf(c_5201,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_5200,c_3504]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.39 % Computer : n003.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Thu Sep 24 06:58:21 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.46
% 0.11/0.46 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.46
% 0.11/0.46 % Detected problem language: tptp
% 0.11/0.47 % Proving...
% 2.79/1.36 % SZS status Started for theBenchmark.p
% 2.79/1.36 % SZS status Theorem for theBenchmark.p
% 2.79/1.36
% 2.79/1.36 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.79/1.36
% 2.79/1.36 % ------ iProver source info
% 2.79/1.36
% 2.79/1.36 % git: date: 2026-07-19 20:42:38 +0200
% 2.79/1.36 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.79/1.36 % git: non_committed_changes: false
% 2.79/1.36
% 2.79/1.36 % ------ Parsing...
% 2.79/1.36 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.79/1.36
% 2.79/1.36 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 2.79/1.36
% 2.79/1.36 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.79/1.36
% 2.79/1.36 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.79/1.36 % ------ Proving...
% 2.79/1.36 % ------ Problem Properties
% 2.79/1.36
% 2.79/1.36 %
% 2.79/1.36 % clauses 53
% 2.79/1.36 % conjectures 1
% 2.79/1.36 % EPR 42
% 2.79/1.36 % Horn 49
% 2.79/1.36 % unary 33
% 2.79/1.36 % binary 4
% 2.79/1.36 % lits 94
% 2.79/1.36 % lits eq 39
% 2.79/1.36 % fd_pure 1
% 2.79/1.36 % fd_pseudo 0
% 2.79/1.36 % fd_cond 0
% 2.79/1.36 % fd_pseudo_cond 4
% 2.79/1.36 % AC symbols 0
% 2.79/1.36
% 2.79/1.36 % ------ Input Options Time Limit: Unbounded
% 2.79/1.36
% 2.79/1.36
% 2.79/1.36 % ------
% 2.79/1.36 % Current options:
% 2.79/1.36 % ------
% 2.79/1.36
% 2.79/1.36
% 2.79/1.36 %
% 2.79/1.36
% 2.79/1.36 % ------ Proving...
% 2.79/1.36 %
% 2.79/1.36
% 2.79/1.36 % SZS status Theorem for theBenchmark.p
% 2.79/1.36
% 2.79/1.36 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.79/1.36
% 2.79/1.36
%------------------------------------------------------------------------------