%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG106+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:04:59 PM UTC 2026
% Result : Theorem 0.14s 0.47s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 49
% Syntax : Number of formulae : 187 ( 13 unt; 43 def)
% Number of atoms : 871 ( 86 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 1131 ( 447 ~; 506 |; 113 &)
% ( 51 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 40 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 3 con; 0-3 aty)
% Number of variables : 291 ( 267 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aElement0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
aElement0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| W0 = sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,definition,
! [W0,W1] :
( ( aSet0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtasasdt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) ) )
& aSet0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,definition,
! [W0] :
( aIdeal0(W0)
<=> ( ! [W1] :
( aElementOf0(W1,W0)
=> ( ! [W2] :
( aElement0(W2)
=> aElementOf0(sdtasdt0(W2,W1),W0) )
& ! [W2] :
( aElementOf0(W2,W0)
=> aElementOf0(sdtpldt0(W1,W2),W0) ) ) )
& aSet0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,definition,
! [W0,W1,W2] :
( ( aIdeal0(W2)
& aElement0(W1)
& aElement0(W0) )
=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
<=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,definition,
! [W0] :
( aElement0(W0)
=> ! [W1] :
( W1 = slsdtgt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) ) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
aElement0(xc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,conjecture,
( ! [W0,W1,W2] :
( ( aElement0(W2)
& aElementOf0(W1,slsdtgt0(xc))
& aElementOf0(W0,slsdtgt0(xc)) )
=> ? [W3] :
( ? [W4] :
( aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))
& aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))
& sdtasdt0(W2,W0) = sdtasdt0(xc,sdtasdt0(W3,W2))
& sdtpldt0(W0,W1) = sdtasdt0(xc,sdtpldt0(W3,W4))
& sdtasdt0(xc,W4) = W1
& aElement0(W4) )
& sdtasdt0(xc,W3) = W0
& aElement0(W3) ) )
=> aIdeal0(slsdtgt0(xc)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
~ ( ! [W0,W1,W2] :
( ( aElement0(W2)
& aElementOf0(W1,slsdtgt0(xc))
& aElementOf0(W0,slsdtgt0(xc)) )
=> ? [W3] :
( ? [W4] :
( aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))
& aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))
& sdtasdt0(W2,W0) = sdtasdt0(xc,sdtasdt0(W3,W2))
& sdtpldt0(W0,W1) = sdtasdt0(xc,sdtpldt0(W3,W4))
& sdtasdt0(xc,W4) = W1
& aElement0(W4) )
& sdtasdt0(xc,W3) = W0
& aElement0(W3) ) )
=> aIdeal0(slsdtgt0(xc)) ),
inference(negated_conjecture,[status(cth)],[f39]) ).
fof(f44,plain,
aElement0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
aElement0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f78,plain,
! [W0,W1] :
( W1 = sz00
| W0 = sz00
| sdtasdt0(W0,W1) != sz00
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f79,plain,
! [X0,X1] :
( X1 = sz00
| X0 = sz00
| sdtasdt0(X0,X1) != sz00
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f84,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f85,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f103,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtasasdt0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) ) )
& aSet0(W2) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f104,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( ~ aElementOf0(W3,W1)
| ~ aElementOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtasasdt0(W0,W1) )
& ( ( ! [W3] :
( ( ~ aElementOf0(W3,W1)
| ~ aElementOf0(W3,W0)
| aElementOf0(W3,W2) )
& ( ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtasasdt0(W0,W1) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) )
| aElementOf0(W3,W2) )
& ( ~ aElementOf0(W3,W1)
| ~ aElementOf0(W3,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtasasdt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ aElementOf0(W3,W1)
| ~ aElementOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtasasdt0(W0,W1) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f104]) ).
fof(f106,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( ( aElementOf0(sK7_skl(W2,W1,W0),W1)
& aElementOf0(sK7_skl(W2,W1,W0),W0) )
| aElementOf0(sK7_skl(W2,W1,W0),W2) )
& ( ~ aElementOf0(sK7_skl(W2,W1,W0),W1)
| ~ aElementOf0(sK7_skl(W2,W1,W0),W0)
| ~ aElementOf0(sK7_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtasasdt0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ~ aElementOf0(W3,W1)
| ~ aElementOf0(W3,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ( aElementOf0(W3,W1)
& aElementOf0(W3,W0) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtasasdt0(W0,W1) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(W3,sK7_skl(W2,W1,W0))],[f105]) ).
fof(f112,plain,
! [X0,X1,X2] :
( aElementOf0(sK7_skl(X2,X1,X0),X0)
| aElementOf0(sK7_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f113,plain,
! [X0,X1,X2] :
( aElementOf0(sK7_skl(X2,X1,X0),X1)
| aElementOf0(sK7_skl(X2,X1,X0),X2)
| ~ aSet0(X2)
| X2 = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f114,plain,
! [W0] :
( aIdeal0(W0)
<=> ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f115,plain,
! [W0] :
( ( ? [W1] :
( ( ? [W2] :
( ~ aElementOf0(sdtasdt0(W2,W1),W0)
& aElement0(W2) )
| ? [W2] :
( ~ aElementOf0(sdtpldt0(W1,W2),W0)
& aElementOf0(W2,W0) ) )
& aElementOf0(W1,W0) )
| ~ aSet0(W0)
| aIdeal0(W0) )
& ( ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aIdeal0(W0) ) ),
inference(NNF_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
( ! [W0] :
( ? [W1] :
( ( ? [W2] :
( ~ aElementOf0(sdtasdt0(W2,W1),W0)
& aElement0(W2) )
| ? [W2] :
( ~ aElementOf0(sdtpldt0(W1,W2),W0)
& aElementOf0(W2,W0) ) )
& aElementOf0(W1,W0) )
| ~ aSet0(W0)
| aIdeal0(W0) )
& ! [W0] :
( ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aIdeal0(W0) ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f117,plain,
( ! [W0] :
( ( ( ( ~ aElementOf0(sdtasdt0(sK10_skl(W0),sK8_skl(W0)),W0)
& aElement0(sK10_skl(W0)) )
| ( ~ aElementOf0(sdtpldt0(sK8_skl(W0),sK9_skl(W0)),W0)
& aElementOf0(sK9_skl(W0),W0) ) )
& aElementOf0(sK8_skl(W0),W0) )
| ~ aSet0(W0)
| aIdeal0(W0) )
& ! [W0] :
( ( ! [W1] :
( ( ! [W2] :
( aElementOf0(sdtasdt0(W2,W1),W0)
| ~ aElement0(W2) )
& ! [W2] :
( aElementOf0(sdtpldt0(W1,W2),W0)
| ~ aElementOf0(W2,W0) ) )
| ~ aElementOf0(W1,W0) )
& aSet0(W0) )
| ~ aIdeal0(W0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl]),skolemize(W1,sK8_skl(W0)),skolemize(W2,sK9_skl(W0)),skolemize(W2,sK10_skl(W0))],[f116]) ).
fof(f119,plain,
! [X0,X1,X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0)
| ~ aElementOf0(X1,X0)
| ~ aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f120,plain,
! [X0,X1,X2] :
( aElementOf0(sdtasdt0(X2,X1),X0)
| ~ aElement0(X2)
| ~ aElementOf0(X1,X0)
| ~ aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f121,plain,
! [X0] :
( aElementOf0(sK8_skl(X0),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f122,plain,
! [X0] :
( aElement0(sK10_skl(X0))
| aElementOf0(sK9_skl(X0),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f123,plain,
! [X0] :
( ~ aElementOf0(sdtasdt0(sK10_skl(X0),sK8_skl(X0)),X0)
| aElementOf0(sK9_skl(X0),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f124,plain,
! [X0] :
( aElement0(sK10_skl(X0))
| ~ aElementOf0(sdtpldt0(sK8_skl(X0),sK9_skl(X0)),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f125,plain,
! [X0] :
( ~ aElementOf0(sdtasdt0(sK10_skl(X0),sK8_skl(X0)),X0)
| ~ aElementOf0(sdtpldt0(sK8_skl(X0),sK9_skl(X0)),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f130,plain,
! [W0,W1,W2] :
( ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
<=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) )
| ~ aIdeal0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f131,plain,
! [W0,W1,W2] :
( ( ( ~ aElementOf0(sdtpldt0(W0,smndt0(W1)),W2)
| sdteqdtlpzmzozddtrp0(W0,W1,W2) )
& ( aElementOf0(sdtpldt0(W0,smndt0(W1)),W2)
| ~ sdteqdtlpzmzozddtrp0(W0,W1,W2) ) )
| ~ aIdeal0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(NNF_transformation,[status(thm)],[f130]) ).
fof(f132,plain,
! [X0,X1,X2] :
( aElementOf0(sdtpldt0(X0,smndt0(X1)),X2)
| ~ sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aIdeal0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f180,plain,
! [W0] :
( ! [W1] :
( W1 = slsdtgt0(W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
<=> ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) ) )
& aSet0(W1) ) )
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f181,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| aElementOf0(W2,W1) )
& ( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slsdtgt0(W0) )
& ( ( ! [W2] :
( ( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| aElementOf0(W2,W1) )
& ( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| ~ aElementOf0(W2,W1) ) )
& aSet0(W1) )
| W1 != slsdtgt0(W0) ) )
| ~ aElement0(W0) ),
inference(NNF_transformation,[status(thm)],[f180]) ).
fof(f182,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| aElementOf0(W2,W1) )
& ( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| ~ aElementOf0(W2,W1) ) )
| ~ aSet0(W1)
| W1 = slsdtgt0(W0) )
& ! [W1] :
( ( ! [W2] :
( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| aElementOf0(W2,W1) )
& ! [W2] :
( ? [W3] :
( sdtasdt0(W0,W3) = W2
& aElement0(W3) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slsdtgt0(W0) ) )
| ~ aElement0(W0) ),
inference(miniscoping,[status(thm)],[f181]) ).
fof(f183,plain,
! [W0] :
( ( ! [W1] :
( ( ( ( sdtasdt0(W0,sK19_skl(W1,W0)) = sK18_skl(W1,W0)
& aElement0(sK19_skl(W1,W0)) )
| aElementOf0(sK18_skl(W1,W0),W1) )
& ( ! [W3] :
( sdtasdt0(W0,W3) != sK18_skl(W1,W0)
| ~ aElement0(W3) )
| ~ aElementOf0(sK18_skl(W1,W0),W1) ) )
| ~ aSet0(W1)
| W1 = slsdtgt0(W0) )
& ! [W1] :
( ( ! [W2] :
( ! [W3] :
( sdtasdt0(W0,W3) != W2
| ~ aElement0(W3) )
| aElementOf0(W2,W1) )
& ! [W2] :
( ( sdtasdt0(W0,sK17_skl(W2,W1,W0)) = W2
& aElement0(sK17_skl(W2,W1,W0)) )
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| W1 != slsdtgt0(W0) ) )
| ~ aElement0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(W3,sK17_skl(W2,W1,W0)),skolemize(W2,sK18_skl(W1,W0)),skolemize(W3,sK19_skl(W1,W0))],[f182]) ).
fof(f184,plain,
! [X0,X1] :
( aSet0(X1)
| X1 != slsdtgt0(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f187,plain,
! [X0,X1,X2,X3] :
( sdtasdt0(X0,X3) != X2
| ~ aElement0(X3)
| aElementOf0(X2,X1)
| X1 != slsdtgt0(X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f191,plain,
aElement0(xc),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f192,plain,
( ~ aIdeal0(slsdtgt0(xc))
& ! [W0,W1,W2] :
( ? [W3] :
( ? [W4] :
( aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))
& aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))
& sdtasdt0(W2,W0) = sdtasdt0(xc,sdtasdt0(W3,W2))
& sdtpldt0(W0,W1) = sdtasdt0(xc,sdtpldt0(W3,W4))
& sdtasdt0(xc,W4) = W1
& aElement0(W4) )
& sdtasdt0(xc,W3) = W0
& aElement0(W3) )
| ~ aElement0(W2)
| ~ aElementOf0(W1,slsdtgt0(xc))
| ~ aElementOf0(W0,slsdtgt0(xc)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f193,plain,
( ~ aIdeal0(slsdtgt0(xc))
& ! [W0,W1,W2] :
( ? [W3] :
( aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))
& aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))
& sdtasdt0(W2,W0) = sdtasdt0(xc,sdtasdt0(W3,W2))
& ? [W4] :
( sdtpldt0(W0,W1) = sdtasdt0(xc,sdtpldt0(W3,W4))
& sdtasdt0(xc,W4) = W1
& aElement0(W4) )
& sdtasdt0(xc,W3) = W0
& aElement0(W3) )
| ~ aElement0(W2)
| ~ aElementOf0(W1,slsdtgt0(xc))
| ~ aElementOf0(W0,slsdtgt0(xc)) ) ),
inference(miniscoping,[status(thm)],[f192]) ).
fof(f194,plain,
( ~ aIdeal0(slsdtgt0(xc))
& ! [W0,W1,W2] :
( ( aElementOf0(sdtasdt0(W2,W0),slsdtgt0(xc))
& aElementOf0(sdtpldt0(W0,W1),slsdtgt0(xc))
& sdtasdt0(W2,W0) = sdtasdt0(xc,sdtasdt0(sK20_skl(W2,W1,W0),W2))
& sdtpldt0(W0,W1) = sdtasdt0(xc,sdtpldt0(sK20_skl(W2,W1,W0),sK21_skl(W2,W1,W0)))
& sdtasdt0(xc,sK21_skl(W2,W1,W0)) = W1
& aElement0(sK21_skl(W2,W1,W0))
& sdtasdt0(xc,sK20_skl(W2,W1,W0)) = W0
& aElement0(sK20_skl(W2,W1,W0)) )
| ~ aElement0(W2)
| ~ aElementOf0(W1,slsdtgt0(xc))
| ~ aElementOf0(W0,slsdtgt0(xc)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl]),skolemize(W3,sK20_skl(W2,W1,W0)),skolemize(W4,sK21_skl(W2,W1,W0))],[f193]) ).
fof(f196,plain,
! [X0,X1,X2] :
( sdtasdt0(xc,sK20_skl(X2,X1,X0)) = X0
| ~ aElement0(X2)
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f198,plain,
! [X0,X1,X2] :
( sdtasdt0(xc,sK21_skl(X2,X1,X0)) = X1
| ~ aElement0(X2)
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f201,plain,
! [X0,X1,X2] :
( aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc))
| ~ aElement0(X2)
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f202,plain,
! [X0,X1,X2] :
( aElementOf0(sdtasdt0(X2,X0),slsdtgt0(xc))
| ~ aElement0(X2)
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f203,plain,
~ aIdeal0(slsdtgt0(xc)),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f221,definition,
! [X0,X1] :
( sQ0_spl
<=> ( aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc))
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc)) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f222,plain,
! [X0,X1] :
( ~ sQ0_spl
| aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc))
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f221]) ).
fof(f224,definition,
! [X2] :
( sQ1_spl
<=> ~ aElement0(X2) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f225,plain,
! [X0] :
( ~ sQ1_spl
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f224]) ).
fof(f227,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f201,f221,f224]) ).
fof(f228,definition,
! [X0,X2] :
( sQ2_spl
<=> ( aElementOf0(sdtasdt0(X2,X0),slsdtgt0(xc))
| ~ aElement0(X2)
| ~ aElementOf0(X0,slsdtgt0(xc)) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f229,plain,
! [X0,X1] :
( ~ sQ2_spl
| aElementOf0(sdtasdt0(X1,X0),slsdtgt0(xc))
| ~ aElement0(X1)
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f228]) ).
fof(f231,definition,
! [X1] :
( sQ3_spl
<=> ~ aElementOf0(X1,slsdtgt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f232,plain,
! [X0] :
( ~ sQ3_spl
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f231]) ).
fof(f234,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f202,f228,f231]) ).
fof(f243,plain,
! [X0] :
( aSet0(slsdtgt0(X0))
| ~ aElement0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f184]) ).
fof(f246,plain,
! [X0,X1] :
( ~ aElement0(X1)
| aElementOf0(sdtasdt0(X0,X1),slsdtgt0(X0))
| ~ aElement0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f187]) ).
fof(f248,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,X1))
| ~ aSet0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f85,f222]) ).
fof(f250,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ aElement0(X0)
| ~ aElementOf0(X1,slsdtgt0(xc))
| aElement0(sdtasdt0(X0,X1))
| ~ aSet0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f85,f229]) ).
fof(f253,definition,
( sQ4_spl
<=> aSet0(slsdtgt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f255,plain,
( sQ4_spl
| ~ aSet0(slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f253]) ).
fof(f256,definition,
! [X0,X1] :
( sQ5_spl
<=> ( ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f257,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,X1)) ),
inference(component_clause,[status(thm)],[f256]) ).
fof(f259,plain,
( ~ sQ0_spl
| sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f248,f253,f256,f221]) ).
fof(f261,definition,
! [X0,X1] :
( sQ6_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,slsdtgt0(xc))
| aElement0(sdtasdt0(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f262,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ aElement0(X0)
| ~ aElementOf0(X1,slsdtgt0(xc))
| aElement0(sdtasdt0(X0,X1)) ),
inference(component_clause,[status(thm)],[f261]) ).
fof(f264,plain,
( ~ sQ2_spl
| sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f250,f253,f261,f228]) ).
fof(f267,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f45,f225]) ).
fof(f270,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f267]) ).
fof(f272,definition,
( sQ7_spl
<=> aIdeal0(slsdtgt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f273,plain,
( ~ sQ7_spl
| aIdeal0(slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f276,plain,
( sQ4_spl
| ~ aElement0(xc) ),
inference(resolution,[status(thm)],[f243,f255]) ).
fof(f277,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f276,f191]) ).
fof(f278,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f277]) ).
fof(f283,definition,
( sQ9_spl
<=> aElement0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f285,plain,
( sQ9_spl
| ~ aElement0(sz00) ),
inference(component_clause,[status(thm)],[f283]) ).
fof(f305,plain,
! [X0] :
( ~ sQ3_spl
| ~ aElement0(X0)
| ~ aElement0(xc) ),
inference(resolution,[status(thm)],[f246,f232]) ).
fof(f306,definition,
( sQ13_spl
<=> aElement0(xc) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( sQ13_spl
| ~ aElement0(xc) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f309,plain,
( ~ sQ3_spl
| sQ1_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f305,f306,f224,f231]) ).
fof(f310,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f191]) ).
fof(f311,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f310]) ).
fof(f312,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ aElement0(X1)
| ~ aElement0(xc)
| ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sdtasdt0(xc,X1))) ),
inference(resolution,[status(thm)],[f262,f246]) ).
fof(f314,definition,
! [X0,X1] :
( sQ14_spl
<=> ( ~ aElement0(X1)
| ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sdtasdt0(xc,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f317,plain,
( ~ sQ6_spl
| ~ sQ13_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f312,f314,f306,f261]) ).
fof(f346,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ aElement0(X1)
| ~ aElement0(xc)
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sdtasdt0(xc,X1))) ),
inference(resolution,[status(thm)],[f257,f246]) ).
fof(f349,definition,
! [X0,X1] :
( sQ17_spl
<=> ( ~ aElement0(X1)
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sdtasdt0(xc,X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f352,plain,
( ~ sQ5_spl
| ~ sQ13_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f346,f349,f306,f256]) ).
fof(f361,plain,
! [X0,X1] :
( sK20_skl(X1,X0,sz00) = sz00
| xc = sz00
| ~ aElement0(sK20_skl(X1,X0,sz00))
| ~ aElement0(xc)
| ~ aElement0(X1)
| ~ aElementOf0(X0,slsdtgt0(xc))
| ~ aElementOf0(sz00,slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f196,f79]) ).
fof(f362,definition,
( sQ20_spl
<=> aElementOf0(sz00,slsdtgt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f365,definition,
! [X0,X1] :
( sQ21_spl
<=> ( sK20_skl(X1,X0,sz00) = sz00
| ~ aElement0(sK20_skl(X1,X0,sz00))
| ~ aElement0(X1)
| ~ aElementOf0(X0,slsdtgt0(xc)) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f368,definition,
( sQ22_spl
<=> xc = sz00 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f369,plain,
( ~ sQ22_spl
| xc = sz00 ),
inference(component_clause,[status(thm)],[f368]) ).
fof(f371,plain,
( sQ22_spl
| ~ sQ13_spl
| sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f361,f362,f365,f306,f368]) ).
fof(f372,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f285,f44]) ).
fof(f373,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f372]) ).
fof(f386,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ sQ22_spl
| aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc))
| ~ aElementOf0(X1,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(forward_demodulation,[status(thm)],[f369,f222]) ).
fof(f387,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ sQ22_spl
| aElementOf0(sdtpldt0(X0,X1),slsdtgt0(xc))
| ~ aElementOf0(X1,slsdtgt0(sz00))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(forward_demodulation,[status(thm)],[f369,f386]) ).
fof(f388,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ sQ22_spl
| aElementOf0(sdtpldt0(X0,X1),slsdtgt0(sz00))
| ~ aElementOf0(X1,slsdtgt0(sz00))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(forward_demodulation,[status(thm)],[f369,f387]) ).
fof(f389,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ sQ22_spl
| aElement0(sdtpldt0(X0,X1))
| ~ aSet0(slsdtgt0(sz00))
| ~ aElementOf0(X1,slsdtgt0(sz00))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f388,f85]) ).
fof(f390,definition,
! [X0,X1] :
( sQ23_spl
<=> ( aElement0(sdtpldt0(X0,X1))
| ~ aElementOf0(X1,slsdtgt0(sz00))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f391,plain,
! [X0,X1] :
( ~ sQ23_spl
| aElement0(sdtpldt0(X0,X1))
| ~ aElementOf0(X1,slsdtgt0(sz00))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,definition,
( sQ24_spl
<=> aSet0(slsdtgt0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f395,plain,
( sQ24_spl
| ~ aSet0(slsdtgt0(sz00)) ),
inference(component_clause,[status(thm)],[f393]) ).
fof(f396,plain,
( ~ sQ0_spl
| ~ sQ22_spl
| ~ sQ24_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f389,f390,f393,f368,f221]) ).
fof(f397,plain,
( sQ24_spl
| ~ aElement0(sz00) ),
inference(resolution,[status(thm)],[f395,f243]) ).
fof(f398,plain,
( sQ24_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f397,f283,f393]) ).
fof(f412,plain,
! [X0,X1] :
( sK21_skl(X1,sz00,X0) = sz00
| xc = sz00
| ~ aElement0(sK21_skl(X1,sz00,X0))
| ~ aElement0(xc)
| ~ aElement0(X1)
| ~ aElementOf0(sz00,slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f198,f79]) ).
fof(f413,definition,
! [X0,X1] :
( sQ25_spl
<=> ( sK21_skl(X1,sz00,X0) = sz00
| ~ aElement0(sK21_skl(X1,sz00,X0))
| ~ aElement0(X1)
| ~ aElementOf0(X0,slsdtgt0(xc)) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f416,plain,
( sQ22_spl
| ~ sQ13_spl
| ~ sQ20_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f412,f413,f362,f306,f368]) ).
fof(f417,plain,
! [X0] :
( ~ sQ6_spl
| ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sK8_skl(slsdtgt0(xc))))
| ~ aSet0(slsdtgt0(xc))
| aIdeal0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f121,f262]) ).
fof(f421,definition,
! [X0] :
( sQ26_spl
<=> ( ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sK8_skl(slsdtgt0(xc)))) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( ~ sQ6_spl
| sQ26_spl
| ~ sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f417,f272,f253,f421,f261]) ).
fof(f435,plain,
! [X0,X1,X2] :
( ~ sQ6_spl
| ~ aElement0(X2)
| aElement0(sdtasdt0(X2,sK7_skl(slsdtgt0(xc),X1,X0)))
| aElementOf0(sK7_skl(slsdtgt0(xc),X1,X0),X0)
| ~ aSet0(slsdtgt0(xc))
| slsdtgt0(xc) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f112,f262]) ).
fof(f439,definition,
! [X0,X1,X2] :
( sQ27_spl
<=> ( ~ aElement0(X2)
| aElement0(sdtasdt0(X2,sK7_skl(slsdtgt0(xc),X1,X0)))
| aElementOf0(sK7_skl(slsdtgt0(xc),X1,X0),X0)
| slsdtgt0(xc) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f435,f439,f253,f261]) ).
fof(f448,plain,
! [X0,X1,X2] :
( ~ sQ6_spl
| ~ aElement0(X2)
| aElement0(sdtasdt0(X2,sK7_skl(slsdtgt0(xc),X1,X0)))
| aElementOf0(sK7_skl(slsdtgt0(xc),X1,X0),X1)
| ~ aSet0(slsdtgt0(xc))
| slsdtgt0(xc) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f113,f262]) ).
fof(f452,definition,
! [X0,X1,X2] :
( sQ28_spl
<=> ( ~ aElement0(X2)
| aElement0(sdtasdt0(X2,sK7_skl(slsdtgt0(xc),X1,X0)))
| aElementOf0(sK7_skl(slsdtgt0(xc),X1,X0),X1)
| slsdtgt0(xc) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f448,f452,f253,f261]) ).
fof(f460,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| aElementOf0(sK7_skl(slsdtgt0(sz00),X1,X2),X1)
| ~ aSet0(slsdtgt0(sz00))
| slsdtgt0(sz00) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(sz00),X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f391,f113]) ).
fof(f461,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| aElementOf0(sK7_skl(slsdtgt0(sz00),X1,X2),X2)
| ~ aSet0(slsdtgt0(sz00))
| slsdtgt0(sz00) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(sz00),X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f391,f112]) ).
fof(f462,plain,
! [X0] :
( ~ sQ23_spl
| ~ aSet0(slsdtgt0(sz00))
| aIdeal0(slsdtgt0(sz00))
| aElement0(sdtpldt0(X0,sK8_skl(slsdtgt0(sz00))))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f391,f121]) ).
fof(f463,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ aElement0(X1)
| ~ aElement0(sz00)
| aElement0(sdtpldt0(X0,sdtasdt0(sz00,X1)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f391,f246]) ).
fof(f464,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| ~ aElement0(X1)
| ~ aElementOf0(X2,slsdtgt0(sz00))
| ~ aIdeal0(slsdtgt0(sz00))
| aElement0(sdtpldt0(X0,sdtasdt0(X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f391,f120]) ).
fof(f465,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| ~ aElementOf0(X2,slsdtgt0(sz00))
| ~ aElementOf0(X1,slsdtgt0(sz00))
| ~ aIdeal0(slsdtgt0(sz00))
| aElement0(sdtpldt0(X0,sdtpldt0(X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f391,f119]) ).
fof(f466,definition,
! [X0,X1,X2] :
( sQ29_spl
<=> ( aElementOf0(sK7_skl(slsdtgt0(sz00),X1,X2),X1)
| slsdtgt0(sz00) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(sz00),X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ23_spl
| ~ sQ24_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f460,f466,f393,f390]) ).
fof(f470,definition,
! [X0,X1,X2] :
( sQ30_spl
<=> ( aElementOf0(sK7_skl(slsdtgt0(sz00),X1,X2),X2)
| slsdtgt0(sz00) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(sz00),X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( ~ sQ23_spl
| ~ sQ24_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f461,f470,f393,f390]) ).
fof(f474,definition,
! [X0] :
( sQ31_spl
<=> ( aElement0(sdtpldt0(X0,sK8_skl(slsdtgt0(sz00))))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f477,definition,
( sQ32_spl
<=> aIdeal0(slsdtgt0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f480,plain,
( ~ sQ23_spl
| ~ sQ24_spl
| sQ32_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f462,f474,f477,f393,f390]) ).
fof(f481,definition,
! [X0,X1] :
( sQ33_spl
<=> ( ~ aElement0(X1)
| aElement0(sdtpldt0(X0,sdtasdt0(sz00,X1)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( ~ sQ23_spl
| ~ sQ9_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f463,f481,f283,f390]) ).
fof(f485,definition,
! [X0,X1,X2] :
( sQ34_spl
<=> ( ~ aElement0(X1)
| ~ aElementOf0(X2,slsdtgt0(sz00))
| aElement0(sdtpldt0(X0,sdtasdt0(X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( ~ sQ23_spl
| ~ sQ32_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f464,f485,f477,f390]) ).
fof(f489,definition,
! [X0,X1,X2] :
( sQ35_spl
<=> ( ~ aElementOf0(X2,slsdtgt0(sz00))
| ~ aElementOf0(X1,slsdtgt0(sz00))
| aElement0(sdtpldt0(X0,sdtpldt0(X1,X2)))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( ~ sQ23_spl
| ~ sQ32_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f465,f489,f477,f390]) ).
fof(f493,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| aElementOf0(sK7_skl(slsdtgt0(xc),X1,X2),X1)
| ~ aSet0(slsdtgt0(xc))
| slsdtgt0(xc) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(xc),X1,X2))) ),
inference(resolution,[status(thm)],[f257,f113]) ).
fof(f494,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| aElementOf0(sK7_skl(slsdtgt0(xc),X1,X2),X2)
| ~ aSet0(slsdtgt0(xc))
| slsdtgt0(xc) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(xc),X1,X2))) ),
inference(resolution,[status(thm)],[f257,f112]) ).
fof(f495,plain,
! [X0] :
( ~ sQ5_spl
| ~ aSet0(slsdtgt0(xc))
| aIdeal0(slsdtgt0(xc))
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sK8_skl(slsdtgt0(xc)))) ),
inference(resolution,[status(thm)],[f257,f121]) ).
fof(f499,definition,
! [X0,X1,X2] :
( sQ36_spl
<=> ( aElementOf0(sK7_skl(slsdtgt0(xc),X1,X2),X1)
| slsdtgt0(xc) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(xc),X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f493,f499,f253,f256]) ).
fof(f503,definition,
! [X0,X1,X2] :
( sQ37_spl
<=> ( aElementOf0(sK7_skl(slsdtgt0(xc),X1,X2),X2)
| slsdtgt0(xc) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sK7_skl(slsdtgt0(xc),X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f506,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f494,f503,f253,f256]) ).
fof(f507,definition,
! [X0] :
( sQ38_spl
<=> ( ~ aElementOf0(X0,slsdtgt0(xc))
| aElement0(sdtpldt0(X0,sK8_skl(slsdtgt0(xc)))) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| sQ7_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f495,f507,f272,f253,f256]) ).
fof(f520,plain,
! [X0] :
( ~ sQ23_spl
| aElement0(sdtpldt0(X0,sK9_skl(slsdtgt0(sz00))))
| ~ aElementOf0(X0,slsdtgt0(sz00))
| aElement0(sK10_skl(slsdtgt0(sz00)))
| ~ aSet0(slsdtgt0(sz00))
| aIdeal0(slsdtgt0(sz00)) ),
inference(resolution,[status(thm)],[f122,f391]) ).
fof(f526,definition,
( sQ39_spl
<=> aElement0(sK10_skl(slsdtgt0(sz00))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f529,definition,
! [X0] :
( sQ40_spl
<=> ( aElement0(sdtpldt0(X0,sK9_skl(slsdtgt0(sz00))))
| ~ aElementOf0(X0,slsdtgt0(sz00)) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f532,plain,
( ~ sQ23_spl
| sQ40_spl
| sQ39_spl
| ~ sQ24_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f520,f477,f393,f526,f529,f390]) ).
fof(f533,definition,
( sQ41_spl
<=> aElement0(sK10_skl(slsdtgt0(xc))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( ~ sQ0_spl
| ~ aElementOf0(sK9_skl(slsdtgt0(xc)),slsdtgt0(xc))
| ~ aElementOf0(sK8_skl(slsdtgt0(xc)),slsdtgt0(xc))
| aElement0(sK10_skl(slsdtgt0(xc)))
| ~ aSet0(slsdtgt0(xc))
| aIdeal0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f124,f222]) ).
fof(f553,definition,
( sQ44_spl
<=> aElementOf0(sK8_skl(slsdtgt0(xc)),slsdtgt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ44_spl
| aElementOf0(sK8_skl(slsdtgt0(xc)),slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f555,plain,
( sQ44_spl
| ~ aElementOf0(sK8_skl(slsdtgt0(xc)),slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,definition,
( sQ45_spl
<=> aElementOf0(sK9_skl(slsdtgt0(xc)),slsdtgt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f558,plain,
( sQ45_spl
| ~ aElementOf0(sK9_skl(slsdtgt0(xc)),slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f556]) ).
fof(f559,plain,
( ~ sQ0_spl
| ~ sQ45_spl
| ~ sQ44_spl
| sQ41_spl
| ~ sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f550,f272,f253,f533,f553,f556,f221]) ).
fof(f561,plain,
( sQ45_spl
| aElement0(sK10_skl(slsdtgt0(xc)))
| ~ aSet0(slsdtgt0(xc))
| aIdeal0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f558,f122]) ).
fof(f562,plain,
( sQ45_spl
| sQ41_spl
| ~ sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f561,f272,f253,f533,f556]) ).
fof(f565,plain,
( sQ44_spl
| ~ aSet0(slsdtgt0(xc))
| aIdeal0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f555,f121]) ).
fof(f566,plain,
( sQ44_spl
| ~ sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f565,f272,f253,f553]) ).
fof(f569,plain,
( ~ sQ44_spl
| aElement0(sK8_skl(slsdtgt0(xc)))
| ~ aSet0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f554,f85]) ).
fof(f570,definition,
( sQ46_spl
<=> aElement0(sK8_skl(slsdtgt0(xc))) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( ~ sQ44_spl
| sQ46_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f569,f253,f570,f553]) ).
fof(f574,plain,
( ~ sQ2_spl
| aElementOf0(sK9_skl(slsdtgt0(xc)),slsdtgt0(xc))
| ~ aSet0(slsdtgt0(xc))
| aIdeal0(slsdtgt0(xc))
| ~ aElement0(sK10_skl(slsdtgt0(xc)))
| ~ aElementOf0(sK8_skl(slsdtgt0(xc)),slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f229,f123]) ).
fof(f578,plain,
( ~ sQ2_spl
| sQ45_spl
| ~ sQ4_spl
| sQ7_spl
| ~ sQ41_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f574,f553,f533,f272,f253,f556,f228]) ).
fof(f599,plain,
( ~ sQ2_spl
| ~ aElement0(sK10_skl(slsdtgt0(xc)))
| ~ aElementOf0(sK8_skl(slsdtgt0(xc)),slsdtgt0(xc))
| ~ aElementOf0(sdtpldt0(sK8_skl(slsdtgt0(xc)),sK9_skl(slsdtgt0(xc))),slsdtgt0(xc))
| ~ aSet0(slsdtgt0(xc))
| aIdeal0(slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f125,f229]) ).
fof(f602,definition,
( sQ48_spl
<=> aElementOf0(sdtpldt0(sK8_skl(slsdtgt0(xc)),sK9_skl(slsdtgt0(xc))),slsdtgt0(xc)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( sQ48_spl
| ~ aElementOf0(sdtpldt0(sK8_skl(slsdtgt0(xc)),sK9_skl(slsdtgt0(xc))),slsdtgt0(xc)) ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f605,plain,
( ~ sQ2_spl
| ~ sQ41_spl
| ~ sQ44_spl
| ~ sQ48_spl
| ~ sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f599,f272,f253,f602,f553,f533,f228]) ).
fof(f607,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| aElement0(sdtpldt0(X2,sdtpldt0(X0,smndt0(X1))))
| ~ aElementOf0(X2,slsdtgt0(sz00))
| ~ sdteqdtlpzmzozddtrp0(X0,X1,slsdtgt0(sz00))
| ~ aIdeal0(slsdtgt0(sz00))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f132,f391]) ).
fof(f614,definition,
! [X0,X1,X2] :
( sQ49_spl
<=> ( aElement0(sdtpldt0(X2,sdtpldt0(X0,smndt0(X1))))
| ~ aElementOf0(X2,slsdtgt0(sz00))
| ~ sdteqdtlpzmzozddtrp0(X0,X1,slsdtgt0(sz00))
| ~ aElement0(X1)
| ~ aElement0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f617,plain,
( ~ sQ23_spl
| ~ sQ32_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f607,f614,f477,f390]) ).
fof(f637,plain,
( ~ sQ0_spl
| sQ48_spl
| ~ aElementOf0(sK9_skl(slsdtgt0(xc)),slsdtgt0(xc))
| ~ aElementOf0(sK8_skl(slsdtgt0(xc)),slsdtgt0(xc)) ),
inference(resolution,[status(thm)],[f604,f222]) ).
fof(f639,plain,
( ~ sQ0_spl
| sQ48_spl
| ~ sQ45_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f637,f553,f556,f602,f221]) ).
fof(f641,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f273,f203]) ).
fof(f642,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f641]) ).
fof(f643,plain,
$false,
inference(sat_refutation,[status(thm)],[f227,f234,f259,f264,f270,f278,f309,f311,f317,f352,f371,f373,f396,f398,f416,f424,f442,f455,f469,f473,f480,f484,f488,f492,f502,f506,f510,f532,f559,f562,f566,f573,f578,f605,f617,f639,f642]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG106+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n004.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 04:20:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 0.14/0.47 % Refutation found
% 0.14/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.50 % Elapsed time: 0.125871 seconds
% 0.14/0.50 % CPU time: 0.722564 seconds
% 0.14/0.50 % Total memory used: 97.348 MB
% 0.14/0.50 % Net memory used: 96.037 MB
%------------------------------------------------------------------------------