%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ005-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:13 PM UTC 2026
% Result : Unsatisfiable 0.13s 5.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ005-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n001.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 03:50:19 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.13/5.40 % Refutation found
% 0.13/5.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/5.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.40 fof(f4,axiom,(
% 0.13/5.40 (![X]: (( ~ monday(X)| ~ thursday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f5,axiom,(
% 0.13/5.40 (![X]: (( ~ monday(X)| ~ friday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f6,axiom,(
% 0.13/5.40 (![X]: (( ~ monday(X)| ~ saturday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f9,axiom,(
% 0.13/5.40 (![X]: (( ~ tuesday(X)| ~ thursday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f10,axiom,(
% 0.13/5.40 (![X]: (( ~ tuesday(X)| ~ friday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f11,axiom,(
% 0.13/5.40 (![X]: (( ~ tuesday(X)| ~ saturday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f12,axiom,(
% 0.13/5.40 (![X]: (( ~ tuesday(X)| ~ sunday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f14,axiom,(
% 0.13/5.40 (![X]: (( ~ wednesday(X)| ~ friday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f15,axiom,(
% 0.13/5.40 (![X]: (( ~ wednesday(X)| ~ saturday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f22,axiom,(
% 0.13/5.40 (![X]: (( ~ saturday(X)| ~ sunday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f24,axiom,(
% 0.13/5.40 (![X]: (( ~ tuesday(yesterday(X))| wednesday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f25,axiom,(
% 0.13/5.40 (![X]: (( ~ wednesday(yesterday(X))| thursday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f26,axiom,(
% 0.13/5.40 (![X]: (( ~ thursday(yesterday(X))| friday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f27,axiom,(
% 0.13/5.40 (![X]: (( ~ friday(yesterday(X))| saturday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f28,axiom,(
% 0.13/5.40 (![X]: (( ~ saturday(yesterday(X))| sunday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f31,axiom,(
% 0.13/5.40 (![X]: (( tuesday(yesterday(X))| ~ wednesday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f33,axiom,(
% 0.13/5.40 (![X]: (( thursday(yesterday(X))| ~ friday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f34,axiom,(
% 0.13/5.40 (![X]: (( friday(yesterday(X))| ~ saturday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f36,axiom,(
% 0.13/5.40 (![X]: (( sunday(yesterday(X))| ~ monday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f37,axiom,(
% 0.13/5.40 (![X]: (( ~ member(X,lying_days(lion))| monday(X)| tuesday(X)| wednesday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f38,axiom,(
% 0.13/5.40 (![X]: (( ~ member(X,lying_days(unicorn))| thursday(X)| friday(X)| saturday(X) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f45,axiom,(
% 0.13/5.40 (![X,T,Y]: (( member(X,lying_days(T))| ~ admits(T,X,Y)| member(Y,lying_days(T)) ) ))),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f49,axiom,(
% 0.13/5.40 admits(lion,today,yesterday(today)) ),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f50,axiom,(
% 0.13/5.40 admits(unicorn,today,yesterday(today)) ),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f51,negated_conjecture,(
% 0.13/5.40 ~ thursday(today) ),
% 0.13/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.40 fof(f55,plain,(
% 0.13/5.40 ![X0]: (~monday(X0)|~thursday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/5.40 fof(f56,plain,(
% 0.13/5.40 ![X0]: (~monday(X0)|~friday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/5.40 fof(f57,plain,(
% 0.13/5.40 ![X0]: (~monday(X0)|~saturday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/5.40 fof(f60,plain,(
% 0.13/5.40 ![X0]: (~tuesday(X0)|~thursday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/5.40 fof(f61,plain,(
% 0.13/5.40 ![X0]: (~tuesday(X0)|~friday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/5.40 fof(f62,plain,(
% 0.13/5.40 ![X0]: (~tuesday(X0)|~saturday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/5.40 fof(f63,plain,(
% 0.13/5.40 ![X0]: (~tuesday(X0)|~sunday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/5.40 fof(f65,plain,(
% 0.13/5.40 ![X0]: (~wednesday(X0)|~friday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/5.40 fof(f66,plain,(
% 0.13/5.40 ![X0]: (~wednesday(X0)|~saturday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/5.40 fof(f73,plain,(
% 0.13/5.40 ![X0]: (~saturday(X0)|~sunday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.13/5.40 fof(f75,plain,(
% 0.13/5.40 ![X0]: (~tuesday(yesterday(X0))|wednesday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/5.40 fof(f76,plain,(
% 0.13/5.40 ![X0]: (~wednesday(yesterday(X0))|thursday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/5.40 fof(f77,plain,(
% 0.13/5.40 ![X0]: (~thursday(yesterday(X0))|friday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/5.40 fof(f78,plain,(
% 0.13/5.40 ![X0]: (~friday(yesterday(X0))|saturday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f27])).
% 0.13/5.40 fof(f79,plain,(
% 0.13/5.40 ![X0]: (~saturday(yesterday(X0))|sunday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/5.40 fof(f82,plain,(
% 0.13/5.40 ![X0]: (tuesday(yesterday(X0))|~wednesday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f31])).
% 0.13/5.40 fof(f84,plain,(
% 0.13/5.40 ![X0]: (thursday(yesterday(X0))|~friday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f33])).
% 0.13/5.40 fof(f85,plain,(
% 0.13/5.40 ![X0]: (friday(yesterday(X0))|~saturday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f34])).
% 0.13/5.40 fof(f87,plain,(
% 0.13/5.40 ![X0]: (sunday(yesterday(X0))|~monday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f36])).
% 0.13/5.40 fof(f88,plain,(
% 0.13/5.40 ![X0]: (~member(X0,lying_days(lion))|monday(X0)|tuesday(X0)|wednesday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f37])).
% 0.13/5.40 fof(f89,plain,(
% 0.13/5.40 ![X0]: (~member(X0,lying_days(unicorn))|thursday(X0)|friday(X0)|saturday(X0))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/5.40 fof(f96,plain,(
% 0.13/5.40 ![T,Y]: ((![X]: (member(X,lying_days(T))|~admits(T,X,Y)))|member(Y,lying_days(T)))),
% 0.13/5.40 inference(miniscoping,[status(thm)],[f45])).
% 0.13/5.40 fof(f97,plain,(
% 0.13/5.40 ![X0,X1,X2]: (member(X0,lying_days(X1))|~admits(X1,X0,X2)|member(X2,lying_days(X1)))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f96])).
% 0.13/5.40 fof(f104,plain,(
% 0.13/5.40 admits(lion,today,yesterday(today))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f49])).
% 0.13/5.40 fof(f105,plain,(
% 0.13/5.40 admits(unicorn,today,yesterday(today))),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f50])).
% 0.13/5.40 fof(f106,plain,(
% 0.13/5.40 ~thursday(today)),
% 0.13/5.40 inference(cnf_transformation,[status(thm)],[f51])).
% 0.13/5.40 fof(f110,plain,(
% 0.13/5.40 member(today,lying_days(unicorn))|member(yesterday(today),lying_days(unicorn))),
% 0.13/5.40 inference(resolution,[status(thm)],[f97,f105])).
% 0.13/5.40 fof(f111,plain,(
% 0.13/5.40 member(today,lying_days(lion))|member(yesterday(today),lying_days(lion))),
% 0.13/5.40 inference(resolution,[status(thm)],[f97,f104])).
% 0.13/5.40 fof(f112,definition,(
% 0.13/5.40 sQ0_spl <=> (member(today,lying_days(unicorn)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f113,plain,(
% 0.13/5.40 member(today,lying_days(unicorn))|~sQ0_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f112])).
% 0.13/5.40 fof(f115,definition,(
% 0.13/5.40 sQ1_spl <=> (member(yesterday(today),lying_days(unicorn)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f116,plain,(
% 0.13/5.40 member(yesterday(today),lying_days(unicorn))|~sQ1_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f115])).
% 0.13/5.40 fof(f118,plain,(
% 0.13/5.40 sQ0_spl|sQ1_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f110,f112,f115])).
% 0.13/5.40 fof(f119,definition,(
% 0.13/5.40 sQ2_spl <=> (member(today,lying_days(lion)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f120,plain,(
% 0.13/5.40 member(today,lying_days(lion))|~sQ2_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f119])).
% 0.13/5.40 fof(f122,definition,(
% 0.13/5.40 sQ3_spl <=> (member(yesterday(today),lying_days(lion)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f123,plain,(
% 0.13/5.40 member(yesterday(today),lying_days(lion))|~sQ3_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f122])).
% 0.13/5.40 fof(f125,plain,(
% 0.13/5.40 sQ2_spl|sQ3_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f111,f119,f122])).
% 0.13/5.40 fof(f126,plain,(
% 0.13/5.40 monday(today)|tuesday(today)|wednesday(today)|~sQ2_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f120,f88])).
% 0.13/5.40 fof(f127,definition,(
% 0.13/5.40 sQ4_spl <=> (monday(today))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f128,plain,(
% 0.13/5.40 monday(today)|~sQ4_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f127])).
% 0.13/5.40 fof(f130,definition,(
% 0.13/5.40 sQ5_spl <=> (tuesday(today))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f131,plain,(
% 0.13/5.40 tuesday(today)|~sQ5_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f130])).
% 0.13/5.40 fof(f133,definition,(
% 0.13/5.40 sQ6_spl <=> (wednesday(today))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f134,plain,(
% 0.13/5.40 wednesday(today)|~sQ6_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f133])).
% 0.13/5.40 fof(f136,plain,(
% 0.13/5.40 sQ4_spl|sQ5_spl|sQ6_spl|~sQ2_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f126,f127,f130,f133,f119])).
% 0.13/5.40 fof(f138,plain,(
% 0.13/5.40 tuesday(yesterday(today))|~sQ6_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f134,f82])).
% 0.13/5.40 fof(f140,plain,(
% 0.13/5.40 ~saturday(today)|~sQ6_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f134,f66])).
% 0.13/5.40 fof(f141,plain,(
% 0.13/5.40 ~friday(today)|~sQ6_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f134,f65])).
% 0.13/5.40 fof(f144,plain,(
% 0.13/5.40 thursday(today)|friday(today)|saturday(today)|~sQ0_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f113,f89])).
% 0.13/5.40 fof(f145,definition,(
% 0.13/5.40 sQ7_spl <=> (thursday(today))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f146,plain,(
% 0.13/5.40 thursday(today)|~sQ7_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f145])).
% 0.13/5.40 fof(f148,definition,(
% 0.13/5.40 sQ8_spl <=> (friday(today))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f149,plain,(
% 0.13/5.40 friday(today)|~sQ8_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f148])).
% 0.13/5.40 fof(f151,definition,(
% 0.13/5.40 sQ9_spl <=> (saturday(today))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f152,plain,(
% 0.13/5.40 saturday(today)|~sQ9_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f151])).
% 0.13/5.40 fof(f154,plain,(
% 0.13/5.40 sQ7_spl|sQ8_spl|sQ9_spl|~sQ0_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f144,f145,f148,f151,f112])).
% 0.13/5.40 fof(f155,plain,(
% 0.13/5.40 $false|~sQ6_spl|~sQ9_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f152,f140])).
% 0.13/5.40 fof(f156,plain,(
% 0.13/5.40 ~sQ6_spl|~sQ9_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f155])).
% 0.13/5.40 fof(f157,plain,(
% 0.13/5.40 $false|~sQ7_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f146,f106])).
% 0.13/5.40 fof(f158,plain,(
% 0.13/5.40 ~sQ7_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f157])).
% 0.13/5.40 fof(f163,plain,(
% 0.13/5.40 ~monday(today)|~sQ8_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f149,f56])).
% 0.13/5.40 fof(f166,plain,(
% 0.13/5.40 ~sunday(today)|~sQ5_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f131,f63])).
% 0.13/5.40 fof(f167,plain,(
% 0.13/5.40 ~saturday(today)|~sQ5_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f131,f62])).
% 0.13/5.40 fof(f168,plain,(
% 0.13/5.40 ~friday(today)|~sQ5_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f131,f61])).
% 0.13/5.40 fof(f172,plain,(
% 0.13/5.40 $false|~sQ8_spl|~sQ5_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f168,f149])).
% 0.13/5.40 fof(f173,plain,(
% 0.13/5.40 ~sQ8_spl|~sQ5_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f172])).
% 0.13/5.40 fof(f174,plain,(
% 0.13/5.40 sunday(yesterday(today))|~sQ4_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f128,f87])).
% 0.13/5.40 fof(f178,plain,(
% 0.13/5.40 ~monday(today)|~sQ9_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f152,f57])).
% 0.13/5.40 fof(f179,plain,(
% 0.13/5.40 $false|~sQ4_spl|~sQ9_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f178,f128])).
% 0.13/5.40 fof(f180,plain,(
% 0.13/5.40 ~sQ4_spl|~sQ9_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f179])).
% 0.13/5.40 fof(f181,plain,(
% 0.13/5.40 $false|~sQ4_spl|~sQ8_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f163,f128])).
% 0.13/5.40 fof(f182,plain,(
% 0.13/5.40 ~sQ4_spl|~sQ8_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f181])).
% 0.13/5.40 fof(f183,plain,(
% 0.13/5.40 ~sQ8_spl|~sQ6_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f141,f148,f133])).
% 0.13/5.40 fof(f184,plain,(
% 0.13/5.40 ~sQ9_spl|~sQ5_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f167,f151,f130])).
% 0.13/5.40 fof(f185,plain,(
% 0.13/5.40 monday(yesterday(today))|tuesday(yesterday(today))|wednesday(yesterday(today))|~sQ3_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f123,f88])).
% 0.13/5.40 fof(f186,definition,(
% 0.13/5.40 sQ10_spl <=> (monday(yesterday(today)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f187,plain,(
% 0.13/5.40 monday(yesterday(today))|~sQ10_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f186])).
% 0.13/5.40 fof(f189,definition,(
% 0.13/5.40 sQ11_spl <=> (tuesday(yesterday(today)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f190,plain,(
% 0.13/5.40 tuesday(yesterday(today))|~sQ11_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f189])).
% 0.13/5.40 fof(f192,definition,(
% 0.13/5.40 sQ12_spl <=> (wednesday(yesterday(today)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f193,plain,(
% 0.13/5.40 wednesday(yesterday(today))|~sQ12_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f192])).
% 0.13/5.40 fof(f195,plain,(
% 0.13/5.40 sQ10_spl|sQ11_spl|sQ12_spl|~sQ3_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f185,f186,f189,f192,f122])).
% 0.13/5.40 fof(f196,plain,(
% 0.13/5.40 thursday(yesterday(today))|friday(yesterday(today))|saturday(yesterday(today))|~sQ1_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f116,f89])).
% 0.13/5.40 fof(f197,definition,(
% 0.13/5.40 sQ13_spl <=> (thursday(yesterday(today)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f198,plain,(
% 0.13/5.40 thursday(yesterday(today))|~sQ13_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f197])).
% 0.13/5.40 fof(f200,definition,(
% 0.13/5.40 sQ14_spl <=> (friday(yesterday(today)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f201,plain,(
% 0.13/5.40 friday(yesterday(today))|~sQ14_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f200])).
% 0.13/5.40 fof(f203,definition,(
% 0.13/5.40 sQ15_spl <=> (saturday(yesterday(today)))),
% 0.13/5.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/5.40 fof(f204,plain,(
% 0.13/5.40 saturday(yesterday(today))|~sQ15_spl),
% 0.13/5.40 inference(component_clause,[status(thm)],[f203])).
% 0.13/5.40 fof(f206,plain,(
% 0.13/5.40 sQ13_spl|sQ14_spl|sQ15_spl|~sQ1_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f196,f197,f200,f203,f115])).
% 0.13/5.40 fof(f215,plain,(
% 0.13/5.40 friday(yesterday(today))|~sQ9_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f152,f85])).
% 0.13/5.40 fof(f218,plain,(
% 0.13/5.40 thursday(today)|~sQ12_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f193,f76])).
% 0.13/5.40 fof(f226,plain,(
% 0.13/5.40 sQ7_spl|~sQ12_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f218,f145,f192])).
% 0.13/5.40 fof(f229,plain,(
% 0.13/5.40 saturday(today)|~sQ14_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f201,f78])).
% 0.13/5.40 fof(f234,plain,(
% 0.13/5.40 ~monday(yesterday(today))|~sQ14_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f201,f56])).
% 0.13/5.40 fof(f235,plain,(
% 0.13/5.40 $false|~sQ10_spl|~sQ14_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f234,f187])).
% 0.13/5.40 fof(f236,plain,(
% 0.13/5.40 ~sQ10_spl|~sQ14_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f235])).
% 0.13/5.40 fof(f243,plain,(
% 0.13/5.40 wednesday(today)|~sQ11_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f190,f75])).
% 0.13/5.40 fof(f247,plain,(
% 0.13/5.40 ~saturday(yesterday(today))|~sQ11_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f190,f62])).
% 0.13/5.40 fof(f249,plain,(
% 0.13/5.40 ~thursday(yesterday(today))|~sQ11_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f190,f60])).
% 0.13/5.40 fof(f252,plain,(
% 0.13/5.40 sQ6_spl|~sQ11_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f243,f133,f189])).
% 0.13/5.40 fof(f256,plain,(
% 0.13/5.40 thursday(yesterday(today))|~sQ8_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f149,f84])).
% 0.13/5.40 fof(f261,plain,(
% 0.13/5.40 friday(today)|~sQ13_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f198,f77])).
% 0.13/5.40 fof(f267,plain,(
% 0.13/5.40 ~monday(yesterday(today))|~sQ13_spl),
% 0.13/5.40 inference(resolution,[status(thm)],[f198,f55])).
% 0.13/5.40 fof(f268,plain,(
% 0.13/5.40 ~sQ10_spl|~sQ13_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f267,f186,f197])).
% 0.13/5.40 fof(f269,plain,(
% 0.13/5.40 sQ8_spl|~sQ13_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f261,f148,f197])).
% 0.13/5.40 fof(f270,plain,(
% 0.13/5.40 $false|~sQ13_spl|~sQ11_spl),
% 0.13/5.40 inference(forward_subsumption_resolution,[status(thm)],[f249,f198])).
% 0.13/5.40 fof(f271,plain,(
% 0.13/5.40 ~sQ13_spl|~sQ11_spl),
% 0.13/5.40 inference(contradiction_clause,[status(thm)],[f270])).
% 0.13/5.40 fof(f273,plain,(
% 0.13/5.40 sQ9_spl|~sQ14_spl),
% 0.13/5.40 inference(split_clause,[status(thm)],[f229,f151,f200])).
% 0.13/5.41 fof(f274,plain,(
% 0.13/5.41 sQ13_spl|~sQ8_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f256,f197,f148])).
% 0.13/5.41 fof(f276,plain,(
% 0.13/5.41 sQ14_spl|~sQ9_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f215,f200,f151])).
% 0.13/5.41 fof(f277,plain,(
% 0.13/5.41 sQ11_spl|~sQ6_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f138,f189,f133])).
% 0.13/5.41 fof(f278,plain,(
% 0.13/5.41 $false|~sQ15_spl|~sQ11_spl),
% 0.13/5.41 inference(forward_subsumption_resolution,[status(thm)],[f247,f204])).
% 0.13/5.41 fof(f279,plain,(
% 0.13/5.41 ~sQ15_spl|~sQ11_spl),
% 0.13/5.41 inference(contradiction_clause,[status(thm)],[f278])).
% 0.13/5.41 fof(f286,plain,(
% 0.13/5.41 sunday(today)|~sQ15_spl),
% 0.13/5.41 inference(resolution,[status(thm)],[f204,f79])).
% 0.13/5.41 fof(f289,plain,(
% 0.13/5.41 ~sunday(yesterday(today))|~sQ15_spl),
% 0.13/5.41 inference(resolution,[status(thm)],[f204,f73])).
% 0.13/5.41 fof(f290,plain,(
% 0.13/5.41 ~monday(yesterday(today))|~sQ15_spl),
% 0.13/5.41 inference(resolution,[status(thm)],[f204,f57])).
% 0.13/5.41 fof(f291,plain,(
% 0.13/5.41 $false|~sQ4_spl|~sQ15_spl),
% 0.13/5.41 inference(forward_subsumption_resolution,[status(thm)],[f289,f174])).
% 0.13/5.41 fof(f292,plain,(
% 0.13/5.41 ~sQ4_spl|~sQ15_spl),
% 0.13/5.41 inference(contradiction_clause,[status(thm)],[f291])).
% 0.13/5.41 fof(f293,plain,(
% 0.13/5.41 ~sQ10_spl|~sQ15_spl),
% 0.13/5.41 inference(split_clause,[status(thm)],[f290,f186,f203])).
% 0.13/5.41 fof(f294,plain,(
% 0.13/5.41 $false|~sQ15_spl|~sQ5_spl),
% 0.13/5.41 inference(forward_subsumption_resolution,[status(thm)],[f166,f286])).
% 0.13/5.41 fof(f295,plain,(
% 0.13/5.41 ~sQ15_spl|~sQ5_spl),
% 0.13/5.41 inference(contradiction_clause,[status(thm)],[f294])).
% 0.13/5.41 fof(f296,plain,(
% 0.13/5.41 $false),
% 0.13/5.41 inference(sat_refutation,[status(thm)],[f118,f125,f136,f154,f156,f158,f173,f180,f182,f183,f184,f195,f206,f226,f236,f252,f268,f269,f271,f273,f274,f276,f277,f279,f292,f293,f295])).
% 0.13/5.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.42 % Elapsed time: 0.041651 seconds
% 0.13/5.42 % CPU time: 0.122741 seconds
% 0.13/5.42 % Total memory used: 16.082 MB
% 0.13/5.42 % Net memory used: 16.000 MB
%------------------------------------------------------------------------------