%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM602+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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 01:41:09 PM UTC 2026
% Result : Theorem 0.18s 0.57s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 4
% Syntax : Number of formulae : 23 ( 4 unt; 1 def)
% Number of atoms : 81 ( 25 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 87 ( 29 ~; 26 |; 30 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 30 ( 21 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f97,hypothesis,
! [W0] :
( ( aElementOf0(W0,xO)
| ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
=> ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,W1) = szDzizrdt0(xd)
& aElementOf0(W1,szNzAzT0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
( aElementOf0(xx,xO)
& ? [W0] :
( sdtlpdtrp0(xe,W0) = xx
& aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,conjecture,
? [W0] :
( sdtlpdtrp0(xe,W0) = xx
& aElementOf0(W0,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,negated_conjecture,
~ ? [W0] :
( sdtlpdtrp0(xe,W0) = xx
& aElementOf0(W0,szNzAzT0) ),
inference(negated_conjecture,[status(cth)],[f99]) ).
fof(f577,plain,
! [W0] :
( ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,W1) = szDzizrdt0(xd)
& aElementOf0(W1,szNzAzT0) )
| ( ~ aElementOf0(W0,xO)
& ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f578,definition,
! [W0] :
( sP9_prd(W0)
<=> ( ~ aElementOf0(W0,xO)
& ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f579,plain,
! [W0] :
( ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,W1) = szDzizrdt0(xd)
& aElementOf0(W1,szNzAzT0) )
| sP9_prd(W0) ),
inference(formula_renaming,[status(thm)],[f577,f578]) ).
fof(f580,plain,
! [W0] :
( ( sdtlpdtrp0(xe,sK35_skl(W0)) = W0
& aElementOf0(sK35_skl(W0),sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,sK35_skl(W0)) = szDzizrdt0(xd)
& aElementOf0(sK35_skl(W0),szNzAzT0) )
| sP9_prd(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl]),skolemize(W1,sK35_skl(W0))],[f579]) ).
fof(f581,plain,
! [X0] :
( aElementOf0(sK35_skl(X0),szNzAzT0)
| sP9_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f580]) ).
fof(f584,plain,
! [X0] :
( sdtlpdtrp0(xe,sK35_skl(X0)) = X0
| sP9_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f580]) ).
fof(f585,plain,
( aElementOf0(xx,xO)
& sdtlpdtrp0(xe,sK36_skl) = xx
& aElementOf0(sK36_skl,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(W0,sK36_skl)],[f98]) ).
fof(f588,plain,
aElementOf0(xx,xO),
inference(cnf_transformation,[status(thm)],[f585]) ).
fof(f589,plain,
! [W0] :
( sdtlpdtrp0(xe,W0) != xx
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f590,plain,
! [X0] :
( sdtlpdtrp0(xe,X0) != xx
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f589]) ).
fof(f712,plain,
! [W0] :
( ( aElementOf0(W0,xO)
| ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| sP9_prd(W0) )
& ( ( ~ aElementOf0(W0,xO)
& ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
| ~ sP9_prd(W0) ) ),
inference(NNF_transformation,[status(thm)],[f578]) ).
fof(f713,plain,
( ! [W0] :
( aElementOf0(W0,xO)
| ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| sP9_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,xO)
& ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
| ~ sP9_prd(W0) ) ),
inference(miniscoping,[status(thm)],[f712]) ).
fof(f714,plain,
( ! [W0] :
( aElementOf0(W0,xO)
| ( sdtlpdtrp0(xe,sK59_skl(W0)) = W0
& aElementOf0(sK59_skl(W0),sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| sP9_prd(W0) )
& ! [W0] :
( ( ~ aElementOf0(W0,xO)
& ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
| ~ sP9_prd(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59_skl]),skolemize(W1,sK59_skl(W0))],[f713]) ).
fof(f716,plain,
! [X0] :
( ~ aElementOf0(X0,xO)
| ~ sP9_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f714]) ).
fof(f1092,plain,
~ sP9_prd(xx),
inference(resolution,[status(thm)],[f716,f588]) ).
fof(f1637,plain,
! [X0] :
( sP9_prd(X0)
| X0 != xx
| ~ aElementOf0(sK35_skl(X0),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f584,f590]) ).
fof(f1645,plain,
( sP9_prd(xx)
| ~ aElementOf0(sK35_skl(xx),szNzAzT0) ),
inference(destructive_equality_resolution,[status(thm)],[f1637]) ).
fof(f1646,plain,
sP9_prd(xx),
inference(forward_subsumption_resolution,[status(thm)],[f1645,f581]) ).
fof(f1647,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1646,f1092]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM602+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n001.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 02:49:28 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.51 % Drodi V4.1.1
% 0.18/0.57 % Refutation found
% 0.18/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.27/0.63 % Elapsed time: 0.176439 seconds
% 0.27/0.63 % CPU time: 0.439193 seconds
% 0.27/0.63 % Total memory used: 72.738 MB
% 0.27/0.63 % Net memory used: 72.347 MB
%------------------------------------------------------------------------------