%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:00:04 PM UTC 2026
% Result : Theorem 0.14s 0.48s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 94
% Syntax : Number of formulae : 536 ( 67 unt; 71 def)
% Number of atoms : 1461 ( 373 equ)
% Maximal formula atoms : 21 ( 2 avg)
% Number of connectives : 1576 ( 651 ~; 800 |; 39 &)
% ( 79 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 77 ( 75 usr; 72 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-1 aty)
% Number of variables : 102 ( 98 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( X = sunday
| X = saturday
| X = friday
| X = thursday
| X = wednesday
| X = tuesday
| X = monday ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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') ).
fof(f3,axiom,
! [X,Y] :
( ( truthday(Y)
& truthday(X) )
=> X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( ( day1(Y)
& day1(X) )
=> X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] :
( ( day2(Y)
& day2(X) )
=> X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] :
( ( day3(Y)
& day3(X) )
=> X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
? [X] : truthday(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
? [X] : day1(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
? [X] : day2(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
? [X] : day3(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
consecutive(sunday) = monday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
consecutive(monday) = tuesday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
consecutive(tuesday) = wednesday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
consecutive(wednesday) = thursday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
consecutive(thursday) = friday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
consecutive(friday) = saturday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
consecutive(saturday) = sunday,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X] :
( day1(X)
<=> day2(consecutive(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X] :
( day2(X)
<=> day3(consecutive(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X] :
( day1(X)
=> ( truthday(X)
<=> ( ~ truthday(tuesday)
& ~ truthday(monday) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X] :
( day2(X)
=> ( truthday(X)
<=> ( day2(sunday)
| day2(saturday)
| day2(thursday) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] :
( day3(X)
=> ( truthday(X)
<=> ( ~ truthday(friday)
& ~ truthday(wednesday) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,conjecture,
truthday(tuesday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
~ truthday(tuesday),
inference(negated_conjecture,[status(cth)],[f23]) ).
fof(f25,plain,
! [X0] :
( X0 = sunday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = wednesday
| X0 = tuesday
| X0 = monday ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f26,plain,
monday != tuesday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f27,plain,
monday != wednesday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f28,plain,
monday != thursday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f29,plain,
monday != friday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f30,plain,
monday != saturday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f31,plain,
monday != sunday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f32,plain,
tuesday != wednesday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f33,plain,
tuesday != thursday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f34,plain,
tuesday != friday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f35,plain,
tuesday != saturday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f36,plain,
tuesday != sunday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f37,plain,
wednesday != thursday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f38,plain,
wednesday != friday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f39,plain,
wednesday != saturday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f40,plain,
wednesday != sunday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f41,plain,
thursday != friday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f42,plain,
thursday != saturday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f43,plain,
thursday != sunday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f44,plain,
friday != saturday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
friday != sunday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f46,plain,
saturday != sunday,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f47,plain,
! [X,Y] :
( X = Y
| ~ truthday(Y)
| ~ truthday(X) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f48,plain,
! [X0,X1] :
( X0 = X1
| ~ truthday(X1)
| ~ truthday(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [X,Y] :
( X = Y
| ~ day1(Y)
| ~ day1(X) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f50,plain,
! [X0,X1] :
( X0 = X1
| ~ day1(X1)
| ~ day1(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [X,Y] :
( X = Y
| ~ day2(Y)
| ~ day2(X) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f52,plain,
! [X0,X1] :
( X0 = X1
| ~ day2(X1)
| ~ day2(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
! [X,Y] :
( X = Y
| ~ day3(Y)
| ~ day3(X) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f54,plain,
! [X0,X1] :
( X0 = X1
| ~ day3(X1)
| ~ day3(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
truthday(sK0_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl)],[f7]) ).
fof(f56,plain,
truthday(sK0_skl),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
day1(sK1_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl)],[f8]) ).
fof(f58,plain,
day1(sK1_skl),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
day2(sK2_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X,sK2_skl)],[f9]) ).
fof(f60,plain,
day2(sK2_skl),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
day3(sK3_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl)],[f10]) ).
fof(f62,plain,
day3(sK3_skl),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
consecutive(sunday) = monday,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f64,plain,
consecutive(monday) = tuesday,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f65,plain,
consecutive(tuesday) = wednesday,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f66,plain,
consecutive(wednesday) = thursday,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f67,plain,
consecutive(thursday) = friday,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f68,plain,
consecutive(friday) = saturday,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f69,plain,
consecutive(saturday) = sunday,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f70,plain,
! [X] :
( ( ~ day2(consecutive(X))
| day1(X) )
& ( day2(consecutive(X))
| ~ day1(X) ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f71,plain,
( ! [X] :
( ~ day2(consecutive(X))
| day1(X) )
& ! [X] :
( day2(consecutive(X))
| ~ day1(X) ) ),
inference(miniscoping,[status(thm)],[f70]) ).
fof(f72,plain,
! [X0] :
( day2(consecutive(X0))
| ~ day1(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0] :
( ~ day2(consecutive(X0))
| day1(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [X] :
( ( ~ day3(consecutive(X))
| day2(X) )
& ( day3(consecutive(X))
| ~ day2(X) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f75,plain,
( ! [X] :
( ~ day3(consecutive(X))
| day2(X) )
& ! [X] :
( day3(consecutive(X))
| ~ day2(X) ) ),
inference(miniscoping,[status(thm)],[f74]) ).
fof(f76,plain,
! [X0] :
( day3(consecutive(X0))
| ~ day2(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [X0] :
( ~ day3(consecutive(X0))
| day2(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f78,plain,
! [X] :
( ( truthday(X)
<=> ( ~ truthday(tuesday)
& ~ truthday(monday) ) )
| ~ day1(X) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f79,plain,
! [X] :
( ( ( truthday(tuesday)
| truthday(monday)
| truthday(X) )
& ( ( ~ truthday(tuesday)
& ~ truthday(monday) )
| ~ truthday(X) ) )
| ~ day1(X) ),
inference(NNF_transformation,[status(thm)],[f78]) ).
fof(f80,plain,
! [X0] :
( ~ truthday(monday)
| ~ truthday(X0)
| ~ day1(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
! [X0] :
( truthday(tuesday)
| truthday(monday)
| truthday(X0)
| ~ day1(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f83,plain,
! [X] :
( ( truthday(X)
<=> ( day2(sunday)
| day2(saturday)
| day2(thursday) ) )
| ~ day2(X) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f84,plain,
! [X] :
( ( ( ( ~ day2(sunday)
& ~ day2(saturday)
& ~ day2(thursday) )
| truthday(X) )
& ( day2(sunday)
| day2(saturday)
| day2(thursday)
| ~ truthday(X) ) )
| ~ day2(X) ),
inference(NNF_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
! [X0] :
( day2(sunday)
| day2(saturday)
| day2(thursday)
| ~ truthday(X0)
| ~ day2(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f86,plain,
! [X0] :
( ~ day2(thursday)
| truthday(X0)
| ~ day2(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f87,plain,
! [X0] :
( ~ day2(saturday)
| truthday(X0)
| ~ day2(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f88,plain,
! [X0] :
( ~ day2(sunday)
| truthday(X0)
| ~ day2(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f89,plain,
! [X] :
( ( truthday(X)
<=> ( ~ truthday(friday)
& ~ truthday(wednesday) ) )
| ~ day3(X) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f90,plain,
! [X] :
( ( ( truthday(friday)
| truthday(wednesday)
| truthday(X) )
& ( ( ~ truthday(friday)
& ~ truthday(wednesday) )
| ~ truthday(X) ) )
| ~ day3(X) ),
inference(NNF_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [X0] :
( ~ truthday(wednesday)
| ~ truthday(X0)
| ~ day3(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0] :
( ~ truthday(friday)
| ~ truthday(X0)
| ~ day3(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f93,plain,
! [X0] :
( truthday(friday)
| truthday(wednesday)
| truthday(X0)
| ~ day3(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f94,plain,
~ truthday(tuesday),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f95,definition,
! [X0] :
( sQ0_spl
<=> ( ~ truthday(X0)
| ~ day1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f96,plain,
! [X0] :
( ~ sQ0_spl
| ~ truthday(X0)
| ~ day1(X0) ),
inference(component_clause,[status(thm)],[f95]) ).
fof(f98,definition,
( sQ1_spl
<=> truthday(monday) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f99,plain,
( ~ sQ1_spl
| truthday(monday) ),
inference(component_clause,[status(thm)],[f98]) ).
fof(f100,plain,
( sQ1_spl
| ~ truthday(monday) ),
inference(component_clause,[status(thm)],[f98]) ).
fof(f101,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f80,f95,f98]) ).
fof(f102,definition,
( sQ2_spl
<=> truthday(tuesday) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f103,plain,
( ~ sQ2_spl
| truthday(tuesday) ),
inference(component_clause,[status(thm)],[f102]) ).
fof(f106,definition,
! [X0] :
( sQ3_spl
<=> ( truthday(X0)
| ~ day1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f107,plain,
! [X0] :
( ~ sQ3_spl
| truthday(X0)
| ~ day1(X0) ),
inference(component_clause,[status(thm)],[f106]) ).
fof(f109,plain,
( sQ2_spl
| sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f82,f106,f98,f102]) ).
fof(f110,definition,
! [X0] :
( sQ4_spl
<=> ( ~ truthday(X0)
| ~ day2(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f111,plain,
! [X0] :
( ~ sQ4_spl
| ~ truthday(X0)
| ~ day2(X0) ),
inference(component_clause,[status(thm)],[f110]) ).
fof(f113,definition,
( sQ5_spl
<=> day2(thursday) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f114,plain,
( ~ sQ5_spl
| day2(thursday) ),
inference(component_clause,[status(thm)],[f113]) ).
fof(f115,plain,
( sQ5_spl
| ~ day2(thursday) ),
inference(component_clause,[status(thm)],[f113]) ).
fof(f116,definition,
( sQ6_spl
<=> day2(saturday) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f117,plain,
( ~ sQ6_spl
| day2(saturday) ),
inference(component_clause,[status(thm)],[f116]) ).
fof(f118,plain,
( sQ6_spl
| ~ day2(saturday) ),
inference(component_clause,[status(thm)],[f116]) ).
fof(f119,definition,
( sQ7_spl
<=> day2(sunday) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f121,plain,
( sQ7_spl
| ~ day2(sunday) ),
inference(component_clause,[status(thm)],[f119]) ).
fof(f122,plain,
( sQ7_spl
| sQ6_spl
| sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f85,f110,f113,f116,f119]) ).
fof(f123,definition,
! [X0] :
( sQ8_spl
<=> ( truthday(X0)
| ~ day2(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f124,plain,
! [X0] :
( ~ sQ8_spl
| truthday(X0)
| ~ day2(X0) ),
inference(component_clause,[status(thm)],[f123]) ).
fof(f126,plain,
( ~ sQ5_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f86,f123,f113]) ).
fof(f127,plain,
( ~ sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f87,f123,f116]) ).
fof(f128,plain,
( ~ sQ7_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f88,f123,f119]) ).
fof(f129,definition,
! [X0] :
( sQ9_spl
<=> ( ~ truthday(X0)
| ~ day3(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f130,plain,
! [X0] :
( ~ sQ9_spl
| ~ truthday(X0)
| ~ day3(X0) ),
inference(component_clause,[status(thm)],[f129]) ).
fof(f132,definition,
( sQ10_spl
<=> truthday(wednesday) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f133,plain,
( ~ sQ10_spl
| truthday(wednesday) ),
inference(component_clause,[status(thm)],[f132]) ).
fof(f134,plain,
( sQ10_spl
| ~ truthday(wednesday) ),
inference(component_clause,[status(thm)],[f132]) ).
fof(f135,plain,
( ~ sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f91,f129,f132]) ).
fof(f136,definition,
( sQ11_spl
<=> truthday(friday) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f137,plain,
( ~ sQ11_spl
| truthday(friday) ),
inference(component_clause,[status(thm)],[f136]) ).
fof(f138,plain,
( sQ11_spl
| ~ truthday(friday) ),
inference(component_clause,[status(thm)],[f136]) ).
fof(f139,plain,
( ~ sQ11_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f92,f129,f136]) ).
fof(f140,definition,
! [X0] :
( sQ12_spl
<=> ( truthday(X0)
| ~ day3(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f141,plain,
! [X0] :
( ~ sQ12_spl
| truthday(X0)
| ~ day3(X0) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f143,plain,
( sQ11_spl
| sQ10_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f93,f140,f132,f136]) ).
fof(f145,plain,
( ~ sQ12_spl
| ~ sQ9_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f62,f146]) ).
fof(f146,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ9_spl
| ~ day3(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f141,f130]) ).
fof(f148,plain,
( ~ sQ4_spl
| ~ sQ8_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f60,f149]) ).
fof(f149,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ8_spl
| ~ day2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f111,f124]) ).
fof(f150,plain,
( ~ sQ3_spl
| ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f58,f151]) ).
fof(f151,plain,
! [X0] :
( ~ sQ3_spl
| ~ sQ0_spl
| ~ day1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f107,f96]) ).
fof(f152,plain,
( ~ sQ12_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f145]) ).
fof(f153,plain,
( ~ sQ4_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f148]) ).
fof(f154,plain,
( ~ sQ3_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f150]) ).
fof(f158,plain,
! [X0] :
( X0 = wednesday
| sunday != wednesday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = tuesday
| X0 = monday ),
inference(equality_factoring,[status(thm)],[f25]) ).
fof(f161,plain,
! [X0] :
( X0 = saturday
| sunday != saturday
| X0 = friday
| X0 = thursday
| X0 = wednesday
| X0 = tuesday
| X0 = monday ),
inference(equality_factoring,[status(thm)],[f25]) ).
fof(f162,definition,
! [X0] :
( sQ13_spl
<=> ( X0 = monday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = wednesday
| X0 = tuesday ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f163,plain,
! [X0] :
( ~ sQ13_spl
| X0 = monday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = wednesday
| X0 = tuesday ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f165,definition,
( sQ14_spl
<=> sunday = monday ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f166,plain,
( ~ sQ14_spl
| sunday = monday ),
inference(component_clause,[status(thm)],[f165]) ).
fof(f169,definition,
( sQ15_spl
<=> sunday = tuesday ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f170,plain,
( ~ sQ15_spl
| sunday = tuesday ),
inference(component_clause,[status(thm)],[f169]) ).
fof(f173,definition,
( sQ16_spl
<=> sunday = wednesday ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( ~ sQ16_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f158,f162,f173]) ).
fof(f177,definition,
( sQ17_spl
<=> sunday = thursday ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f178,plain,
( ~ sQ17_spl
| sunday = thursday ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f181,definition,
( sQ18_spl
<=> sunday = friday ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( ~ sQ18_spl
| sunday = friday ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f185,definition,
( sQ19_spl
<=> sunday = saturday ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f188,plain,
( ~ sQ19_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f161,f162,f185]) ).
fof(f189,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f103,f94]) ).
fof(f190,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f189]) ).
fof(f191,plain,
! [X0] :
( X0 = sK0_skl
| ~ truthday(X0) ),
inference(resolution,[status(thm)],[f56,f48]) ).
fof(f193,plain,
( ~ sQ10_spl
| wednesday = sK0_skl ),
inference(resolution,[status(thm)],[f133,f191]) ).
fof(f199,plain,
( ~ sQ10_spl
| sK0_skl != thursday ),
inference(backward_demodulation,[status(thm)],[f193,f37]) ).
fof(f202,plain,
! [X0] :
( ~ sQ13_spl
| ~ sQ10_spl
| X0 = monday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = sK0_skl
| X0 = tuesday ),
inference(backward_demodulation,[status(thm)],[f193,f163]) ).
fof(f203,plain,
( ~ sQ10_spl
| consecutive(sK0_skl) = thursday ),
inference(backward_demodulation,[status(thm)],[f193,f66]) ).
fof(f212,plain,
( ~ sQ13_spl
| ~ sQ10_spl
| sunday = monday
| sunday = friday
| sunday = thursday
| sunday = sK0_skl
| sunday = tuesday ),
inference(resolution,[status(thm)],[f202,f46]) ).
fof(f224,definition,
( sQ20_spl
<=> sK0_skl = tuesday ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f225,plain,
( ~ sQ20_spl
| sK0_skl = tuesday ),
inference(component_clause,[status(thm)],[f224]) ).
fof(f226,plain,
( sQ20_spl
| sK0_skl != tuesday ),
inference(component_clause,[status(thm)],[f224]) ).
fof(f230,definition,
( sQ22_spl
<=> sK0_skl = thursday ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( ~ sQ22_spl
| sK0_skl = thursday ),
inference(component_clause,[status(thm)],[f230]) ).
fof(f233,definition,
( sQ23_spl
<=> sK0_skl = friday ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ23_spl
| sK0_skl = friday ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f236,definition,
( sQ24_spl
<=> sK0_skl = monday ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f237,plain,
( ~ sQ24_spl
| sK0_skl = monday ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f240,definition,
( sQ25_spl
<=> friday = tuesday ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f241,plain,
( ~ sQ25_spl
| friday = tuesday ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,definition,
( sQ26_spl
<=> friday = thursday ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( ~ sQ26_spl
| friday = thursday ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f245,plain,
( sQ26_spl
| friday != thursday ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,definition,
( sQ27_spl
<=> friday = friday ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f249,definition,
( sQ28_spl
<=> friday = monday ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( ~ sQ28_spl
| friday = monday ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f253,definition,
( sQ29_spl
<=> thursday = tuesday ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f254,plain,
( ~ sQ29_spl
| thursday = tuesday ),
inference(component_clause,[status(thm)],[f253]) ).
fof(f256,definition,
( sQ30_spl
<=> thursday = thursday ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f259,definition,
( sQ31_spl
<=> thursday = monday ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( ~ sQ31_spl
| thursday = monday ),
inference(component_clause,[status(thm)],[f259]) ).
fof(f261,plain,
( sQ31_spl
| thursday != monday ),
inference(component_clause,[status(thm)],[f259]) ).
fof(f263,definition,
( sQ32_spl
<=> tuesday = tuesday ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f266,definition,
( sQ33_spl
<=> tuesday = monday ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f270,definition,
( sQ34_spl
<=> monday = monday ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f274,definition,
( sQ35_spl
<=> sunday = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f275,plain,
( ~ sQ35_spl
| sunday = sK0_skl ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f276,plain,
( sQ35_spl
| sunday != sK0_skl ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f277,plain,
( ~ sQ13_spl
| ~ sQ10_spl
| sQ14_spl
| sQ18_spl
| sQ17_spl
| sQ35_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f212,f169,f274,f177,f181,f165,f132,f162]) ).
fof(f278,definition,
! [X0] :
( sQ36_spl
<=> ( X0 = tuesday
| X0 = monday
| X0 = friday
| X0 = thursday
| X0 = sK0_skl ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f279,plain,
! [X0] :
( ~ sQ36_spl
| X0 = tuesday
| X0 = monday
| X0 = friday
| X0 = thursday
| X0 = sK0_skl ),
inference(component_clause,[status(thm)],[f278]) ).
fof(f281,definition,
( sQ37_spl
<=> saturday = tuesday ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f285,definition,
( sQ38_spl
<=> saturday = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f286,plain,
( ~ sQ38_spl
| saturday = sK0_skl ),
inference(component_clause,[status(thm)],[f285]) ).
fof(f289,definition,
( sQ39_spl
<=> saturday = thursday ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f297,definition,
( sQ41_spl
<=> saturday = monday ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f301,plain,
( ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f250,f29]) ).
fof(f302,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f301]) ).
fof(f303,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f260,f28]) ).
fof(f304,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f303]) ).
fof(f306,plain,
( sQ1_spl
| ~ sQ24_spl
| ~ truthday(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f237,f100]) ).
fof(f307,plain,
( ~ sQ24_spl
| consecutive(sunday) = sK0_skl ),
inference(backward_demodulation,[status(thm)],[f237,f63]) ).
fof(f336,plain,
( ~ sQ35_spl
| consecutive(saturday) = sK0_skl ),
inference(backward_demodulation,[status(thm)],[f275,f69]) ).
fof(f365,plain,
( ~ sQ35_spl
| consecutive(sK0_skl) = monday ),
inference(forward_demodulation,[status(thm)],[f275,f63]) ).
fof(f380,plain,
( ~ sQ23_spl
| thursday != sK0_skl ),
inference(backward_demodulation,[status(thm)],[f234,f41]) ).
fof(f384,plain,
( ~ sQ23_spl
| consecutive(sK0_skl) = saturday ),
inference(backward_demodulation,[status(thm)],[f234,f68]) ).
fof(f387,plain,
( ~ sQ22_spl
| consecutive(wednesday) = sK0_skl ),
inference(backward_demodulation,[status(thm)],[f231,f66]) ).
fof(f395,plain,
( ~ sQ20_spl
| ~ truthday(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f225,f94]) ).
fof(f399,plain,
( sQ31_spl
| ~ sQ22_spl
| sK0_skl != monday ),
inference(forward_demodulation,[status(thm)],[f231,f261]) ).
fof(f418,plain,
( sQ1_spl
| ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f306,f56]) ).
fof(f419,plain,
( sQ1_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f418]) ).
fof(f420,plain,
( ~ sQ24_spl
| monday = sK0_skl ),
inference(forward_demodulation,[status(thm)],[f63,f307]) ).
fof(f421,plain,
( ~ sQ24_spl
| sQ31_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f399]) ).
fof(f422,plain,
( ~ sQ24_spl
| sQ31_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f421]) ).
fof(f426,plain,
( ~ sQ23_spl
| ~ sQ22_spl
| sK0_skl != sK0_skl ),
inference(forward_demodulation,[status(thm)],[f231,f380]) ).
fof(f427,plain,
( ~ sQ23_spl
| ~ sQ22_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f426]) ).
fof(f428,plain,
( ~ sQ23_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f427]) ).
fof(f438,plain,
( ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f241,f34]) ).
fof(f439,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f438]) ).
fof(f440,plain,
( ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f244,f41]) ).
fof(f441,plain,
~ sQ26_spl,
inference(contradiction_clause,[status(thm)],[f440]) ).
fof(f455,plain,
( ~ sQ29_spl
| tuesday != tuesday ),
inference(forward_demodulation,[status(thm)],[f254,f33]) ).
fof(f456,plain,
( ~ sQ29_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f455]) ).
fof(f457,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f456]) ).
fof(f458,plain,
! [X0] :
( X0 = sK3_skl
| ~ day3(X0) ),
inference(resolution,[status(thm)],[f54,f62]) ).
fof(f461,plain,
( sQ26_spl
| ~ sQ36_spl
| thursday = tuesday
| thursday = monday
| thursday = thursday
| thursday = sK0_skl ),
inference(resolution,[status(thm)],[f279,f245]) ).
fof(f465,plain,
! [X0] :
( ~ sQ36_spl
| X0 = sK0_skl
| friday != sK0_skl
| X0 = tuesday
| X0 = monday
| X0 = thursday ),
inference(equality_factoring,[status(thm)],[f279]) ).
fof(f470,plain,
( sQ26_spl
| ~ sQ36_spl
| sQ29_spl
| sQ31_spl
| sQ30_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f461,f230,f256,f259,f253,f278,f243]) ).
fof(f471,definition,
! [X0] :
( sQ42_spl
<=> ( X0 = sK0_skl
| X0 = tuesday
| X0 = monday
| X0 = thursday ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f472,plain,
! [X0] :
( ~ sQ42_spl
| X0 = sK0_skl
| X0 = tuesday
| X0 = monday
| X0 = thursday ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f474,plain,
( ~ sQ36_spl
| ~ sQ23_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f465,f471,f233,f278]) ).
fof(f478,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f395,f56]) ).
fof(f479,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f478]) ).
fof(f494,plain,
day2(consecutive(sK1_skl)),
inference(resolution,[status(thm)],[f72,f58]) ).
fof(f497,definition,
( sQ43_spl
<=> day1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( ~ sQ43_spl
| day1(sK0_skl) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,definition,
( sQ44_spl
<=> day2(tuesday) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f504,definition,
( sQ45_spl
<=> day2(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f505,plain,
( ~ sQ45_spl
| day2(sK0_skl) ),
inference(component_clause,[status(thm)],[f504]) ).
fof(f507,definition,
( sQ46_spl
<=> day3(tuesday) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( ~ sQ46_spl
| day3(tuesday) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f509,plain,
( sQ46_spl
| ~ day3(tuesday) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f512,plain,
( ~ sQ45_spl
| day3(consecutive(sK0_skl)) ),
inference(resolution,[status(thm)],[f505,f76]) ).
fof(f513,plain,
( ~ sQ43_spl
| day2(consecutive(sK0_skl)) ),
inference(resolution,[status(thm)],[f498,f72]) ).
fof(f514,plain,
( ~ sQ11_spl
| friday = sK0_skl ),
inference(resolution,[status(thm)],[f137,f191]) ).
fof(f516,plain,
( ~ sQ11_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f514,f233,f136]) ).
fof(f524,plain,
( ~ sQ23_spl
| consecutive(thursday) = sK0_skl ),
inference(backward_demodulation,[status(thm)],[f234,f67]) ).
fof(f525,plain,
( ~ sQ23_spl
| consecutive(sK0_skl) = saturday ),
inference(backward_demodulation,[status(thm)],[f234,f68]) ).
fof(f527,plain,
( ~ sQ43_spl
| ~ sQ23_spl
| day2(saturday) ),
inference(backward_demodulation,[status(thm)],[f384,f513]) ).
fof(f529,plain,
( sQ11_spl
| ~ sQ23_spl
| ~ truthday(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f234,f138]) ).
fof(f530,plain,
( sQ11_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f56]) ).
fof(f531,plain,
( sQ11_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f530]) ).
fof(f534,plain,
( ~ sQ10_spl
| sK0_skl != saturday ),
inference(backward_demodulation,[status(thm)],[f193,f39]) ).
fof(f537,plain,
( ~ sQ10_spl
| consecutive(sK0_skl) = thursday ),
inference(backward_demodulation,[status(thm)],[f193,f66]) ).
fof(f538,plain,
( ~ sQ10_spl
| consecutive(tuesday) = sK0_skl ),
inference(backward_demodulation,[status(thm)],[f193,f65]) ).
fof(f539,plain,
( ~ sQ10_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f199,f230,f132]) ).
fof(f545,plain,
( ~ sQ45_spl
| ~ sQ10_spl
| day3(thursday) ),
inference(forward_demodulation,[status(thm)],[f203,f512]) ).
fof(f555,plain,
( ~ sQ23_spl
| monday != sK0_skl ),
inference(backward_demodulation,[status(thm)],[f560,f29]) ).
fof(f557,plain,
( ~ sQ23_spl
| sK0_skl != saturday ),
inference(backward_demodulation,[status(thm)],[f560,f44]) ).
fof(f560,plain,
( ~ sQ23_spl
| friday = sK0_skl ),
inference(forward_demodulation,[status(thm)],[f67,f524]) ).
fof(f567,plain,
! [X0] :
( X0 = sK1_skl
| ~ day1(X0) ),
inference(resolution,[status(thm)],[f50,f58]) ).
fof(f568,plain,
( ~ sQ5_spl
| ~ sQ8_spl
| truthday(thursday) ),
inference(resolution,[status(thm)],[f124,f114]) ).
fof(f570,plain,
( ~ sQ8_spl
| truthday(sK2_skl) ),
inference(resolution,[status(thm)],[f124,f60]) ).
fof(f571,plain,
( ~ day2(sunday)
| day1(saturday) ),
inference(paramodulation,[status(thm)],[f69,f73]) ).
fof(f572,plain,
( ~ day3(sunday)
| day2(saturday) ),
inference(paramodulation,[status(thm)],[f69,f77]) ).
fof(f573,definition,
( sQ47_spl
<=> day1(saturday) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f574,plain,
( ~ sQ47_spl
| day1(saturday) ),
inference(component_clause,[status(thm)],[f573]) ).
fof(f575,plain,
( sQ47_spl
| ~ day1(saturday) ),
inference(component_clause,[status(thm)],[f573]) ).
fof(f576,plain,
( ~ sQ7_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f571,f573,f119]) ).
fof(f577,definition,
( sQ48_spl
<=> day3(sunday) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f579,plain,
( sQ48_spl
| ~ day3(sunday) ),
inference(component_clause,[status(thm)],[f577]) ).
fof(f580,plain,
( ~ sQ48_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f572,f116,f577]) ).
fof(f584,definition,
( sQ49_spl
<=> day3(saturday) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f586,plain,
( sQ49_spl
| ~ day3(saturday) ),
inference(component_clause,[status(thm)],[f584]) ).
fof(f595,plain,
( ~ sQ43_spl
| ~ sQ23_spl
| day3(consecutive(saturday)) ),
inference(resolution,[status(thm)],[f527,f76]) ).
fof(f596,plain,
( ~ sQ43_spl
| ~ sQ23_spl
| day3(sunday) ),
inference(forward_demodulation,[status(thm)],[f69,f595]) ).
fof(f597,plain,
( ~ sQ43_spl
| ~ sQ23_spl
| sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f596,f579]) ).
fof(f598,plain,
( ~ sQ43_spl
| ~ sQ23_spl
| sQ48_spl ),
inference(contradiction_clause,[status(thm)],[f597]) ).
fof(f602,plain,
( ~ sQ10_spl
| monday != sK0_skl ),
inference(backward_demodulation,[status(thm)],[f606,f27]) ).
fof(f604,plain,
( ~ sQ10_spl
| sK0_skl != sunday ),
inference(backward_demodulation,[status(thm)],[f606,f40]) ).
fof(f606,plain,
( ~ sQ10_spl
| wednesday = sK0_skl ),
inference(forward_demodulation,[status(thm)],[f65,f538]) ).
fof(f634,definition,
! [X0] :
( sQ51_spl
<=> ( X0 = monday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = sK0_skl
| X0 = tuesday ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f635,plain,
! [X0] :
( ~ sQ51_spl
| X0 = monday
| X0 = saturday
| X0 = friday
| X0 = thursday
| X0 = sK0_skl
| X0 = tuesday ),
inference(component_clause,[status(thm)],[f634]) ).
fof(f644,plain,
( ~ day2(tuesday)
| day1(monday) ),
inference(paramodulation,[status(thm)],[f64,f73]) ).
fof(f646,definition,
( sQ52_spl
<=> day1(monday) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( ~ sQ52_spl
| day1(monday) ),
inference(component_clause,[status(thm)],[f646]) ).
fof(f649,plain,
( ~ sQ44_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f644,f646,f500]) ).
fof(f650,definition,
( sQ53_spl
<=> day2(monday) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f651,plain,
( ~ sQ53_spl
| day2(monday) ),
inference(component_clause,[status(thm)],[f650]) ).
fof(f655,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f182,f45]) ).
fof(f656,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f655]) ).
fof(f657,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f178,f43]) ).
fof(f658,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f657]) ).
fof(f659,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f166,f31]) ).
fof(f660,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f659]) ).
fof(f676,plain,
( ~ sQ1_spl
| monday = sK0_skl ),
inference(resolution,[status(thm)],[f99,f191]) ).
fof(f678,plain,
( ~ sQ1_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f676,f555]) ).
fof(f679,plain,
( ~ sQ1_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f678]) ).
fof(f695,definition,
( sQ54_spl
<=> day3(thursday) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f697,plain,
( sQ54_spl
| ~ day3(thursday) ),
inference(component_clause,[status(thm)],[f695]) ).
fof(f699,plain,
( ~ sQ43_spl
| ~ sQ10_spl
| day2(thursday) ),
inference(forward_demodulation,[status(thm)],[f537,f513]) ).
fof(f701,plain,
( ~ sQ45_spl
| ~ sQ10_spl
| day3(thursday) ),
inference(forward_demodulation,[status(thm)],[f537,f512]) ).
fof(f702,plain,
( ~ sQ45_spl
| ~ sQ10_spl
| sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f701,f697]) ).
fof(f703,plain,
( ~ sQ45_spl
| ~ sQ10_spl
| sQ54_spl ),
inference(contradiction_clause,[status(thm)],[f702]) ).
fof(f704,plain,
( ~ sQ8_spl
| sK2_skl = sK0_skl ),
inference(resolution,[status(thm)],[f570,f191]) ).
fof(f707,plain,
( ~ sQ8_spl
| day2(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f704,f60]) ).
fof(f713,plain,
( ~ sQ47_spl
| day2(consecutive(saturday)) ),
inference(resolution,[status(thm)],[f574,f72]) ).
fof(f714,plain,
( ~ sQ47_spl
| day2(sunday) ),
inference(forward_demodulation,[status(thm)],[f69,f713]) ).
fof(f715,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| truthday(saturday) ),
inference(resolution,[status(thm)],[f117,f124]) ).
fof(f721,plain,
( ~ sQ53_spl
| day3(consecutive(monday)) ),
inference(resolution,[status(thm)],[f651,f76]) ).
fof(f723,plain,
( ~ sQ53_spl
| day3(tuesday) ),
inference(forward_demodulation,[status(thm)],[f64,f721]) ).
fof(f724,plain,
( ~ sQ53_spl
| sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f723,f509]) ).
fof(f725,plain,
( ~ sQ53_spl
| sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f726,plain,
( ~ sQ1_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f676,f602]) ).
fof(f727,plain,
( ~ sQ1_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f726]) ).
fof(f734,plain,
( ~ day3(monday)
| day2(sunday) ),
inference(paramodulation,[status(thm)],[f63,f77]) ).
fof(f735,definition,
( sQ55_spl
<=> day1(sunday) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f736,plain,
( ~ sQ55_spl
| day1(sunday) ),
inference(component_clause,[status(thm)],[f735]) ).
fof(f739,definition,
( sQ56_spl
<=> day3(monday) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f741,plain,
( sQ56_spl
| ~ day3(monday) ),
inference(component_clause,[status(thm)],[f739]) ).
fof(f742,plain,
( ~ sQ56_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f734,f119,f739]) ).
fof(f751,plain,
( ~ sQ8_spl
| ~ sQ43_spl
| ~ sQ10_spl
| truthday(thursday) ),
inference(resolution,[status(thm)],[f699,f124]) ).
fof(f755,plain,
( ~ sQ9_spl
| ~ sQ45_spl
| ~ sQ10_spl
| ~ truthday(thursday) ),
inference(resolution,[status(thm)],[f545,f130]) ).
fof(f757,plain,
( ~ sQ9_spl
| ~ sQ45_spl
| ~ sQ10_spl
| ~ sQ8_spl
| ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f755,f751]) ).
fof(f758,plain,
( ~ sQ9_spl
| ~ sQ45_spl
| ~ sQ10_spl
| ~ sQ8_spl
| ~ sQ43_spl ),
inference(contradiction_clause,[status(thm)],[f757]) ).
fof(f759,plain,
( sQ5_spl
| ~ sQ43_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f115,f699]) ).
fof(f760,plain,
( sQ5_spl
| ~ sQ43_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f759]) ).
fof(f766,plain,
( ~ sQ8_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f707,f504,f123]) ).
fof(f770,plain,
( sQ7_spl
| ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f121,f714]) ).
fof(f771,plain,
( sQ7_spl
| ~ sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f770]) ).
fof(f780,plain,
( ~ sQ47_spl
| day3(consecutive(sunday)) ),
inference(resolution,[status(thm)],[f714,f76]) ).
fof(f781,plain,
( ~ sQ47_spl
| day3(monday) ),
inference(forward_demodulation,[status(thm)],[f63,f780]) ).
fof(f782,plain,
( ~ sQ47_spl
| sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f781,f741]) ).
fof(f783,plain,
( ~ sQ47_spl
| sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f782]) ).
fof(f784,plain,
( ~ day2(friday)
| day1(thursday) ),
inference(paramodulation,[status(thm)],[f67,f73]) ).
fof(f785,plain,
( ~ day3(friday)
| day2(thursday) ),
inference(paramodulation,[status(thm)],[f67,f77]) ).
fof(f786,definition,
( sQ57_spl
<=> day1(thursday) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( ~ sQ57_spl
| day1(thursday) ),
inference(component_clause,[status(thm)],[f786]) ).
fof(f789,definition,
( sQ58_spl
<=> day2(friday) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f792,plain,
( ~ sQ58_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f784,f786,f789]) ).
fof(f793,definition,
( sQ59_spl
<=> day3(friday) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f796,plain,
( ~ sQ59_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f785,f113,f793]) ).
fof(f797,plain,
( ~ day2(saturday)
| day1(friday) ),
inference(paramodulation,[status(thm)],[f68,f73]) ).
fof(f798,plain,
( ~ day3(saturday)
| day2(friday) ),
inference(paramodulation,[status(thm)],[f68,f77]) ).
fof(f799,definition,
( sQ60_spl
<=> day1(friday) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( ~ sQ60_spl
| day1(friday) ),
inference(component_clause,[status(thm)],[f799]) ).
fof(f802,plain,
( ~ sQ6_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f797,f799,f116]) ).
fof(f803,plain,
( ~ sQ49_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f798,f789,f584]) ).
fof(f817,plain,
( ~ sQ3_spl
| truthday(sK1_skl) ),
inference(resolution,[status(thm)],[f107,f58]) ).
fof(f822,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| saturday = sK0_skl ),
inference(resolution,[status(thm)],[f715,f191]) ).
fof(f824,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f822,f534]) ).
fof(f825,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f824]) ).
fof(f828,plain,
( ~ sQ57_spl
| day2(consecutive(thursday)) ),
inference(resolution,[status(thm)],[f787,f72]) ).
fof(f831,plain,
( ~ sQ57_spl
| day2(friday) ),
inference(forward_demodulation,[status(thm)],[f67,f828]) ).
fof(f832,plain,
( ~ sQ3_spl
| ~ sQ60_spl
| truthday(friday) ),
inference(resolution,[status(thm)],[f800,f107]) ).
fof(f834,plain,
( ~ sQ60_spl
| day2(consecutive(friday)) ),
inference(resolution,[status(thm)],[f800,f72]) ).
fof(f835,plain,
( ~ sQ3_spl
| ~ sQ60_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f832,f136,f799,f106]) ).
fof(f836,plain,
( ~ sQ60_spl
| day2(saturday) ),
inference(forward_demodulation,[status(thm)],[f68,f834]) ).
fof(f837,plain,
( ~ sQ60_spl
| sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f836,f118]) ).
fof(f838,plain,
( ~ sQ60_spl
| sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f837]) ).
fof(f841,plain,
( ~ sQ55_spl
| day2(consecutive(sunday)) ),
inference(resolution,[status(thm)],[f736,f72]) ).
fof(f842,plain,
( ~ sQ55_spl
| day2(monday) ),
inference(forward_demodulation,[status(thm)],[f63,f841]) ).
fof(f846,plain,
( sQ26_spl
| ~ sQ42_spl
| friday = sK0_skl
| friday = tuesday
| friday = monday ),
inference(resolution,[status(thm)],[f472,f245]) ).
fof(f847,plain,
( ~ sQ42_spl
| monday = sK0_skl
| monday = tuesday
| monday = monday ),
inference(resolution,[status(thm)],[f472,f28]) ).
fof(f848,plain,
( ~ sQ42_spl
| tuesday = sK0_skl
| tuesday = tuesday
| tuesday = monday ),
inference(resolution,[status(thm)],[f472,f33]) ).
fof(f863,plain,
( sQ26_spl
| ~ sQ42_spl
| sQ23_spl
| sQ25_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f846,f249,f240,f233,f471,f243]) ).
fof(f864,plain,
( ~ sQ42_spl
| sQ24_spl
| sQ33_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f847,f270,f266,f236,f471]) ).
fof(f865,plain,
( ~ sQ42_spl
| sQ20_spl
| sQ32_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f848,f266,f263,f224,f471]) ).
fof(f869,definition,
! [X0] :
( sQ61_spl
<=> ( X0 = monday
| X0 = sK0_skl
| X0 = tuesday ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f870,plain,
! [X0] :
( ~ sQ61_spl
| X0 = monday
| X0 = sK0_skl
| X0 = tuesday ),
inference(component_clause,[status(thm)],[f869]) ).
fof(f877,plain,
( ~ sQ61_spl
| friday = monday
| friday = sK0_skl ),
inference(resolution,[status(thm)],[f870,f34]) ).
fof(f878,plain,
( ~ sQ61_spl
| thursday = monday
| thursday = sK0_skl ),
inference(resolution,[status(thm)],[f870,f33]) ).
fof(f887,plain,
! [X0] :
( ~ sQ61_spl
| X0 = monday
| tuesday != monday
| X0 = sK0_skl ),
inference(equality_factoring,[status(thm)],[f870]) ).
fof(f890,plain,
( ~ sQ61_spl
| sQ28_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f877,f233,f249,f869]) ).
fof(f891,plain,
( ~ sQ61_spl
| sQ31_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f878,f230,f259,f869]) ).
fof(f894,definition,
! [X0] :
( sQ62_spl
<=> ( X0 = sK0_skl
| X0 = monday ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f895,plain,
! [X0] :
( ~ sQ62_spl
| X0 = sK0_skl
| X0 = monday ),
inference(component_clause,[status(thm)],[f894]) ).
fof(f898,plain,
( ~ sQ61_spl
| ~ sQ33_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f887,f894,f266,f869]) ).
fof(f901,plain,
( ~ sQ62_spl
| tuesday = sK0_skl ),
inference(resolution,[status(thm)],[f895,f26]) ).
fof(f912,plain,
( ~ sQ62_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f901,f224,f894]) ).
fof(f918,plain,
( ~ sQ51_spl
| thursday = monday
| thursday = friday
| thursday = thursday
| thursday = sK0_skl
| thursday = tuesday ),
inference(resolution,[status(thm)],[f635,f42]) ).
fof(f919,plain,
( ~ sQ51_spl
| tuesday = monday
| tuesday = friday
| tuesday = thursday
| tuesday = sK0_skl
| tuesday = tuesday ),
inference(resolution,[status(thm)],[f635,f35]) ).
fof(f934,plain,
! [X0] :
( ~ sQ51_spl
| X0 = monday
| saturday != monday
| X0 = friday
| X0 = thursday
| X0 = sK0_skl
| X0 = tuesday ),
inference(equality_factoring,[status(thm)],[f635]) ).
fof(f937,plain,
( ~ sQ51_spl
| sQ31_spl
| sQ26_spl
| sQ30_spl
| sQ22_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f918,f253,f230,f256,f243,f259,f634]) ).
fof(f938,plain,
( ~ sQ51_spl
| sQ33_spl
| sQ25_spl
| sQ29_spl
| sQ20_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f919,f263,f224,f253,f240,f266,f634]) ).
fof(f945,plain,
( ~ sQ51_spl
| ~ sQ41_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f934,f278,f297,f634]) ).
fof(f980,plain,
( ~ sQ35_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f275,f604]) ).
fof(f981,plain,
( ~ sQ35_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f980]) ).
fof(f1016,plain,
( ~ sQ3_spl
| sK1_skl = sK0_skl ),
inference(resolution,[status(thm)],[f817,f191]) ).
fof(f1019,plain,
( ~ sQ3_spl
| day1(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1016,f58]) ).
fof(f1021,plain,
( ~ sQ3_spl
| day2(consecutive(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f1016,f494]) ).
fof(f1023,plain,
( ~ sQ3_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1019,f497,f106]) ).
fof(f1025,plain,
( ~ sQ3_spl
| ~ sQ10_spl
| day2(thursday) ),
inference(forward_demodulation,[status(thm)],[f537,f1021]) ).
fof(f1026,plain,
( ~ sQ3_spl
| ~ sQ10_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1025,f115]) ).
fof(f1027,plain,
( ~ sQ3_spl
| ~ sQ10_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1026]) ).
fof(f1033,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f170,f36]) ).
fof(f1034,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1033]) ).
fof(f1045,plain,
( sQ48_spl
| ~ sQ35_spl
| ~ day3(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1046,f579]) ).
fof(f1046,plain,
( ~ sQ35_spl
| sunday = sK0_skl ),
inference(forward_demodulation,[status(thm)],[f69,f336]) ).
fof(f1051,plain,
( ~ day2(wednesday)
| day1(tuesday) ),
inference(paramodulation,[status(thm)],[f65,f73]) ).
fof(f1052,plain,
( ~ day3(wednesday)
| day2(tuesday) ),
inference(paramodulation,[status(thm)],[f65,f77]) ).
fof(f1053,definition,
( sQ63_spl
<=> day1(tuesday) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( ~ sQ63_spl
| day1(tuesday) ),
inference(component_clause,[status(thm)],[f1053]) ).
fof(f1056,definition,
( sQ64_spl
<=> day2(wednesday) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1059,plain,
( ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1051,f1053,f1056]) ).
fof(f1060,definition,
( sQ65_spl
<=> day3(wednesday) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
( sQ65_spl
| ~ day3(wednesday) ),
inference(component_clause,[status(thm)],[f1060]) ).
fof(f1063,plain,
( ~ sQ65_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1052,f500,f1060]) ).
fof(f1065,plain,
( ~ day3(thursday)
| day2(wednesday) ),
inference(paramodulation,[status(thm)],[f66,f77]) ).
fof(f1070,plain,
( ~ sQ54_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1065,f1056,f695]) ).
fof(f1074,plain,
! [X0] :
( ~ sQ43_spl
| X0 = sK0_skl
| ~ day1(X0) ),
inference(resolution,[status(thm)],[f498,f50]) ).
fof(f1080,plain,
! [X0] :
( ~ sQ3_spl
| X0 = consecutive(sK0_skl)
| ~ day2(X0) ),
inference(resolution,[status(thm)],[f1021,f52]) ).
fof(f1081,plain,
( ~ sQ3_spl
| day3(consecutive(consecutive(sK0_skl))) ),
inference(resolution,[status(thm)],[f1021,f76]) ).
fof(f1087,plain,
( ~ sQ5_spl
| ~ sQ8_spl
| thursday = sK0_skl ),
inference(resolution,[status(thm)],[f568,f191]) ).
fof(f1089,plain,
( ~ sQ5_spl
| ~ sQ8_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f1087,f230,f123,f113]) ).
fof(f1100,plain,
( ~ sQ1_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f676,f236,f98]) ).
fof(f1129,plain,
( ~ sQ24_spl
| consecutive(sunday) = sK0_skl ),
inference(forward_demodulation,[status(thm)],[f237,f63]) ).
fof(f1133,plain,
( ~ sQ12_spl
| truthday(sK3_skl) ),
inference(resolution,[status(thm)],[f141,f62]) ).
fof(f1145,plain,
( ~ sQ24_spl
| ~ day2(sK0_skl)
| day1(sunday) ),
inference(paramodulation,[status(thm)],[f1129,f73]) ).
fof(f1146,plain,
( ~ sQ24_spl
| ~ day3(sK0_skl)
| day2(sunday) ),
inference(paramodulation,[status(thm)],[f1129,f77]) ).
fof(f1147,plain,
( ~ sQ24_spl
| ~ sQ45_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1145,f735,f504,f236]) ).
fof(f1148,definition,
( sQ67_spl
<=> day3(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( sQ67_spl
| ~ day3(sK0_skl) ),
inference(component_clause,[status(thm)],[f1148]) ).
fof(f1151,plain,
( ~ sQ24_spl
| ~ sQ67_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1146,f119,f1148,f236]) ).
fof(f1154,plain,
! [X0] :
( ~ sQ3_spl
| X0 = sK0_skl
| ~ day1(X0) ),
inference(backward_demodulation,[status(thm)],[f1016,f567]) ).
fof(f1156,plain,
( ~ sQ57_spl
| day3(consecutive(friday)) ),
inference(resolution,[status(thm)],[f831,f76]) ).
fof(f1157,plain,
( ~ sQ57_spl
| day3(saturday) ),
inference(forward_demodulation,[status(thm)],[f68,f1156]) ).
fof(f1175,plain,
( ~ sQ63_spl
| ~ sQ43_spl
| tuesday = sK0_skl ),
inference(resolution,[status(thm)],[f1074,f1054]) ).
fof(f1177,plain,
( ~ sQ63_spl
| ~ sQ43_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1175,f224,f497,f1053]) ).
fof(f1180,plain,
! [X0] :
( ~ sQ3_spl
| X0 = consecutive(consecutive(sK0_skl))
| ~ day3(X0) ),
inference(resolution,[status(thm)],[f1081,f54]) ).
fof(f1182,plain,
( ~ sQ3_spl
| sK2_skl = consecutive(sK0_skl) ),
inference(resolution,[status(thm)],[f1080,f60]) ).
fof(f1186,plain,
! [X0] :
( ~ sQ3_spl
| X0 = consecutive(sK2_skl)
| ~ day3(X0) ),
inference(backward_demodulation,[status(thm)],[f1182,f1180]) ).
fof(f1203,plain,
( ~ sQ3_spl
| sK3_skl = consecutive(sK2_skl) ),
inference(resolution,[status(thm)],[f1186,f62]) ).
fof(f1216,definition,
( sQ72_spl
<=> day3(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1218,plain,
( sQ72_spl
| ~ day3(sK3_skl) ),
inference(component_clause,[status(thm)],[f1216]) ).
fof(f1256,plain,
( ~ sQ55_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f842,f650,f735]) ).
fof(f1270,plain,
( ~ sQ12_spl
| sK3_skl = sK0_skl ),
inference(resolution,[status(thm)],[f1133,f191]) ).
fof(f1273,plain,
( ~ sQ12_spl
| day3(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1270,f62]) ).
fof(f1275,plain,
! [X0] :
( ~ sQ12_spl
| X0 = sK0_skl
| ~ day3(X0) ),
inference(backward_demodulation,[status(thm)],[f1270,f458]) ).
fof(f1277,plain,
( ~ sQ12_spl
| sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1273,f1150]) ).
fof(f1278,plain,
( ~ sQ12_spl
| sQ67_spl ),
inference(contradiction_clause,[status(thm)],[f1277]) ).
fof(f1284,plain,
( ~ sQ3_spl
| ~ sQ12_spl
| sK0_skl = consecutive(sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f1270,f1203]) ).
fof(f1299,plain,
( ~ sQ57_spl
| ~ sQ12_spl
| saturday = sK0_skl ),
inference(resolution,[status(thm)],[f1275,f1157]) ).
fof(f1302,plain,
( ~ sQ57_spl
| ~ sQ12_spl
| consecutive(sK0_skl) = sunday ),
inference(backward_demodulation,[status(thm)],[f1299,f69]) ).
fof(f1304,plain,
( sQ47_spl
| ~ sQ57_spl
| ~ sQ12_spl
| ~ day1(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1299,f575]) ).
fof(f1320,plain,
( sQ7_spl
| ~ sQ57_spl
| ~ sQ12_spl
| ~ sQ3_spl
| ~ day2(sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f1324,f121]) ).
fof(f1324,plain,
( ~ sQ57_spl
| ~ sQ12_spl
| ~ sQ3_spl
| sK2_skl = sunday ),
inference(forward_demodulation,[status(thm)],[f1182,f1302]) ).
fof(f1326,plain,
( sQ47_spl
| ~ sQ57_spl
| ~ sQ12_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1304,f497,f140,f786,f573]) ).
fof(f1328,plain,
( sQ7_spl
| ~ sQ57_spl
| ~ sQ12_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1320,f60]) ).
fof(f1329,plain,
( sQ7_spl
| ~ sQ57_spl
| ~ sQ12_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f1328]) ).
fof(f1343,plain,
( ~ sQ3_spl
| ~ sQ52_spl
| monday = sK0_skl ),
inference(resolution,[status(thm)],[f647,f1154]) ).
fof(f1347,plain,
( ~ sQ3_spl
| ~ sQ52_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1343,f236,f646,f106]) ).
fof(f1363,plain,
( ~ sQ13_spl
| thursday = monday
| thursday = friday
| thursday = thursday
| thursday = wednesday
| thursday = tuesday ),
inference(resolution,[status(thm)],[f163,f42]) ).
fof(f1364,plain,
( ~ sQ13_spl
| monday = monday
| monday = friday
| monday = thursday
| monday = wednesday
| monday = tuesday ),
inference(resolution,[status(thm)],[f163,f30]) ).
fof(f1365,plain,
( ~ sQ13_spl
| wednesday = monday
| wednesday = friday
| wednesday = thursday
| wednesday = wednesday
| wednesday = tuesday ),
inference(resolution,[status(thm)],[f163,f39]) ).
fof(f1366,plain,
( ~ sQ13_spl
| friday = monday
| friday = friday
| friday = thursday
| friday = wednesday
| friday = tuesday ),
inference(resolution,[status(thm)],[f163,f44]) ).
fof(f1367,plain,
( ~ sQ13_spl
| tuesday = monday
| tuesday = friday
| tuesday = thursday
| tuesday = wednesday
| tuesday = tuesday ),
inference(resolution,[status(thm)],[f163,f35]) ).
fof(f1368,plain,
( ~ sQ13_spl
| sunday = monday
| sunday = friday
| sunday = thursday
| sunday = wednesday
| sunday = tuesday ),
inference(resolution,[status(thm)],[f163,f46]) ).
fof(f1384,definition,
( sQ73_spl
<=> thursday = wednesday ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1385,plain,
( ~ sQ73_spl
| thursday = wednesday ),
inference(component_clause,[status(thm)],[f1384]) ).
fof(f1387,plain,
( ~ sQ13_spl
| sQ31_spl
| sQ26_spl
| sQ30_spl
| sQ73_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f1363,f253,f1384,f256,f243,f259,f162]) ).
fof(f1388,definition,
( sQ74_spl
<=> monday = wednesday ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1389,plain,
( ~ sQ74_spl
| monday = wednesday ),
inference(component_clause,[status(thm)],[f1388]) ).
fof(f1391,plain,
( ~ sQ13_spl
| sQ34_spl
| sQ28_spl
| sQ31_spl
| sQ74_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1364,f266,f1388,f259,f249,f270,f162]) ).
fof(f1392,definition,
( sQ75_spl
<=> wednesday = tuesday ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
( ~ sQ75_spl
| wednesday = tuesday ),
inference(component_clause,[status(thm)],[f1392]) ).
fof(f1395,definition,
( sQ76_spl
<=> wednesday = wednesday ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1398,definition,
( sQ77_spl
<=> wednesday = friday ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1399,plain,
( ~ sQ77_spl
| wednesday = friday ),
inference(component_clause,[status(thm)],[f1398]) ).
fof(f1401,plain,
( ~ sQ13_spl
| sQ74_spl
| sQ77_spl
| sQ73_spl
| sQ76_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1365,f1392,f1395,f1384,f1398,f1388,f162]) ).
fof(f1402,plain,
( ~ sQ13_spl
| sQ28_spl
| sQ27_spl
| sQ26_spl
| sQ77_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f1366,f240,f1398,f243,f246,f249,f162]) ).
fof(f1403,plain,
( ~ sQ13_spl
| sQ33_spl
| sQ25_spl
| sQ29_spl
| sQ75_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f1367,f263,f1392,f253,f240,f266,f162]) ).
fof(f1404,plain,
( ~ sQ13_spl
| sQ14_spl
| sQ18_spl
| sQ17_spl
| sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f1368,f169,f173,f177,f181,f165,f162]) ).
fof(f1419,plain,
( sQ54_spl
| ~ sQ22_spl
| ~ day3(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1428,f697]) ).
fof(f1428,plain,
( ~ sQ22_spl
| thursday = sK0_skl ),
inference(forward_demodulation,[status(thm)],[f66,f387]) ).
fof(f1430,plain,
( ~ sQ3_spl
| ~ sQ8_spl
| sK0_skl = consecutive(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f704,f1182]) ).
fof(f1456,plain,
( sQ54_spl
| ~ sQ22_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1419,f1148,f230,f695]) ).
fof(f1481,plain,
( thursday = saturday
| thursday = friday
| thursday = thursday
| thursday = wednesday
| thursday = tuesday
| thursday = monday ),
inference(resolution,[status(thm)],[f25,f43]) ).
fof(f1483,plain,
( monday = saturday
| monday = friday
| monday = thursday
| monday = wednesday
| monday = tuesday
| monday = monday ),
inference(resolution,[status(thm)],[f25,f31]) ).
fof(f1486,plain,
( tuesday = saturday
| tuesday = friday
| tuesday = thursday
| tuesday = wednesday
| tuesday = tuesday
| tuesday = monday ),
inference(resolution,[status(thm)],[f25,f36]) ).
fof(f1487,plain,
( sQ35_spl
| sK0_skl = saturday
| sK0_skl = friday
| sK0_skl = thursday
| sK0_skl = wednesday
| sK0_skl = tuesday
| sK0_skl = monday ),
inference(resolution,[status(thm)],[f25,f276]) ).
fof(f1506,plain,
( sQ39_spl
| sQ26_spl
| sQ30_spl
| sQ73_spl
| sQ29_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1481,f259,f253,f1384,f256,f243,f289]) ).
fof(f1508,plain,
( sQ41_spl
| sQ28_spl
| sQ31_spl
| sQ74_spl
| sQ33_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f1483,f270,f266,f1388,f259,f249,f297]) ).
fof(f1511,plain,
( sQ37_spl
| sQ25_spl
| sQ29_spl
| sQ75_spl
| sQ32_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1486,f266,f263,f1392,f253,f240,f281]) ).
fof(f1512,definition,
( sQ80_spl
<=> sK0_skl = wednesday ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1513,plain,
( ~ sQ80_spl
| sK0_skl = wednesday ),
inference(component_clause,[status(thm)],[f1512]) ).
fof(f1515,plain,
( sQ35_spl
| sQ38_spl
| sQ23_spl
| sQ22_spl
| sQ80_spl
| sQ20_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1487,f236,f224,f1512,f230,f233,f285,f274]) ).
fof(f1524,plain,
( ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1393,f32]) ).
fof(f1525,plain,
~ sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1524]) ).
fof(f1526,plain,
( ~ sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1399,f38]) ).
fof(f1527,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f1526]) ).
fof(f1528,plain,
( ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1385,f37]) ).
fof(f1529,plain,
~ sQ73_spl,
inference(contradiction_clause,[status(thm)],[f1528]) ).
fof(f1530,plain,
( ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1389,f27]) ).
fof(f1531,plain,
~ sQ74_spl,
inference(contradiction_clause,[status(thm)],[f1530]) ).
fof(f1539,plain,
( ~ sQ38_spl
| consecutive(sK0_skl) = sunday ),
inference(backward_demodulation,[status(thm)],[f286,f69]) ).
fof(f1540,plain,
( sQ49_spl
| ~ sQ38_spl
| ~ day3(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f286,f586]) ).
fof(f1545,plain,
( sQ7_spl
| ~ sQ38_spl
| ~ sQ3_spl
| ~ day2(sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f1555,f121]) ).
fof(f1554,plain,
( sQ35_spl
| ~ sQ38_spl
| ~ sQ3_spl
| sK2_skl != sK0_skl ),
inference(backward_demodulation,[status(thm)],[f1555,f276]) ).
fof(f1555,plain,
( ~ sQ38_spl
| ~ sQ3_spl
| sK2_skl = sunday ),
inference(forward_demodulation,[status(thm)],[f1182,f1539]) ).
fof(f1556,plain,
( sQ49_spl
| ~ sQ38_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1540,f1148,f285,f584]) ).
fof(f1559,plain,
( sQ7_spl
| ~ sQ38_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1545,f60]) ).
fof(f1560,plain,
( sQ7_spl
| ~ sQ38_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f1559]) ).
fof(f1563,plain,
( sQ65_spl
| ~ sQ80_spl
| ~ day3(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1513,f1062]) ).
fof(f1566,plain,
( sQ10_spl
| ~ sQ80_spl
| ~ truthday(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1513,f134]) ).
fof(f1586,plain,
( sQ65_spl
| ~ sQ80_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1563,f1148,f1512,f1060]) ).
fof(f1587,plain,
( sQ10_spl
| ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1566,f56]) ).
fof(f1588,plain,
( sQ10_spl
| ~ sQ80_spl ),
inference(contradiction_clause,[status(thm)],[f1587]) ).
fof(f1589,plain,
( sQ72_spl
| ~ sQ12_spl
| ~ day3(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f1270,f1218]) ).
fof(f1590,plain,
( sQ72_spl
| ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1589,f1273]) ).
fof(f1591,plain,
( sQ72_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f1590]) ).
fof(f1600,plain,
( sQ48_spl
| ~ sQ35_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f1045,f1148,f274,f577]) ).
fof(f1603,plain,
( ~ sQ35_spl
| ~ sQ3_spl
| consecutive(sK2_skl) = tuesday ),
inference(backward_demodulation,[status(thm)],[f1611,f64]) ).
fof(f1611,plain,
( ~ sQ35_spl
| ~ sQ3_spl
| sK2_skl = monday ),
inference(forward_demodulation,[status(thm)],[f1182,f365]) ).
fof(f1627,plain,
( ~ sQ35_spl
| ~ sQ3_spl
| ~ sQ12_spl
| sK0_skl = tuesday ),
inference(forward_demodulation,[status(thm)],[f1284,f1603]) ).
fof(f1628,plain,
( ~ sQ35_spl
| ~ sQ3_spl
| ~ sQ12_spl
| sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1627,f226]) ).
fof(f1629,plain,
( ~ sQ35_spl
| ~ sQ3_spl
| ~ sQ12_spl
| sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f1628]) ).
fof(f1632,plain,
( ~ sQ3_spl
| ~ sQ8_spl
| sK0_skl = consecutive(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1635,f1182]) ).
fof(f1635,plain,
( ~ sQ3_spl
| ~ sQ8_spl
| sK0_skl = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f1182,f1430]) ).
fof(f1637,plain,
( sQ35_spl
| ~ sQ38_spl
| ~ sQ3_spl
| ~ sQ8_spl
| sK0_skl != sK0_skl ),
inference(forward_demodulation,[status(thm)],[f1635,f1554]) ).
fof(f1638,plain,
( sQ35_spl
| ~ sQ38_spl
| ~ sQ3_spl
| ~ sQ8_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1637]) ).
fof(f1639,plain,
( sQ35_spl
| ~ sQ38_spl
| ~ sQ3_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f1638]) ).
fof(f1669,plain,
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ8_spl
| sK0_skl = saturday ),
inference(forward_demodulation,[status(thm)],[f1632,f525]) ).
fof(f1670,plain,
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1669,f557]) ).
fof(f1671,plain,
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f1670]) ).
fof(f1673,plain,
( ~ sQ8_spl
| ~ sQ6_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f822,f285,f116,f123]) ).
fof(f1748,plain,
( ~ sQ46_spl
| ~ sQ12_spl
| tuesday = sK0_skl ),
inference(resolution,[status(thm)],[f1275,f508]) ).
fof(f1750,plain,
( ~ sQ46_spl
| ~ sQ12_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1748,f224,f140,f507]) ).
fof(f1751,plain,
$false,
inference(sat_refutation,[status(thm)],[f101,f109,f122,f126,f127,f128,f135,f139,f143,f152,f153,f154,f176,f188,f190,f277,f302,f304,f419,f422,f428,f439,f441,f457,f470,f474,f479,f516,f531,f539,f576,f580,f598,f649,f656,f658,f660,f679,f703,f725,f727,f742,f758,f760,f766,f771,f783,f792,f796,f802,f803,f825,f835,f838,f863,f864,f865,f890,f891,f898,f912,f937,f938,f945,f981,f1023,f1027,f1034,f1059,f1063,f1070,f1089,f1100,f1147,f1151,f1177,f1256,f1278,f1326,f1329,f1347,f1387,f1391,f1401,f1402,f1403,f1404,f1456,f1506,f1508,f1511,f1515,f1525,f1527,f1529,f1531,f1556,f1560,f1586,f1588,f1591,f1600,f1629,f1639,f1671,f1673,f1750]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 03:50:11 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.14/0.48 % Refutation found
% 0.14/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.50 % Elapsed time: 0.115061 seconds
% 0.14/0.50 % CPU time: 0.671746 seconds
% 0.14/0.50 % Total memory used: 115.426 MB
% 0.14/0.50 % Net memory used: 114.221 MB
%------------------------------------------------------------------------------