%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM621+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 : n002.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:13 PM UTC 2026
% Result : Theorem 12.54s 2.03s
% Output : CNFRefutation 12.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 14
% Syntax : Number of formulae : 70 ( 22 unt; 1 def)
% Number of atoms : 251 ( 41 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 262 ( 81 ~; 75 |; 87 &)
% ( 4 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 14 con; 0-2 aty)
% Number of variables : 75 ( 69 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,hypothesis,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(sdtlpdtrp0(xe,W0),W1) )
& aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0)) ) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,hypothesis,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( aElementOf0(W0,xO)
<=> ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& ! [W0] :
( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,hypothesis,
( aSubsetOf0(xO,xS)
& ! [W0] :
( aElementOf0(W0,xO)
=> aElementOf0(W0,xS) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,hypothesis,
( aElementOf0(xQ,slbdtsldtrb0(xO,xK))
& sbrdtbr0(xQ) = xK
& aSubsetOf0(xQ,xO)
& ! [W0] :
( aElementOf0(W0,xQ)
=> aElementOf0(W0,xO) )
& aSet0(xQ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
( xp = szmzizndt0(xQ)
& ! [W0] :
( aElementOf0(W0,xQ)
=> sdtlseqdt0(xp,W0) )
& aElementOf0(xp,xQ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)
& aElementOf0(xn,szDzozmdt0(xd)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,hypothesis,
( aElementOf0(xx,xP)
& xx != szmzizndt0(xQ)
& aElementOf0(xx,xQ)
& aElement0(xx) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,hypothesis,
( ? [W0] :
( sdtlpdtrp0(xe,W0) = xx
& aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aElementOf0(xx,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,hypothesis,
! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xm))
=> sdtlseqdt0(xx,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,conjecture,
( ( aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ) )
=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,negated_conjecture,
~ ( ( aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ) )
=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
inference(negated_conjecture,[status(cth)],[f118]) ).
fof(f144,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f145,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f144]) ).
fof(f146,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f147,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f146]) ).
fof(f149,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f196,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f224,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f225,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f379,plain,
( isCountable0(xS)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f380,plain,
aSet0(xS),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f382,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f551,plain,
( ! [W0] :
( ( sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0))
& ! [W1] :
( sdtlseqdt0(sdtlpdtrp0(xe,W0),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f554,plain,
! [X0] :
( aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f551]) ).
fof(f582,plain,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| aElementOf0(W0,xO) )
& ( ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| ~ aElementOf0(W0,xO) ) )
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
inference(NNF_transformation,[status(thm)],[f95]) ).
fof(f583,plain,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| aElementOf0(W0,xO) )
& ! [W0] :
( ? [W1] :
( sdtlpdtrp0(xe,W1) = W0
& aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| ~ aElementOf0(W0,xO) )
& ! [W0] :
( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
inference(miniscoping,[status(thm)],[f582]) ).
fof(f584,plain,
( xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [W0] :
( ! [W1] :
( sdtlpdtrp0(xe,W1) != W0
| ~ aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| aElementOf0(W0,xO) )
& ! [W0] :
( ( sdtlpdtrp0(xe,sK34_skl(W0)) = W0
& aElementOf0(sK34_skl(W0),sdtlbdtrb0(xd,szDzizrdt0(xd))) )
| ~ aElementOf0(W0,xO) )
& ! [W0] :
( sdtlpdtrp0(xd,W0) != szDzizrdt0(xd)
| ~ aElementOf0(W0,szDzozmdt0(xd))
| aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& ! [W0] :
( ( sdtlpdtrp0(xd,W0) = szDzizrdt0(xd)
& aElementOf0(W0,szDzozmdt0(xd)) )
| ~ aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aSet0(xO) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W1,sK34_skl(W0))],[f583]) ).
fof(f585,plain,
aSet0(xO),
inference(cnf_transformation,[status(thm)],[f584]) ).
fof(f604,plain,
( aSubsetOf0(xO,xS)
& ! [W0] :
( aElementOf0(W0,xS)
| ~ aElementOf0(W0,xO) ) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f606,plain,
aSubsetOf0(xO,xS),
inference(cnf_transformation,[status(thm)],[f604]) ).
fof(f607,plain,
( aElementOf0(xQ,slbdtsldtrb0(xO,xK))
& sbrdtbr0(xQ) = xK
& aSubsetOf0(xQ,xO)
& ! [W0] :
( aElementOf0(W0,xO)
| ~ aElementOf0(W0,xQ) )
& aSet0(xQ) ),
inference(pre_NNF_transformation,[status(thm)],[f99]) ).
fof(f610,plain,
aSubsetOf0(xQ,xO),
inference(cnf_transformation,[status(thm)],[f607]) ).
fof(f627,plain,
( xp = szmzizndt0(xQ)
& ! [W0] :
( sdtlseqdt0(xp,W0)
| ~ aElementOf0(W0,xQ) )
& aElementOf0(xp,xQ) ),
inference(pre_NNF_transformation,[status(thm)],[f103]) ).
fof(f628,plain,
aElementOf0(xp,xQ),
inference(cnf_transformation,[status(thm)],[f627]) ).
fof(f629,plain,
! [X0] :
( sdtlseqdt0(xp,X0)
| ~ aElementOf0(X0,xQ) ),
inference(cnf_transformation,[status(thm)],[f627]) ).
fof(f630,plain,
xp = szmzizndt0(xQ),
inference(cnf_transformation,[status(thm)],[f627]) ).
fof(f656,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f657,plain,
sdtlpdtrp0(xe,xn) = xp,
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f660,plain,
aElementOf0(xx,xQ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f661,plain,
xx != szmzizndt0(xQ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f663,plain,
( sdtlpdtrp0(xe,sK38_skl) = xx
& aElementOf0(sK38_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& aElementOf0(xx,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(W0,sK38_skl)],[f114]) ).
fof(f664,plain,
aElementOf0(xx,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f663]) ).
fof(f669,plain,
! [W0] :
( sdtlseqdt0(xx,W0)
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xm)) ),
inference(pre_NNF_transformation,[status(thm)],[f116]) ).
fof(f670,plain,
! [X0] :
( sdtlseqdt0(xx,X0)
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xm)) ),
inference(cnf_transformation,[status(thm)],[f669]) ).
fof(f676,plain,
( ~ aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
& ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f119]) ).
fof(f677,plain,
! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xn)) ),
inference(cnf_transformation,[status(thm)],[f676]) ).
fof(f982,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f382,f149]) ).
fof(f986,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) ),
inference(forward_subsumption_resolution,[status(thm)],[f982,f196]) ).
fof(f1081,plain,
! [X0] :
( aElementOf0(X0,xS)
| ~ aElementOf0(X0,xO)
| ~ aSet0(xS) ),
inference(resolution,[status(thm)],[f606,f149]) ).
fof(f1085,plain,
! [X0] :
( aElementOf0(X0,xS)
| ~ aElementOf0(X0,xO) ),
inference(forward_subsumption_resolution,[status(thm)],[f1081,f380]) ).
fof(f1088,plain,
! [X0] :
( aElementOf0(X0,xO)
| ~ aElementOf0(X0,xQ)
| ~ aSet0(xO) ),
inference(resolution,[status(thm)],[f610,f149]) ).
fof(f1092,plain,
! [X0] :
( aElementOf0(X0,xO)
| ~ aElementOf0(X0,xQ) ),
inference(forward_subsumption_resolution,[status(thm)],[f1088,f585]) ).
fof(f1111,plain,
xx != xp,
inference(backward_demodulation,[status(thm)],[f630,f661]) ).
fof(f1146,plain,
aElementOf0(xp,xO),
inference(resolution,[status(thm)],[f1092,f628]) ).
fof(f1153,plain,
aElementOf0(xp,xS),
inference(resolution,[status(thm)],[f1146,f1085]) ).
fof(f1159,plain,
aElementOf0(xp,szNzAzT0),
inference(resolution,[status(thm)],[f1153,f986]) ).
fof(f1684,plain,
sdtlseqdt0(xp,xx),
inference(resolution,[status(thm)],[f629,f660]) ).
fof(f1864,plain,
! [X0] :
( X0 = xx
| ~ sdtlseqdt0(xx,X0)
| ~ sdtlseqdt0(X0,xx)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f225,f664]) ).
fof(f3283,plain,
( xp = xx
| ~ sdtlseqdt0(xx,xp)
| ~ aElementOf0(xp,szNzAzT0) ),
inference(resolution,[status(thm)],[f1864,f1684]) ).
fof(f3298,plain,
( xp = xx
| ~ sdtlseqdt0(xx,xp) ),
inference(forward_subsumption_resolution,[status(thm)],[f3283,f1159]) ).
fof(f3305,plain,
~ sdtlseqdt0(xx,xp),
inference(forward_subsumption_resolution,[status(thm)],[f3298,f1111]) ).
fof(f8289,plain,
( aElementOf0(sdtlpdtrp0(xe,xn),sdtlpdtrp0(xN,xm))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f554,f677]) ).
fof(f8307,plain,
( aElementOf0(xp,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f657,f8289]) ).
fof(f8308,plain,
aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(forward_subsumption_resolution,[status(thm)],[f8307,f656]) ).
fof(f8316,plain,
sdtlseqdt0(xx,xp),
inference(resolution,[status(thm)],[f8308,f670]) ).
fof(f8319,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8316,f3305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM621+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:47:48 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 12.54/2.03 % Refutation found
% 12.54/2.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.54/2.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.54/2.06 % Elapsed time: 1.683208 seconds
% 12.54/2.06 % CPU time: 12.911457 seconds
% 12.54/2.06 % Total memory used: 234.458 MB
% 12.54/2.06 % Net memory used: 223.884 MB
%------------------------------------------------------------------------------