%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ005+1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 : Theorem 0.10s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ005+1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n006.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:44:28 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.41 fof(f4,axiom,(
% 0.10/0.41 thursday(a_thursday) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f10,axiom,(
% 0.10/0.41 (! [X] :( wednesday(X)=> day(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f11,axiom,(
% 0.10/0.41 (! [X] :( thursday(X)=> day(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f18,axiom,(
% 0.10/0.41 (! [X] :( thursday(X)=> wednesday(yesterday(X)) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f24,axiom,(
% 0.10/0.41 (! [X] :( wednesday(X)=> lion_lies(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f25,axiom,(
% 0.10/0.41 (! [X] :( thursday(X)=> ~ lion_lies(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f31,axiom,(
% 0.10/0.41 (! [X] :( wednesday(X)=> ~ unicorn_lies(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f32,axiom,(
% 0.10/0.41 (! [X] :( thursday(X)=> unicorn_lies(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f36,axiom,(
% 0.10/0.41 (! [X] :( lion_lies(X)=> day(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f37,axiom,(
% 0.10/0.41 (! [X] :( unicorn_lies(X)=> day(X) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f40,axiom,(
% 0.10/0.41 (! [X] :( day(X)=> (! [Y] :( day(Y)=> ( ( ~ lion_lies(X)& ~ lies_on_one_of(a_lion,X,Y) )=> ~ lion_lies(Y) ) ) )) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f45,axiom,(
% 0.10/0.41 (! [X] :( day(X)=> (! [Y] :( day(Y)=> ( ( unicorn_lies(X)& ~ lies_on_one_of(a_unicorn,X,Y) )=> unicorn_lies(Y) ) ) )) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f46,conjecture,(
% 0.10/0.41 (? [X] :( day(X)& lies_on_one_of(a_lion,X,yesterday(X))& lies_on_one_of(a_unicorn,X,yesterday(X)) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f47,negated_conjecture,(
% 0.10/0.41 ~((? [X] :( day(X)& lies_on_one_of(a_lion,X,yesterday(X))& lies_on_one_of(a_unicorn,X,yesterday(X)) ) ))),
% 0.10/0.41 inference(negated_conjecture,[status(cth)],[f46])).
% 0.10/0.41 fof(f51,plain,(
% 0.10/0.41 thursday(a_thursday)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.41 fof(f59,plain,(
% 0.10/0.41 ![X]: (~wednesday(X)|day(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.10/0.41 fof(f60,plain,(
% 0.10/0.41 ![X0]: (~wednesday(X0)|day(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.10/0.41 fof(f61,plain,(
% 0.10/0.41 ![X]: (~thursday(X)|day(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.10/0.41 fof(f62,plain,(
% 0.10/0.41 ![X0]: (~thursday(X0)|day(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f61])).
% 0.10/0.41 fof(f75,plain,(
% 0.10/0.41 ![X]: (~thursday(X)|wednesday(yesterday(X)))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.10/0.41 fof(f76,plain,(
% 0.10/0.41 ![X0]: (~thursday(X0)|wednesday(yesterday(X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f75])).
% 0.10/0.41 fof(f87,plain,(
% 0.10/0.41 ![X]: (~wednesday(X)|lion_lies(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.10/0.41 fof(f88,plain,(
% 0.10/0.41 ![X0]: (~wednesday(X0)|lion_lies(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f87])).
% 0.10/0.41 fof(f89,plain,(
% 0.10/0.41 ![X]: (~thursday(X)|~lion_lies(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.10/0.41 fof(f90,plain,(
% 0.10/0.41 ![X0]: (~thursday(X0)|~lion_lies(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f89])).
% 0.10/0.41 fof(f101,plain,(
% 0.10/0.41 ![X]: (~wednesday(X)|~unicorn_lies(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.10/0.41 fof(f102,plain,(
% 0.10/0.41 ![X0]: (~wednesday(X0)|~unicorn_lies(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f101])).
% 0.10/0.41 fof(f103,plain,(
% 0.10/0.41 ![X]: (~thursday(X)|unicorn_lies(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.10/0.41 fof(f104,plain,(
% 0.10/0.41 ![X0]: (~thursday(X0)|unicorn_lies(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f103])).
% 0.10/0.41 fof(f111,plain,(
% 0.10/0.41 ![X]: (~lion_lies(X)|day(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.10/0.41 fof(f112,plain,(
% 0.10/0.41 ![X0]: (~lion_lies(X0)|day(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f111])).
% 0.10/0.41 fof(f113,plain,(
% 0.10/0.41 ![X]: (~unicorn_lies(X)|day(X))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.10/0.41 fof(f114,plain,(
% 0.10/0.41 ![X0]: (~unicorn_lies(X0)|day(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f113])).
% 0.10/0.41 fof(f119,plain,(
% 0.10/0.41 ![X]: (~day(X)|(![Y]: (~day(Y)|((lion_lies(X)|lies_on_one_of(a_lion,X,Y))|~lion_lies(Y)))))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.10/0.41 fof(f120,plain,(
% 0.10/0.41 ![X0,X1]: (~day(X0)|~day(X1)|lion_lies(X0)|lies_on_one_of(a_lion,X0,X1)|~lion_lies(X1))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f119])).
% 0.10/0.41 fof(f129,plain,(
% 0.10/0.41 ![X]: (~day(X)|(![Y]: (~day(Y)|((~unicorn_lies(X)|lies_on_one_of(a_unicorn,X,Y))|unicorn_lies(Y)))))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.10/0.41 fof(f130,plain,(
% 0.10/0.41 ![X0,X1]: (~day(X0)|~day(X1)|~unicorn_lies(X0)|lies_on_one_of(a_unicorn,X0,X1)|unicorn_lies(X1))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f129])).
% 0.10/0.41 fof(f131,plain,(
% 0.10/0.41 (![X]: ((~day(X)|~lies_on_one_of(a_lion,X,yesterday(X)))|~lies_on_one_of(a_unicorn,X,yesterday(X))))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.10/0.41 fof(f132,plain,(
% 0.10/0.41 ![X0]: (~day(X0)|~lies_on_one_of(a_lion,X0,yesterday(X0))|~lies_on_one_of(a_unicorn,X0,yesterday(X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f131])).
% 0.10/0.41 fof(f134,plain,(
% 0.10/0.41 ![X0,X1]: (~day(X0)|lion_lies(X0)|lies_on_one_of(a_lion,X0,X1)|~lion_lies(X1))),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f120,f112])).
% 0.10/0.41 fof(f138,plain,(
% 0.10/0.41 ![X0,X1]: (~day(X0)|~unicorn_lies(X1)|lies_on_one_of(a_unicorn,X1,X0)|unicorn_lies(X0))),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f130,f114])).
% 0.10/0.41 fof(f142,plain,(
% 0.10/0.41 ![X0]: (~thursday(X0)|~lies_on_one_of(a_lion,X0,yesterday(X0))|~lies_on_one_of(a_unicorn,X0,yesterday(X0)))),
% 0.10/0.41 inference(resolution,[status(thm)],[f62,f132])).
% 0.10/0.41 fof(f195,plain,(
% 0.10/0.41 ~lion_lies(a_thursday)),
% 0.10/0.41 inference(resolution,[status(thm)],[f90,f51])).
% 0.10/0.41 fof(f237,plain,(
% 0.10/0.41 ![X0,X1]: (~day(X0)|lion_lies(X0)|lies_on_one_of(a_lion,X0,X1)|~wednesday(X1))),
% 0.10/0.41 inference(resolution,[status(thm)],[f134,f88])).
% 0.10/0.41 fof(f253,plain,(
% 0.10/0.41 ![X0,X1]: (~day(X0)|lion_lies(X0)|lies_on_one_of(a_lion,X0,yesterday(X1))|~thursday(X1))),
% 0.10/0.41 inference(resolution,[status(thm)],[f237,f76])).
% 0.10/0.41 fof(f372,plain,(
% 0.10/0.41 unicorn_lies(a_thursday)),
% 0.10/0.41 inference(resolution,[status(thm)],[f104,f51])).
% 0.10/0.41 fof(f450,definition,(
% 0.10/0.41 sQ21_spl <=> (day(yesterday(a_thursday)))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f452,plain,(
% 0.10/0.41 ~day(yesterday(a_thursday))|sQ21_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f450])).
% 0.10/0.41 fof(f467,plain,(
% 0.10/0.41 ![X0]: (~day(X0)|lion_lies(X0)|lies_on_one_of(a_lion,X0,yesterday(a_thursday)))),
% 0.10/0.41 inference(resolution,[status(thm)],[f253,f51])).
% 0.10/0.41 fof(f590,plain,(
% 0.10/0.41 ~wednesday(yesterday(a_thursday))|sQ21_spl),
% 0.10/0.41 inference(resolution,[status(thm)],[f452,f60])).
% 0.10/0.41 fof(f652,plain,(
% 0.10/0.41 ~thursday(a_thursday)|sQ21_spl),
% 0.10/0.41 inference(resolution,[status(thm)],[f590,f76])).
% 0.10/0.41 fof(f653,plain,(
% 0.10/0.41 $false|sQ21_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f652,f51])).
% 0.10/0.41 fof(f654,plain,(
% 0.10/0.41 sQ21_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f653])).
% 0.10/0.41 fof(f692,plain,(
% 0.10/0.41 ![X0]: (~day(X0)|lies_on_one_of(a_unicorn,a_thursday,X0)|unicorn_lies(X0))),
% 0.10/0.41 inference(resolution,[status(thm)],[f372,f138])).
% 0.10/0.41 fof(f698,definition,(
% 0.10/0.41 sQ47_spl <=> (day(a_thursday))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f700,plain,(
% 0.10/0.41 ~day(a_thursday)|sQ47_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f698])).
% 0.10/0.41 fof(f736,plain,(
% 0.10/0.41 ~thursday(a_thursday)|sQ47_spl),
% 0.10/0.41 inference(resolution,[status(thm)],[f700,f62])).
% 0.10/0.41 fof(f739,plain,(
% 0.10/0.41 $false|sQ47_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f736,f51])).
% 0.10/0.41 fof(f740,plain,(
% 0.10/0.41 sQ47_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f739])).
% 0.10/0.41 fof(f745,plain,(
% 0.10/0.41 ~day(yesterday(a_thursday))|unicorn_lies(yesterday(a_thursday))|~thursday(a_thursday)|~lies_on_one_of(a_lion,a_thursday,yesterday(a_thursday))),
% 0.10/0.41 inference(resolution,[status(thm)],[f692,f142])).
% 0.10/0.41 fof(f749,definition,(
% 0.10/0.41 sQ54_spl <=> (unicorn_lies(yesterday(a_thursday)))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f750,plain,(
% 0.10/0.41 unicorn_lies(yesterday(a_thursday))|~sQ54_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f749])).
% 0.10/0.41 fof(f755,definition,(
% 0.10/0.41 sQ56_spl <=> (lies_on_one_of(a_lion,a_thursday,yesterday(a_thursday)))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f757,plain,(
% 0.10/0.41 ~lies_on_one_of(a_lion,a_thursday,yesterday(a_thursday))|sQ56_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f755])).
% 0.10/0.41 fof(f759,definition,(
% 0.10/0.41 sQ57_spl <=> (thursday(a_thursday))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f761,plain,(
% 0.10/0.41 ~thursday(a_thursday)|sQ57_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f759])).
% 0.10/0.41 fof(f762,plain,(
% 0.10/0.41 ~sQ21_spl|sQ54_spl|~sQ57_spl|~sQ56_spl),
% 0.10/0.41 inference(split_clause,[status(thm)],[f745,f450,f749,f759,f755])).
% 0.10/0.41 fof(f780,plain,(
% 0.10/0.41 $false|sQ57_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f761,f51])).
% 0.10/0.41 fof(f781,plain,(
% 0.10/0.41 sQ57_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f780])).
% 0.10/0.41 fof(f783,plain,(
% 0.10/0.41 ~wednesday(yesterday(a_thursday))|~sQ54_spl),
% 0.10/0.41 inference(resolution,[status(thm)],[f750,f102])).
% 0.10/0.41 fof(f785,plain,(
% 0.10/0.41 ~thursday(a_thursday)|~sQ54_spl),
% 0.10/0.41 inference(resolution,[status(thm)],[f783,f76])).
% 0.10/0.41 fof(f786,plain,(
% 0.10/0.41 ~sQ57_spl|~sQ54_spl),
% 0.10/0.41 inference(split_clause,[status(thm)],[f785,f759,f749])).
% 0.10/0.41 fof(f787,plain,(
% 0.10/0.41 ~day(a_thursday)|lion_lies(a_thursday)|sQ56_spl),
% 0.10/0.41 inference(resolution,[status(thm)],[f757,f467])).
% 0.10/0.41 fof(f788,definition,(
% 0.10/0.41 sQ62_spl <=> (lion_lies(a_thursday))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f789,plain,(
% 0.10/0.41 lion_lies(a_thursday)|~sQ62_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f788])).
% 0.10/0.41 fof(f791,plain,(
% 0.10/0.41 ~sQ47_spl|sQ62_spl|sQ56_spl),
% 0.10/0.41 inference(split_clause,[status(thm)],[f787,f698,f788,f755])).
% 0.10/0.41 fof(f792,plain,(
% 0.10/0.41 $false|~sQ62_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f789,f195])).
% 0.10/0.41 fof(f793,plain,(
% 0.10/0.41 ~sQ62_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f792])).
% 0.10/0.41 fof(f794,plain,(
% 0.10/0.41 $false),
% 0.10/0.41 inference(sat_refutation,[status(thm)],[f654,f740,f762,f781,f786,f791,f793])).
% 0.10/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.43 % Elapsed time: 0.050459 seconds
% 0.10/0.43 % CPU time: 0.169508 seconds
% 0.10/0.43 % Total memory used: 13.248 MB
% 0.10/0.43 % Net memory used: 13.172 MB
%------------------------------------------------------------------------------