%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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:03 PM UTC 2026
% Result : Theorem 22.82s 3.64s
% Output : Proof 22.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ078+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n003.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 06:58:35 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.82/3.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.82/3.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.82/3.64 fof(sdef4, definition, (spl4 <=> (truthday(monday))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 22.82/3.64 cnf(p48, plain, (truthday(monday) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 22.82/3.64 fof(sdef1, definition, (spl1 <=> (~truthday(monday))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 22.82/3.64 cnf(p43, plain, (~truthday(monday) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 22.82/3.64 cnf(p93, plain, ($false | ~spl1 | ~spl4), inference(resolution, [status(thm)], [p48, p43])).
% 22.82/3.64 cnf(sct0, plain, (~spl1 | ~spl4), inference(avatar_contradiction_clause, [status(thm)], [p93])).
% 22.82/3.64 fof(f22, conjecture, truthday(tuesday), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', tuesday_leo_tells_truths)).
% 22.82/3.64 fof(f22_neg, negated_conjecture, ~(truthday(tuesday)), inference(negated_conjecture, [status(cth)], [f22])).
% 22.82/3.64 fof(f22_nnf, plain, ~(truthday(tuesday)), inference(nnf_transformation, [status(thm)], [f22_neg])).
% 22.82/3.64 fof(f22_sk, plain, ~(truthday(tuesday)), inference(skolemisation, [status(esa)], [f22_nnf])).
% 22.82/3.64 cnf(c51, plain, ~truthday(tuesday), inference(cnf_transformation, [status(esa)], [f22_sk])).
% 22.82/3.64 fof(sdef5, definition, (spl5 <=> (truthday(tuesday))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 22.82/3.64 cnf(p49, plain, (truthday(tuesday) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 22.82/3.64 cnf(p95, plain, ($false | ~spl5), inference(resolution, [status(thm)], [c51, p49])).
% 22.82/3.64 cnf(sct1, plain, (~spl5), inference(avatar_contradiction_clause, [status(thm)], [p95])).
% 22.82/3.64 fof(sdef11, definition, (spl11 <=> (~day2(thursday))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 22.82/3.64 cnf(p57, plain, (~day2(thursday) | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 22.82/3.64 fof(sdef7, definition, (spl7 <=> (day2(thursday))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 22.82/3.64 cnf(p52, plain, (day2(thursday) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 22.82/3.64 cnf(p97, plain, ($false | ~spl7 | ~spl11), inference(resolution, [status(thm)], [p57, p52])).
% 22.82/3.64 cnf(sct2, plain, (~spl7 | ~spl11), inference(avatar_contradiction_clause, [status(thm)], [p97])).
% 22.82/3.64 fof(sdef12, definition, (spl12 <=> (~day2(saturday))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 22.82/3.64 cnf(p59, plain, (~day2(saturday) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 22.82/3.64 fof(sdef8, definition, (spl8 <=> (day2(saturday))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 22.82/3.64 cnf(p53, plain, (day2(saturday) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 22.82/3.64 cnf(p98, plain, ($false | ~spl8 | ~spl12), inference(resolution, [status(thm)], [p59, p53])).
% 22.82/3.64 cnf(sct3, plain, (~spl8 | ~spl12), inference(avatar_contradiction_clause, [status(thm)], [p98])).
% 22.82/3.64 fof(sdef13, definition, (spl13 <=> (~day2(sunday))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 22.82/3.64 cnf(p61, plain, (~day2(sunday) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 22.82/3.64 fof(sdef9, definition, (spl9 <=> (day2(sunday))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 22.82/3.64 cnf(p54, plain, (day2(sunday) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 22.82/3.64 cnf(p100, plain, ($false | ~spl9 | ~spl13), inference(resolution, [status(thm)], [p61, p54])).
% 22.82/3.64 cnf(sct4, plain, (~spl9 | ~spl13), inference(avatar_contradiction_clause, [status(thm)], [p100])).
% 22.82/3.64 fof(sdef18, definition, (spl18 <=> (truthday(wednesday))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 22.82/3.64 cnf(p69, plain, (truthday(wednesday) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 22.82/3.64 fof(sdef15, definition, (spl15 <=> (~truthday(wednesday))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 22.82/3.64 cnf(p64, plain, (~truthday(wednesday) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 22.82/3.64 cnf(p101, plain, ($false | ~spl15 | ~spl18), inference(resolution, [status(thm)], [p69, p64])).
% 22.82/3.64 cnf(sct5, plain, (~spl15 | ~spl18), inference(avatar_contradiction_clause, [status(thm)], [p101])).
% 22.82/3.64 fof(sdef19, definition, (spl19 <=> (truthday(friday))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 22.82/3.64 cnf(p70, plain, (truthday(friday) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 22.82/3.64 fof(sdef16, definition, (spl16 <=> (~truthday(friday))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 22.82/3.64 cnf(p66, plain, (~truthday(friday) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 22.82/3.64 cnf(p102, plain, ($false | ~spl16 | ~spl19), inference(resolution, [status(thm)], [p70, p66])).
% 22.82/3.64 cnf(sct6, plain, (~spl16 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p102])).
% 22.82/3.64 fof(sdef3, definition, (spl3 <=> (~day1(X0) | truthday(X0))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 22.82/3.64 cnf(p47, plain, (~day1(X0) | truthday(X0) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 22.82/3.64 fof(f7, axiom, ? [X] : day1(X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', day1_once)).
% 22.82/3.64 fof(f7_nnf, plain, ? [X] : (day1(X)), inference(nnf_transformation, [status(thm)], [f7])).
% 22.82/3.64 fof(f7_sk, plain, day1(sk1), inference(skolemisation, [status(esa), new_symbols(skolem, [sk1])], [f7_nnf])).
% 22.82/3.64 cnf(c27, plain, day1(sk1), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 22.82/3.64 cnf(p117, plain, (truthday(sk1) | ~spl3), inference(resolution, [status(thm)], [p47, c27])).
% 22.82/3.64 fof(sdef0, definition, (spl0 <=> (~day1(X0) | ~truthday(X0))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 22.82/3.64 cnf(p42, plain, (~day1(X0) | ~truthday(X0) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 22.82/3.64 cnf(p116, plain, (~truthday(sk1) | ~spl0), inference(resolution, [status(thm)], [p42, c27])).
% 22.82/3.64 cnf(p119, plain, ($false | ~spl0 | ~spl3), inference(resolution, [status(thm)], [p117, p116])).
% 22.82/3.64 cnf(sct7, plain, (~spl0 | ~spl3), inference(avatar_contradiction_clause, [status(thm)], [p119])).
% 22.82/3.64 fof(sdef10, definition, (spl10 <=> (~day2(X0) | truthday(X0))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 22.82/3.64 cnf(p56, plain, (~day2(X0) | truthday(X0) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 22.82/3.64 fof(f8, axiom, ? [X] : day2(X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', day2_once)).
% 22.82/3.64 fof(f8_nnf, plain, ? [X] : (day2(X)), inference(nnf_transformation, [status(thm)], [f8])).
% 22.82/3.64 fof(f8_sk, plain, day2(sk2), inference(skolemisation, [status(esa), new_symbols(skolem, [sk2])], [f8_nnf])).
% 22.82/3.64 cnf(c28, plain, day2(sk2), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 22.82/3.64 cnf(p122, plain, (truthday(sk2) | ~spl10), inference(resolution, [status(thm)], [p56, c28])).
% 22.82/3.64 fof(sdef6, definition, (spl6 <=> (~day2(X0) | ~truthday(X0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 22.82/3.64 cnf(p51, plain, (~day2(X0) | ~truthday(X0) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 22.82/3.64 cnf(p121, plain, (~truthday(sk2) | ~spl6), inference(resolution, [status(thm)], [p51, c28])).
% 22.82/3.64 cnf(p124, plain, ($false | ~spl6 | ~spl10), inference(resolution, [status(thm)], [p122, p121])).
% 22.82/3.64 cnf(sct8, plain, (~spl6 | ~spl10), inference(avatar_contradiction_clause, [status(thm)], [p124])).
% 22.82/3.64 fof(sdef17, definition, (spl17 <=> (~day3(X0) | truthday(X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 22.82/3.64 cnf(p68, plain, (~day3(X0) | truthday(X0) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 22.82/3.64 fof(f9, axiom, ? [X] : day3(X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', day3_once)).
% 22.82/3.64 fof(f9_nnf, plain, ? [X] : (day3(X)), inference(nnf_transformation, [status(thm)], [f9])).
% 22.82/3.64 fof(f9_sk, plain, day3(sk3), inference(skolemisation, [status(esa), new_symbols(skolem, [sk3])], [f9_nnf])).
% 22.82/3.64 cnf(c29, plain, day3(sk3), inference(cnf_transformation, [status(esa)], [f9_sk])).
% 22.82/3.64 cnf(p134, plain, (truthday(sk3) | ~spl17), inference(resolution, [status(thm)], [p68, c29])).
% 22.82/3.64 fof(sdef14, definition, (spl14 <=> (~day3(X0) | ~truthday(X0))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 22.82/3.64 cnf(p63, plain, (~day3(X0) | ~truthday(X0) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 22.82/3.64 cnf(p129, plain, (~truthday(sk3) | ~spl14), inference(resolution, [status(thm)], [p63, c29])).
% 22.82/3.64 cnf(p136, plain, ($false | ~spl14 | ~spl17), inference(resolution, [status(thm)], [p134, p129])).
% 22.82/3.64 cnf(sct9, plain, (~spl14 | ~spl17), inference(avatar_contradiction_clause, [status(thm)], [p136])).
% 22.82/3.64 fof(f15, axiom, consecutive(friday) = saturday, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', saturday_follows_friday)).
% 22.82/3.64 fof(f15_nnf, plain, consecutive(friday) = saturday, inference(nnf_transformation, [status(thm)], [f15])).
% 22.82/3.64 cnf(c35, plain, consecutive(friday) = saturday, inference(cnf_transformation, [status(esa)], [f15_nnf])).
% 22.82/3.64 fof(f17, axiom, ! [X] : ( day1(X) <=> day2(consecutive(X)) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', day2_follows_day1)).
% 22.82/3.64 fof(f17_nnf, plain, ! [X] : (((~(day1(X)) | day2(consecutive(X))) & (day1(X) | ~(day2(consecutive(X)))))), inference(nnf_transformation, [status(thm)], [f17])).
% 22.82/3.64 fof(f17_sk, plain, ! [X] : (((~(day1(X)) | day2(consecutive(X))) & (day1(X) | ~(day2(consecutive(X)))))), inference(skolemisation, [status(esa)], [f17_nnf])).
% 22.82/3.64 cnf(c38, plain, day1(X0) | ~day2(consecutive(X0)), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 22.82/3.64 cnf(p142, plain, day1(friday) | ~day2(saturday), inference(superposition, [status(thm)], [c35, c38])).
% 22.82/3.64 cnf(p162, plain, (day1(friday) | ~spl8), inference(resolution, [status(thm)], [p142, p53])).
% 22.82/3.64 cnf(p179, plain, (~truthday(friday) | ~spl0 | ~spl8), inference(resolution, [status(thm)], [p162, p42])).
% 22.82/3.64 cnf(p180, plain, ($false | ~spl0 | ~spl8 | ~spl19), inference(resolution, [status(thm)], [p179, p70])).
% 22.82/3.64 cnf(sct10, plain, (~spl0 | ~spl8 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p180])).
% 22.82/3.64 fof(f2, axiom, ! [X,Y] : ( ( truthday(X) & truthday(Y) ) => X = Y ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', truth_unique)).
% 22.82/3.64 fof(f2_nnf, plain, ! [X,Y] : (((~(truthday(X)) | ~(truthday(Y))) | X = Y)), inference(nnf_transformation, [status(thm)], [f2])).
% 22.82/3.64 fof(f2_sk, plain, ! [X,Y] : (((~(truthday(X)) | ~(truthday(Y))) | X = Y)), inference(skolemisation, [status(esa)], [f2_nnf])).
% 22.82/3.64 cnf(c22, plain, ~truthday(X0) | ~truthday(X1) | X0 = X1, inference(cnf_transformation, [status(esa)], [f2_sk])).
% 22.82/3.64 fof(f6, axiom, ? [X] : truthday(X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', truth_once)).
% 22.82/3.64 fof(f6_nnf, plain, ? [X] : (truthday(X)), inference(nnf_transformation, [status(thm)], [f6])).
% 22.82/3.64 fof(f6_sk, plain, truthday(sk0), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0])], [f6_nnf])).
% 22.82/3.64 cnf(c26, plain, truthday(sk0), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 22.82/3.64 cnf(p110, plain, ~truthday(X0) | sk0 = X0, inference(resolution, [status(thm)], [c22, c26])).
% 22.82/3.64 cnf(p212, plain, (sk0 = monday | ~spl4), inference(resolution, [status(thm)], [p110, p48])).
% 22.82/3.64 cnf(p213, plain, (sk0 = wednesday | ~spl18), inference(resolution, [status(thm)], [p110, p69])).
% 22.82/3.64 cnf(p232, plain, (monday = wednesday | ~spl4 | ~spl18), inference(superposition, [status(thm)], [p212, p213])).
% 22.82/3.64 fof(f1, axiom, ( monday != tuesday & monday != wednesday & monday != thursday & monday != friday & monday != saturday & monday != sunday & tuesday != wednesday & tuesday != thursday & tuesday != friday & tuesday != saturday & tuesday != sunday & wednesday != thursday & wednesday != friday & wednesday != saturday & wednesday != sunday & thursday != friday & thursday != saturday & thursday != sunday & friday != saturday & friday != sunday & saturday != sunday ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', uniquenames)).
% 22.82/3.64 fof(f1_nnf, plain, ((((((((((((((((((((monday != tuesday & monday != wednesday) & monday != thursday) & monday != friday) & monday != saturday) & monday != sunday) & tuesday != wednesday) & tuesday != thursday) & tuesday != friday) & tuesday != saturday) & tuesday != sunday) & wednesday != thursday) & wednesday != friday) & wednesday != saturday) & wednesday != sunday) & thursday != friday) & thursday != saturday) & thursday != sunday) & friday != saturday) & friday != sunday) & saturday != sunday), inference(nnf_transformation, [status(thm)], [f1])).
% 22.82/3.64 fof(f1_sk, plain, ((((((((((((((((((((monday != tuesday & monday != wednesday) & monday != thursday) & monday != friday) & monday != saturday) & monday != sunday) & tuesday != wednesday) & tuesday != thursday) & tuesday != friday) & tuesday != saturday) & tuesday != sunday) & wednesday != thursday) & wednesday != friday) & wednesday != saturday) & wednesday != sunday) & thursday != friday) & thursday != saturday) & thursday != sunday) & friday != saturday) & friday != sunday) & saturday != sunday), inference(skolemisation, [status(esa)], [f1_nnf])).
% 22.82/3.64 cnf(c2, plain, monday != wednesday, inference(cnf_transformation, [status(esa)], [f1_sk])).
% 22.82/3.64 cnf(p303, plain, ($false | ~spl4 | ~spl18), inference(resolution, [status(thm)], [p232, c2])).
% 22.82/3.64 cnf(sct11, plain, (~spl4 | ~spl18), inference(avatar_contradiction_clause, [status(thm)], [p303])).
% 22.82/3.64 fof(f18, axiom, ! [X] : ( day2(X) <=> day3(consecutive(X)) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', day3_follows_day2)).
% 22.82/3.64 fof(f18_nnf, plain, ! [X] : (((~(day2(X)) | day3(consecutive(X))) & (day2(X) | ~(day3(consecutive(X)))))), inference(nnf_transformation, [status(thm)], [f18])).
% 22.82/3.64 fof(f18_sk, plain, ! [X] : (((~(day2(X)) | day3(consecutive(X))) & (day2(X) | ~(day3(consecutive(X)))))), inference(skolemisation, [status(esa)], [f18_nnf])).
% 22.82/3.64 cnf(c39, plain, ~day2(X0) | day3(consecutive(X0)), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 22.82/3.64 cnf(p307, plain, (day3(friday) | ~spl7), inference(resolution, [status(thm)], [p52, c39])).
% 22.82/3.64 cnf(p335, plain, (~truthday(friday) | ~spl7 | ~spl14), inference(resolution, [status(thm)], [p307, p63])).
% 22.82/3.64 cnf(p336, plain, ($false | ~spl7 | ~spl14 | ~spl19), inference(resolution, [status(thm)], [p335, p70])).
% 22.82/3.64 cnf(sct12, plain, (~spl7 | ~spl14 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p336])).
% 22.82/3.64 cnf(p347, plain, (truthday(sunday) | ~spl9 | ~spl10), inference(resolution, [status(thm)], [p54, p56])).
% 22.82/3.64 cnf(p214, plain, (sk0 = sk2 | ~spl10), inference(resolution, [status(thm)], [p110, p122])).
% 22.82/3.64 cnf(p233, plain, (day2(sk0) | ~spl10), inference(superposition, [status(thm)], [p214, c28])).
% 22.82/3.64 cnf(p239, plain, (day2(monday) | ~spl4 | ~spl10), inference(superposition, [status(thm)], [p212, p233])).
% 22.82/3.64 fof(f10, axiom, consecutive(sunday) = monday, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', monday_follows_sunday)).
% 22.82/3.64 fof(f10_nnf, plain, consecutive(sunday) = monday, inference(nnf_transformation, [status(thm)], [f10])).
% 22.82/3.64 cnf(c30, plain, consecutive(sunday) = monday, inference(cnf_transformation, [status(esa)], [f10_nnf])).
% 22.82/3.64 cnf(p137, plain, day1(sunday) | ~day2(monday), inference(superposition, [status(thm)], [c30, c38])).
% 22.82/3.64 cnf(p255, plain, (day1(sunday) | ~spl4 | ~spl10), inference(resolution, [status(thm)], [p239, p137])).
% 22.82/3.64 cnf(p262, plain, (~truthday(sunday) | ~spl0 | ~spl4 | ~spl10), inference(resolution, [status(thm)], [p255, p42])).
% 22.82/3.64 cnf(p353, plain, ($false | ~spl0 | ~spl4 | ~spl9 | ~spl10), inference(resolution, [status(thm)], [p347, p262])).
% 22.82/3.64 cnf(sct13, plain, (~spl0 | ~spl4 | ~spl9 | ~spl10), inference(avatar_contradiction_clause, [status(thm)], [p353])).
% 22.82/3.64 cnf(p363, plain, (sk0 = sk3 | ~spl17), inference(resolution, [status(thm)], [p134, p110])).
% 22.82/3.64 cnf(p377, plain, (day3(sk0) | ~spl17), inference(superposition, [status(thm)], [p363, c29])).
% 22.82/3.64 cnf(p381, plain, (day3(monday) | ~spl4 | ~spl17), inference(superposition, [status(thm)], [p212, p377])).
% 22.82/3.64 cnf(c40, plain, day2(X0) | ~day3(consecutive(X0)), inference(cnf_transformation, [status(esa)], [f18_sk])).
% 22.82/3.64 cnf(p153, plain, day2(sunday) | ~day3(monday), inference(superposition, [status(thm)], [c30, c40])).
% 22.82/3.64 cnf(p391, plain, (day2(sunday) | ~spl4 | ~spl17), inference(resolution, [status(thm)], [p381, p153])).
% 22.82/3.64 cnf(p395, plain, ($false | ~spl4 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p391, p61])).
% 22.82/3.64 cnf(sct14, plain, (~spl4 | ~spl13 | ~spl17), inference(avatar_contradiction_clause, [status(thm)], [p395])).
% 22.82/3.64 cnf(p397, plain, (truthday(sunday) | ~spl4 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p391, p56])).
% 22.82/3.64 cnf(p411, plain, ($false | ~spl0 | ~spl4 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p397, p262])).
% 22.82/3.64 cnf(sct15, plain, (~spl0 | ~spl4 | ~spl10 | ~spl17), inference(avatar_contradiction_clause, [status(thm)], [p411])).
% 22.82/3.64 cnf(p319, plain, (sk0 = friday | ~spl19), inference(resolution, [status(thm)], [p70, p110])).
% 22.82/3.64 cnf(p418, plain, (monday = friday | ~spl4 | ~spl19), inference(superposition, [status(thm)], [p212, p319])).
% 22.82/3.64 cnf(c4, plain, monday != friday, inference(cnf_transformation, [status(esa)], [f1_sk])).
% 22.82/3.64 cnf(p432, plain, ($false | ~spl4 | ~spl19), inference(resolution, [status(thm)], [p418, c4])).
% 22.82/3.64 cnf(sct16, plain, (~spl4 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p432])).
% 22.82/3.64 cnf(p240, plain, (day2(wednesday) | ~spl10 | ~spl18), inference(superposition, [status(thm)], [p213, p233])).
% 22.82/3.64 fof(f12, axiom, consecutive(tuesday) = wednesday, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', wednesday_follows_tuesday)).
% 22.82/3.64 fof(f12_nnf, plain, consecutive(tuesday) = wednesday, inference(nnf_transformation, [status(thm)], [f12])).
% 22.82/3.64 cnf(c32, plain, consecutive(tuesday) = wednesday, inference(cnf_transformation, [status(esa)], [f12_nnf])).
% 22.82/3.64 cnf(p139, plain, day1(tuesday) | ~day2(wednesday), inference(superposition, [status(thm)], [c32, c38])).
% 22.82/3.64 cnf(p258, plain, (day1(tuesday) | ~spl10 | ~spl18), inference(resolution, [status(thm)], [p240, p139])).
% 22.82/3.64 cnf(p445, plain, (truthday(tuesday) | ~spl3 | ~spl10 | ~spl18), inference(resolution, [status(thm)], [p258, p47])).
% 22.82/3.64 fof(sdef2, definition, (spl2 <=> (~truthday(tuesday))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 22.82/3.64 cnf(p45, plain, (~truthday(tuesday) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 22.82/3.64 cnf(p452, plain, ($false | ~spl2 | ~spl3 | ~spl10 | ~spl18), inference(resolution, [status(thm)], [p445, p45])).
% 22.82/3.64 cnf(sct17, plain, (~spl2 | ~spl3 | ~spl10 | ~spl18), inference(avatar_contradiction_clause, [status(thm)], [p452])).
% 22.82/3.64 cnf(p442, plain, (day2(friday) | ~spl10 | ~spl19), inference(superposition, [status(thm)], [p319, p233])).
% 22.82/3.64 cnf(p450, plain, (day3(saturday) | ~spl10 | ~spl19), inference(resolution, [status(thm)], [p442, c39])).
% 22.82/3.64 cnf(p454, plain, (~truthday(saturday) | ~spl10 | ~spl14 | ~spl19), inference(resolution, [status(thm)], [p450, p63])).
% 22.82/3.64 cnf(p127, plain, (truthday(saturday) | ~spl8 | ~spl10), inference(resolution, [status(thm)], [p53, p56])).
% 22.82/3.64 cnf(p457, plain, ($false | ~spl8 | ~spl10 | ~spl14 | ~spl19), inference(resolution, [status(thm)], [p454, p127])).
% 22.82/3.64 cnf(sct18, plain, (~spl8 | ~spl10 | ~spl14 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p457])).
% 22.82/3.64 fof(f16, axiom, consecutive(saturday) = sunday, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sunday_follows_saturday)).
% 22.82/3.64 fof(f16_nnf, plain, consecutive(saturday) = sunday, inference(nnf_transformation, [status(thm)], [f16])).
% 22.82/3.64 cnf(c36, plain, consecutive(saturday) = sunday, inference(cnf_transformation, [status(esa)], [f16_nnf])).
% 22.82/3.64 cnf(p143, plain, day1(saturday) | ~day2(sunday), inference(superposition, [status(thm)], [c36, c38])).
% 22.82/3.64 cnf(p349, plain, (day1(saturday) | ~spl9), inference(resolution, [status(thm)], [p54, p143])).
% 22.82/3.64 cnf(p488, plain, (truthday(saturday) | ~spl3 | ~spl9), inference(resolution, [status(thm)], [p349, p47])).
% 22.82/3.64 cnf(p509, plain, ($false | ~spl3 | ~spl9 | ~spl10 | ~spl14 | ~spl19), inference(resolution, [status(thm)], [p488, p454])).
% 22.82/3.64 cnf(sct19, plain, (~spl3 | ~spl9 | ~spl10 | ~spl14 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p509])).
% 22.82/3.64 cnf(p441, plain, (truthday(friday) | ~spl3 | ~spl8), inference(resolution, [status(thm)], [p162, p47])).
% 22.82/3.64 cnf(p525, plain, ($false | ~spl3 | ~spl8 | ~spl16), inference(resolution, [status(thm)], [p66, p441])).
% 22.82/3.64 cnf(sct20, plain, (~spl3 | ~spl8 | ~spl16), inference(avatar_contradiction_clause, [status(thm)], [p525])).
% 22.82/3.64 cnf(p305, plain, (truthday(thursday) | ~spl7 | ~spl10), inference(resolution, [status(thm)], [p52, p56])).
% 22.82/3.64 cnf(p321, plain, (sk0 = thursday | ~spl7 | ~spl10), inference(resolution, [status(thm)], [p305, p110])).
% 22.82/3.64 cnf(p382, plain, (day3(thursday) | ~spl7 | ~spl10 | ~spl17), inference(superposition, [status(thm)], [p321, p377])).
% 22.82/3.64 fof(f13, axiom, consecutive(wednesday) = thursday, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thursday_follows_wednesday)).
% 22.82/3.64 fof(f13_nnf, plain, consecutive(wednesday) = thursday, inference(nnf_transformation, [status(thm)], [f13])).
% 22.82/3.64 cnf(c33, plain, consecutive(wednesday) = thursday, inference(cnf_transformation, [status(esa)], [f13_nnf])).
% 22.82/3.64 cnf(p156, plain, day2(wednesday) | ~day3(thursday), inference(superposition, [status(thm)], [c33, c40])).
% 22.82/3.64 cnf(p393, plain, (day2(wednesday) | ~spl7 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p382, p156])).
% 22.82/3.64 cnf(p400, plain, (truthday(wednesday) | ~spl7 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p393, p56])).
% 22.82/3.64 cnf(p558, plain, ($false | ~spl7 | ~spl10 | ~spl15 | ~spl17), inference(resolution, [status(thm)], [p400, p64])).
% 22.82/3.64 cnf(sct21, plain, (~spl7 | ~spl10 | ~spl15 | ~spl17), inference(avatar_contradiction_clause, [status(thm)], [p558])).
% 22.82/3.64 cnf(p352, plain, (sk0 = sunday | ~spl9 | ~spl10), inference(resolution, [status(thm)], [p347, p110])).
% 22.82/3.64 cnf(p593, plain, (day3(sunday) | ~spl9 | ~spl10 | ~spl17), inference(superposition, [status(thm)], [p352, p377])).
% 22.82/3.64 cnf(p159, plain, day2(saturday) | ~day3(sunday), inference(superposition, [status(thm)], [c36, c40])).
% 22.82/3.64 cnf(p619, plain, (day2(saturday) | ~spl9 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p593, p159])).
% 22.82/3.64 cnf(p620, plain, ($false | ~spl9 | ~spl10 | ~spl12 | ~spl17), inference(resolution, [status(thm)], [p619, p59])).
% 22.82/3.64 cnf(sct22, plain, (~spl9 | ~spl10 | ~spl12 | ~spl17), inference(avatar_contradiction_clause, [status(thm)], [p620])).
% 22.82/3.64 cnf(p623, plain, (day1(friday) | ~spl9 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p619, p142])).
% 22.82/3.64 cnf(p632, plain, (truthday(friday) | ~spl3 | ~spl9 | ~spl10 | ~spl17), inference(resolution, [status(thm)], [p623, p47])).
% 22.82/3.64 cnf(p669, plain, ($false | ~spl3 | ~spl9 | ~spl10 | ~spl16 | ~spl17), inference(resolution, [status(thm)], [p632, p66])).
% 22.82/3.64 cnf(sct23, plain, (~spl3 | ~spl9 | ~spl10 | ~spl16 | ~spl17), inference(avatar_contradiction_clause, [status(thm)], [p669])).
% 22.82/3.64 cnf(p118, plain, (~truthday(X0) | sk1 = X0 | ~spl3), inference(resolution, [status(thm)], [p117, c22])).
% 22.82/3.64 cnf(p671, plain, (sk1 = sk0 | ~spl3), inference(resolution, [status(thm)], [p118, c26])).
% 22.82/3.64 cnf(p676, plain, (day1(sk0) | ~spl3), inference(superposition, [status(thm)], [p671, c27])).
% 22.82/3.64 cnf(p682, plain, (day1(wednesday) | ~spl3 | ~spl18), inference(superposition, [status(thm)], [p213, p676])).
% 22.82/3.64 cnf(c37, plain, ~day1(X0) | day2(consecutive(X0)), inference(cnf_transformation, [status(esa)], [f17_sk])).
% 22.82/3.64 cnf(p685, plain, (day2(thursday) | ~spl3 | ~spl18), inference(resolution, [status(thm)], [p682, c37])).
% 22.82/3.64 cnf(p688, plain, ($false | ~spl3 | ~spl11 | ~spl18), inference(resolution, [status(thm)], [p685, p57])).
% 22.82/3.64 cnf(sct24, plain, (~spl3 | ~spl11 | ~spl18), inference(avatar_contradiction_clause, [status(thm)], [p688])).
% 22.82/3.64 cnf(p683, plain, (day1(friday) | ~spl3 | ~spl19), inference(superposition, [status(thm)], [p319, p676])).
% 22.82/3.64 cnf(p687, plain, (day2(saturday) | ~spl3 | ~spl19), inference(resolution, [status(thm)], [p683, c37])).
% 22.82/3.64 cnf(p691, plain, ($false | ~spl3 | ~spl12 | ~spl19), inference(resolution, [status(thm)], [p687, p59])).
% 22.82/3.64 cnf(sct25, plain, (~spl3 | ~spl12 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p691])).
% 22.82/3.64 fof(f0, axiom, ! [X] : ( X = monday | X = tuesday | X = wednesday | X = thursday | X = friday | X = saturday | X = sunday ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', days_of_week)).
% 22.82/3.64 fof(f0_nnf, plain, ! [X] : (((((((X = monday | X = tuesday) | X = wednesday) | X = thursday) | X = friday) | X = saturday) | X = sunday)), inference(nnf_transformation, [status(thm)], [f0])).
% 22.82/3.64 fof(f0_sk, plain, ! [X] : (((((((X = monday | X = tuesday) | X = wednesday) | X = thursday) | X = friday) | X = saturday) | X = sunday)), inference(skolemisation, [status(esa)], [f0_nnf])).
% 22.82/3.64 cnf(c0, plain, X0 = monday | X0 = tuesday | X0 = wednesday | X0 = thursday | X0 = friday | X0 = saturday | X0 = sunday, inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.82/3.64 cnf(p99, plain, (X0 = monday | X0 = tuesday | X0 = wednesday | X0 = thursday | X0 = friday | X0 = saturday | ~day2(X0) | ~spl13), inference(superposition, [status(thm)], [c0, p61])).
% 22.82/3.64 cnf(p781, plain, (sk2 = monday | sk2 = tuesday | sk2 = wednesday | sk2 = thursday | sk2 = friday | sk2 = saturday | ~spl13), inference(resolution, [status(thm)], [p99, c28])).
% 22.82/3.64 cnf(p805, plain, (sk2 = monday | sk2 = tuesday | sk2 = wednesday | sk2 = thursday | sk2 = friday | day2(saturday) | ~spl13), inference(superposition, [status(thm)], [p781, c28])).
% 22.82/3.64 cnf(p825, plain, (sk2 = monday | sk2 = tuesday | sk2 = wednesday | sk2 = thursday | day2(saturday) | day2(friday) | ~spl13), inference(superposition, [status(thm)], [p805, c28])).
% 22.82/3.64 cnf(p840, plain, (sk2 = monday | sk2 = tuesday | sk2 = wednesday | day2(saturday) | day2(friday) | day2(thursday) | ~spl13), inference(superposition, [status(thm)], [p825, c28])).
% 22.82/3.64 cnf(p852, plain, (sk2 = monday | sk2 = tuesday | day2(saturday) | day2(friday) | day2(thursday) | day2(wednesday) | ~spl13), inference(superposition, [status(thm)], [p840, c28])).
% 22.82/3.64 cnf(p869, plain, (sk2 = monday | day2(saturday) | day2(friday) | day2(thursday) | day2(wednesday) | day2(tuesday) | ~spl13), inference(superposition, [status(thm)], [p852, c28])).
% 22.82/3.64 cnf(p877, plain, (day2(saturday) | day2(friday) | day2(thursday) | day2(wednesday) | day2(tuesday) | day2(monday) | ~spl13), inference(superposition, [status(thm)], [p869, c28])).
% 22.82/3.64 cnf(p886, plain, (day2(friday) | day2(thursday) | day2(wednesday) | day2(tuesday) | day2(monday) | ~spl12 | ~spl13), inference(resolution, [status(thm)], [p877, p59])).
% 22.82/3.64 fof(f14, axiom, consecutive(thursday) = friday, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', friday_follows_thursday)).
% 22.82/3.64 fof(f14_nnf, plain, consecutive(thursday) = friday, inference(nnf_transformation, [status(thm)], [f14])).
% 22.82/3.64 cnf(c34, plain, consecutive(thursday) = friday, inference(cnf_transformation, [status(esa)], [f14_nnf])).
% 22.82/3.64 cnf(p141, plain, day1(thursday) | ~day2(friday), inference(superposition, [status(thm)], [c34, c38])).
% 22.82/3.64 cnf(p896, plain, (day2(thursday) | day2(wednesday) | day2(tuesday) | day2(monday) | day1(thursday) | ~spl12 | ~spl13), inference(resolution, [status(thm)], [p886, p141])).
% 22.82/3.64 cnf(p910, plain, (day2(wednesday) | day2(tuesday) | day2(monday) | day1(thursday) | ~spl11 | ~spl12 | ~spl13), inference(resolution, [status(thm)], [p896, p57])).
% 22.82/3.64 cnf(p918, plain, (day2(tuesday) | day2(monday) | day1(thursday) | day1(tuesday) | ~spl11 | ~spl12 | ~spl13), inference(resolution, [status(thm)], [p910, p139])).
% 22.82/3.64 fof(f11, axiom, consecutive(monday) = tuesday, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', tuesday_follows_monday)).
% 22.82/3.64 fof(f11_nnf, plain, consecutive(monday) = tuesday, inference(nnf_transformation, [status(thm)], [f11])).
% 22.82/3.64 cnf(c31, plain, consecutive(monday) = tuesday, inference(cnf_transformation, [status(esa)], [f11_nnf])).
% 22.82/3.64 cnf(p138, plain, day1(monday) | ~day2(tuesday), inference(superposition, [status(thm)], [c31, c38])).
% 22.82/3.64 cnf(p928, plain, (day2(monday) | day1(thursday) | day1(tuesday) | day1(monday) | ~spl11 | ~spl12 | ~spl13), inference(resolution, [status(thm)], [p918, p138])).
% 22.82/3.64 cnf(p938, plain, (day1(thursday) | day1(tuesday) | day1(monday) | day3(tuesday) | ~spl11 | ~spl12 | ~spl13), inference(resolution, [status(thm)], [p928, c39])).
% 22.82/3.64 cnf(p963, plain, (day1(thursday) | day1(tuesday) | day1(monday) | truthday(tuesday) | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p938, p68])).
% 22.82/3.64 cnf(p988, plain, (day1(tuesday) | day1(monday) | truthday(tuesday) | truthday(thursday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p963, p47])).
% 22.82/3.64 cnf(p1027, plain, (day1(monday) | truthday(tuesday) | truthday(thursday) | truthday(tuesday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p988, p47])).
% 22.82/3.64 cnf(p1100, plain, (day1(monday) | truthday(tuesday) | truthday(thursday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(factoring, [status(thm)], [p1027])).
% 22.82/3.64 fof(f3, axiom, ! [X,Y] : ( ( day1(X) & day1(Y) ) => X = Y ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', day1_unique)).
% 22.82/3.64 fof(f3_nnf, plain, ! [X,Y] : (((~(day1(X)) | ~(day1(Y))) | X = Y)), inference(nnf_transformation, [status(thm)], [f3])).
% 22.82/3.64 fof(f3_sk, plain, ! [X,Y] : (((~(day1(X)) | ~(day1(Y))) | X = Y)), inference(skolemisation, [status(esa)], [f3_nnf])).
% 22.82/3.64 cnf(c23, plain, ~day1(X0) | ~day1(X1) | X0 = X1, inference(cnf_transformation, [status(esa)], [f3_sk])).
% 22.82/3.64 cnf(p115, plain, ~day1(X0) | sk1 = X0, inference(resolution, [status(thm)], [c23, c27])).
% 22.82/3.64 cnf(p1104, plain, (truthday(tuesday) | truthday(thursday) | sk0 = monday | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1100, p115])).
% 22.82/3.64 cnf(p1125, plain, (truthday(tuesday) | truthday(thursday) | day3(monday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(superposition, [status(thm)], [p1104, p377])).
% 22.82/3.64 cnf(p1130, plain, (truthday(tuesday) | truthday(thursday) | day2(sunday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1125, p153])).
% 22.82/3.64 cnf(p1141, plain, (truthday(tuesday) | truthday(thursday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1130, p61])).
% 22.82/3.64 cnf(p1143, plain, (truthday(tuesday) | sk0 = thursday | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1141, p110])).
% 22.82/3.64 cnf(p1144, plain, (truthday(tuesday) | day3(thursday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(superposition, [status(thm)], [p1143, p377])).
% 22.82/3.64 cnf(p1149, plain, (truthday(tuesday) | day2(wednesday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1144, p156])).
% 22.82/3.64 cnf(p1163, plain, (truthday(tuesday) | day1(tuesday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1149, p139])).
% 22.82/3.64 cnf(p1178, plain, (truthday(tuesday) | truthday(tuesday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1163, p47])).
% 22.82/3.64 cnf(p1184, plain, (truthday(tuesday) | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(factoring, [status(thm)], [p1178])).
% 22.82/3.64 cnf(p1192, plain, ($false | ~spl2 | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(resolution, [status(thm)], [p1184, p45])).
% 22.82/3.64 cnf(sct26, plain, (~spl2 | ~spl3 | ~spl11 | ~spl12 | ~spl13 | ~spl17), inference(avatar_contradiction_clause, [status(thm)], [p1192])).
% 22.82/3.64 fof(f19, axiom, ! [X] : ( day1(X) => ( truthday(X) <=> ( ~ truthday(monday) & ~ truthday(tuesday) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', statement1)).
% 22.82/3.64 fof(f19_nnf, plain, ! [X] : ((~(day1(X)) | ((~(truthday(X)) | (~(truthday(monday)) & ~(truthday(tuesday)))) & (truthday(X) | (truthday(monday) | truthday(tuesday)))))), inference(nnf_transformation, [status(thm)], [f19])).
% 22.82/3.64 fof(f19_sk, plain, ! [X] : ((~(day1(X)) | ((~(truthday(X)) | (~(truthday(monday)) & ~(truthday(tuesday)))) & (truthday(X) | (truthday(monday) | truthday(tuesday)))))), inference(skolemisation, [status(esa)], [f19_nnf])).
% 22.82/3.64 cnf(c41, plain, ~day1(X0) | ~truthday(X0) | ~truthday(monday), inference(cnf_transformation, [status(esa)], [f19_sk])).
% 22.82/3.64 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [c41, sdef0, sdef1])).
% 22.82/3.64 cnf(c42, plain, ~day1(X0) | ~truthday(X0) | ~truthday(tuesday), inference(cnf_transformation, [status(esa)], [f19_sk])).
% 22.82/3.64 cnf(ssp1, plain, (spl0 | spl2), inference(avatar_split_clause, [status(thm)], [c42, sdef0, sdef2])).
% 22.82/3.64 cnf(c43, plain, ~day1(X0) | truthday(X0) | truthday(monday) | truthday(tuesday), inference(cnf_transformation, [status(esa)], [f19_sk])).
% 22.82/3.64 cnf(ssp2, plain, (spl3 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [c43, sdef3, sdef4, sdef5])).
% 22.82/3.64 fof(f20, axiom, ! [X] : ( day2(X) => ( truthday(X) <=> ( day2(thursday) | day2(saturday) | day2(sunday) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', statement2)).
% 22.82/3.64 fof(f20_nnf, plain, ! [X] : ((~(day2(X)) | ((~(truthday(X)) | ((day2(thursday) | day2(saturday)) | day2(sunday))) & (truthday(X) | ((~(day2(thursday)) & ~(day2(saturday))) & ~(day2(sunday))))))), inference(nnf_transformation, [status(thm)], [f20])).
% 22.82/3.64 fof(f20_sk, plain, ! [X] : ((~(day2(X)) | ((~(truthday(X)) | ((day2(thursday) | day2(saturday)) | day2(sunday))) & (truthday(X) | ((~(day2(thursday)) & ~(day2(saturday))) & ~(day2(sunday))))))), inference(skolemisation, [status(esa)], [f20_nnf])).
% 22.82/3.64 cnf(c44, plain, ~day2(X0) | ~truthday(X0) | day2(thursday) | day2(saturday) | day2(sunday), inference(cnf_transformation, [status(esa)], [f20_sk])).
% 22.82/3.64 cnf(ssp3, plain, (spl6 | spl7 | spl8 | spl9), inference(avatar_split_clause, [status(thm)], [c44, sdef6, sdef7, sdef8, sdef9])).
% 22.82/3.64 cnf(c45, plain, ~day2(X0) | truthday(X0) | ~day2(thursday), inference(cnf_transformation, [status(esa)], [f20_sk])).
% 22.82/3.64 cnf(ssp4, plain, (spl10 | spl11), inference(avatar_split_clause, [status(thm)], [c45, sdef10, sdef11])).
% 22.82/3.64 cnf(c46, plain, ~day2(X0) | truthday(X0) | ~day2(saturday), inference(cnf_transformation, [status(esa)], [f20_sk])).
% 22.82/3.64 cnf(ssp5, plain, (spl10 | spl12), inference(avatar_split_clause, [status(thm)], [c46, sdef10, sdef12])).
% 22.82/3.64 cnf(c47, plain, ~day2(X0) | truthday(X0) | ~day2(sunday), inference(cnf_transformation, [status(esa)], [f20_sk])).
% 22.82/3.64 cnf(ssp6, plain, (spl10 | spl13), inference(avatar_split_clause, [status(thm)], [c47, sdef10, sdef13])).
% 22.82/3.64 fof(f21, axiom, ! [X] : ( day3(X) => ( truthday(X) <=> ( ~ truthday(wednesday) & ~ truthday(friday) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', statement3)).
% 22.82/3.64 fof(f21_nnf, plain, ! [X] : ((~(day3(X)) | ((~(truthday(X)) | (~(truthday(wednesday)) & ~(truthday(friday)))) & (truthday(X) | (truthday(wednesday) | truthday(friday)))))), inference(nnf_transformation, [status(thm)], [f21])).
% 22.82/3.64 fof(f21_sk, plain, ! [X] : ((~(day3(X)) | ((~(truthday(X)) | (~(truthday(wednesday)) & ~(truthday(friday)))) & (truthday(X) | (truthday(wednesday) | truthday(friday)))))), inference(skolemisation, [status(esa)], [f21_nnf])).
% 22.82/3.64 cnf(c48, plain, ~day3(X0) | ~truthday(X0) | ~truthday(wednesday), inference(cnf_transformation, [status(esa)], [f21_sk])).
% 22.82/3.64 cnf(ssp7, plain, (spl14 | spl15), inference(avatar_split_clause, [status(thm)], [c48, sdef14, sdef15])).
% 22.82/3.64 cnf(c49, plain, ~day3(X0) | ~truthday(X0) | ~truthday(friday), inference(cnf_transformation, [status(esa)], [f21_sk])).
% 22.82/3.64 cnf(ssp8, plain, (spl14 | spl16), inference(avatar_split_clause, [status(thm)], [c49, sdef14, sdef16])).
% 22.82/3.64 cnf(c50, plain, ~day3(X0) | truthday(X0) | truthday(wednesday) | truthday(friday), inference(cnf_transformation, [status(esa)], [f21_sk])).
% 22.82/3.64 cnf(ssp9, plain, (spl17 | spl18 | spl19), inference(avatar_split_clause, [status(thm)], [c50, sdef17, sdef18, sdef19])).
% 22.82/3.64 cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19, sct20, sct21, sct22, sct23, sct24, sct25, sct26])).
% 22.82/3.64 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------