%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ023-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:16 PM UTC 2026
% Result : Unsatisfiable 0.19s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PUZ023-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n016.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 03:50:52 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 0.19/0.47 % Refutation found
% 0.19/0.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.19/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.47 fof(f1,axiom,(
% 0.19/0.47 (![X]: (( a_truth(truthteller(X))| a_truth(liar(X)) ) ))),
% 0.19/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.47 fof(f18,hypothesis,(
% 0.19/0.47 ( ~ a_truth(liar(b))| ~ a_truth(liar(c))| an_answer(b_and_c_liars) ) ),
% 0.19/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.47 fof(f19,hypothesis,(
% 0.19/0.47 ( ~ a_truth(liar(b))| ~ a_truth(truthteller(c))| an_answer(b_liar_and_c_truthteller) ) ),
% 0.19/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.47 fof(f20,hypothesis,(
% 0.19/0.47 ( ~ a_truth(truthteller(b))| ~ a_truth(liar(c))| an_answer(b_truthteller_and_c_liar) ) ),
% 0.19/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.47 fof(f21,hypothesis,(
% 0.19/0.47 ( ~ a_truth(truthteller(b))| ~ a_truth(truthteller(c))| an_answer(b_and_c_truthtellers) ) ),
% 0.19/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.47 fof(f22,negated_conjecture,(
% 0.19/0.47 (![X]: (~ an_answer(X) ))),
% 0.19/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.47 fof(f23,plain,(
% 0.19/0.47 ![X0]: (a_truth(truthteller(X0))|a_truth(liar(X0)))),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f1])).
% 0.19/0.47 fof(f51,plain,(
% 0.19/0.47 ~a_truth(liar(b))|~a_truth(liar(c))|an_answer(b_and_c_liars)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f18])).
% 0.19/0.47 fof(f52,plain,(
% 0.19/0.47 ~a_truth(liar(b))|~a_truth(truthteller(c))|an_answer(b_liar_and_c_truthteller)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f19])).
% 0.19/0.47 fof(f53,plain,(
% 0.19/0.47 ~a_truth(truthteller(b))|~a_truth(liar(c))|an_answer(b_truthteller_and_c_liar)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f20])).
% 0.19/0.47 fof(f54,plain,(
% 0.19/0.47 ~a_truth(truthteller(b))|~a_truth(truthteller(c))|an_answer(b_and_c_truthtellers)),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f21])).
% 0.19/0.47 fof(f55,plain,(
% 0.19/0.47 ![X0]: (~an_answer(X0))),
% 0.19/0.47 inference(cnf_transformation,[status(thm)],[f22])).
% 0.19/0.47 fof(f87,definition,(
% 0.19/0.47 sQ8_spl <=> (a_truth(liar(b)))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f89,plain,(
% 0.19/0.47 ~a_truth(liar(b))|sQ8_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f87])).
% 0.19/0.47 fof(f90,definition,(
% 0.19/0.47 sQ9_spl <=> (a_truth(liar(c)))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f92,plain,(
% 0.19/0.47 ~a_truth(liar(c))|sQ9_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f90])).
% 0.19/0.47 fof(f93,definition,(
% 0.19/0.47 sQ10_spl <=> (an_answer(b_and_c_liars))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f94,plain,(
% 0.19/0.47 an_answer(b_and_c_liars)|~sQ10_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f93])).
% 0.19/0.47 fof(f96,plain,(
% 0.19/0.47 ~sQ8_spl|~sQ9_spl|sQ10_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f51,f87,f90,f93])).
% 0.19/0.47 fof(f97,definition,(
% 0.19/0.47 sQ11_spl <=> (a_truth(truthteller(c)))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f99,plain,(
% 0.19/0.47 ~a_truth(truthteller(c))|sQ11_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f97])).
% 0.19/0.47 fof(f100,definition,(
% 0.19/0.47 sQ12_spl <=> (an_answer(b_liar_and_c_truthteller))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f101,plain,(
% 0.19/0.47 an_answer(b_liar_and_c_truthteller)|~sQ12_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f100])).
% 0.19/0.47 fof(f103,plain,(
% 0.19/0.47 ~sQ8_spl|~sQ11_spl|sQ12_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f52,f87,f97,f100])).
% 0.19/0.47 fof(f104,definition,(
% 0.19/0.47 sQ13_spl <=> (a_truth(truthteller(b)))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f106,plain,(
% 0.19/0.47 ~a_truth(truthteller(b))|sQ13_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f104])).
% 0.19/0.47 fof(f107,definition,(
% 0.19/0.47 sQ14_spl <=> (an_answer(b_truthteller_and_c_liar))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f108,plain,(
% 0.19/0.47 an_answer(b_truthteller_and_c_liar)|~sQ14_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f107])).
% 0.19/0.47 fof(f110,plain,(
% 0.19/0.47 ~sQ13_spl|~sQ9_spl|sQ14_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f53,f104,f90,f107])).
% 0.19/0.47 fof(f111,definition,(
% 0.19/0.47 sQ15_spl <=> (an_answer(b_and_c_truthtellers))),
% 0.19/0.47 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.19/0.47 fof(f112,plain,(
% 0.19/0.47 an_answer(b_and_c_truthtellers)|~sQ15_spl),
% 0.19/0.47 inference(component_clause,[status(thm)],[f111])).
% 0.19/0.47 fof(f114,plain,(
% 0.19/0.47 ~sQ13_spl|~sQ11_spl|sQ15_spl),
% 0.19/0.47 inference(split_clause,[status(thm)],[f54,f104,f97,f111])).
% 0.19/0.47 fof(f115,plain,(
% 0.19/0.47 a_truth(truthteller(c))|sQ9_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f92,f23])).
% 0.19/0.47 fof(f116,plain,(
% 0.19/0.47 $false|sQ11_spl|sQ9_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f115,f99])).
% 0.19/0.47 fof(f117,plain,(
% 0.19/0.47 sQ11_spl|sQ9_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f116])).
% 0.19/0.47 fof(f118,plain,(
% 0.19/0.47 a_truth(truthteller(b))|sQ8_spl),
% 0.19/0.47 inference(resolution,[status(thm)],[f89,f23])).
% 0.19/0.47 fof(f119,plain,(
% 0.19/0.47 $false|sQ13_spl|sQ8_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f118,f106])).
% 0.19/0.47 fof(f120,plain,(
% 0.19/0.47 sQ13_spl|sQ8_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f119])).
% 0.19/0.47 fof(f121,plain,(
% 0.19/0.47 $false|~sQ15_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f112,f55])).
% 0.19/0.47 fof(f122,plain,(
% 0.19/0.47 ~sQ15_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f121])).
% 0.19/0.47 fof(f123,plain,(
% 0.19/0.47 $false|~sQ12_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f101,f55])).
% 0.19/0.47 fof(f124,plain,(
% 0.19/0.47 ~sQ12_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f123])).
% 0.19/0.47 fof(f125,plain,(
% 0.19/0.47 $false|~sQ10_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f94,f55])).
% 0.19/0.47 fof(f126,plain,(
% 0.19/0.47 ~sQ10_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f125])).
% 0.19/0.47 fof(f127,plain,(
% 0.19/0.47 $false|~sQ14_spl),
% 0.19/0.47 inference(forward_subsumption_resolution,[status(thm)],[f108,f55])).
% 0.19/0.47 fof(f128,plain,(
% 0.19/0.47 ~sQ14_spl),
% 0.19/0.47 inference(contradiction_clause,[status(thm)],[f127])).
% 0.19/0.47 fof(f129,plain,(
% 0.19/0.47 $false),
% 0.19/0.47 inference(sat_refutation,[status(thm)],[f96,f103,f110,f114,f117,f120,f122,f124,f126,f128])).
% 0.19/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.53 % Elapsed time: 0.072488 seconds
% 0.19/0.53 % CPU time: 0.061047 seconds
% 0.19/0.53 % Total memory used: 1.085 MB
% 0.19/0.53 % Net memory used: 1.074 MB
%------------------------------------------------------------------------------