%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEV644+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:07 PM UTC 2026
% Result : Theorem 162.24s 162.52s
% Output : CNFRefutation 162.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 2
% Syntax : Number of formulae : 11 ( 3 unt; 1 def)
% Number of atoms : 28 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 25 ( 8 ~; 6 |; 5 &)
% ( 3 <=>; 2 =>; 0 <=; 1 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 2 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 4 ( 2 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2364,conjecture,
! [V0__P] :
( cProp___24t(V0__P)
=> ( p(V0__P)
<=> p(V0__P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2365,negated_conjecture,
~ ! [V0__P] :
( cProp___24t(V0__P)
=> ( p(V0__P)
<=> p(V0__P) ) ),
inference(negated_conjecture,[status(cth)],[f2364]) ).
fof(f10940,plain,
? [V0__P] :
( ( p(V0__P)
<~> p(V0__P) )
& cProp___24t(V0__P) ),
inference(pre_NNF_transformation,[status(thm)],[f2365]) ).
fof(f10941,plain,
? [V0__P] :
( ( ~ p(V0__P)
| ~ p(V0__P) )
& ( p(V0__P)
| p(V0__P) )
& cProp___24t(V0__P) ),
inference(NNF_transformation,[status(thm)],[f10940]) ).
fof(f10942,plain,
( ( ~ p(sK894_skl)
| ~ p(sK894_skl) )
& ( p(sK894_skl)
| p(sK894_skl) )
& cProp___24t(sK894_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK894_skl]),skolemize(V0__P,sK894_skl)],[f10941]) ).
fof(f10944,plain,
( p(sK894_skl)
| p(sK894_skl) ),
inference(cnf_transformation,[status(thm)],[f10942]) ).
fof(f10945,plain,
( ~ p(sK894_skl)
| ~ p(sK894_skl) ),
inference(cnf_transformation,[status(thm)],[f10942]) ).
fof(f16138,definition,
( sQ52_spl
<=> p(sK894_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f16141,plain,
sQ52_spl,
inference(split_clause,[status(thm)],[f10944,f16138]) ).
fof(f16142,plain,
~ sQ52_spl,
inference(split_clause,[status(thm)],[f10945,f16138]) ).
fof(f16666,plain,
$false,
inference(sat_refutation,[status(thm)],[f16141,f16142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV644+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n014.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 07:31:35 UTC 2026
% 0.10/0.37 % CPUTime :
% 162.15/162.45 % Drodi V4.1.1
% 162.24/162.52 % Refutation found
% 162.24/162.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 162.24/162.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 162.35/162.72 % Elapsed time: 162.325568 seconds
% 162.35/162.72 % CPU time: 162.469082 seconds
% 162.35/162.72 % Total memory used: 1.040 GB
% 162.35/162.72 % Net memory used: 1.039 GB
%------------------------------------------------------------------------------