%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV644+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:33:49 PM UTC 2026
% Result : Theorem 71.42s 81.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV644+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/10.38 % Computer : n003.cluster.edu
% 0.11/10.38 % Model : x86_64 x86_64
% 0.11/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.38 % Memory : 8046.5625MB
% 0.11/10.38 % OS : Linux 6.8.0-71-generic
% 0.11/10.38 % CPULimit : 300
% 0.11/10.38 % WCLimit : 300
% 0.11/10.38 % DateTime : Mon Sep 21 07:33:26 UTC 2026
% 0.11/10.38 % CPUTime :
% 71.32/81.66 % Drodi V4.1.1
% 71.42/81.79 % Refutation found
% 71.42/81.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 71.42/81.79 % SZS output start CNFRefutation for theBenchmark
% 71.42/81.79 fof(f2364,conjecture,(
% 71.42/81.79 (! [V0__P] :( cProp___24t(V0__P)=> ( p(V0__P)<=> p(V0__P) ) ) )),
% 71.42/81.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.42/81.79 fof(f2365,negated_conjecture,(
% 71.42/81.79 ~((! [V0__P] :( cProp___24t(V0__P)=> ( p(V0__P)<=> p(V0__P) ) ) ))),
% 71.42/81.79 inference(negated_conjecture,[status(cth)],[f2364])).
% 71.42/81.79 fof(f10940,plain,(
% 71.42/81.79 (?[V0__P]: (cProp___24t(V0__P)&(p(V0__P)<~>p(V0__P))))),
% 71.42/81.79 inference(pre_NNF_transformation,[status(thm)],[f2365])).
% 71.42/81.79 fof(f10941,plain,(
% 71.42/81.79 ?[V0__P]: (cProp___24t(V0__P)&((p(V0__P)|p(V0__P))&(~p(V0__P)|~p(V0__P))))),
% 71.42/81.79 inference(NNF_transformation,[status(thm)],[f10940])).
% 71.42/81.79 fof(f10942,plain,(
% 71.42/81.79 (cProp___24t(sK894_skl)&((p(sK894_skl)|p(sK894_skl))&(~p(sK894_skl)|~p(sK894_skl))))),
% 71.42/81.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK894_skl]),skolemize(V0__P,sK894_skl)],[f10941])).
% 71.42/81.79 fof(f10944,plain,(
% 71.42/81.79 p(sK894_skl)|p(sK894_skl)),
% 71.42/81.79 inference(cnf_transformation,[status(thm)],[f10942])).
% 71.42/81.79 fof(f10945,plain,(
% 71.42/81.79 ~p(sK894_skl)|~p(sK894_skl)),
% 71.42/81.79 inference(cnf_transformation,[status(thm)],[f10942])).
% 71.42/81.79 fof(f16138,definition,(
% 71.42/81.79 sQ52_spl <=> (p(sK894_skl))),
% 71.42/81.79 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 71.42/81.79 fof(f16141,plain,(
% 71.42/81.79 sQ52_spl),
% 71.42/81.79 inference(split_clause,[status(thm)],[f10944,f16138])).
% 71.42/81.79 fof(f16142,plain,(
% 71.42/81.79 ~sQ52_spl),
% 71.42/81.79 inference(split_clause,[status(thm)],[f10945,f16138])).
% 71.42/81.79 fof(f16666,plain,(
% 71.42/81.79 $false),
% 71.42/81.79 inference(sat_refutation,[status(thm)],[f16141,f16142])).
% 71.42/81.79 % SZS output end CNFRefutation for theBenchmark.p
% 71.46/81.95 % Elapsed time: 71.540957 seconds
% 71.46/81.95 % CPU time: 71.880700 seconds
% 71.46/81.95 % Total memory used: 2.600 GB
% 71.46/81.95 % Net memory used: 2.598 GB
%------------------------------------------------------------------------------