%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG092+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 : n013.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:56 PM UTC 2026
% Result : Theorem 0.13s 0.45s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 43
% Syntax : Number of formulae : 193 ( 12 unt; 39 def)
% Number of atoms : 897 ( 54 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 1159 ( 455 ~; 504 |; 141 &)
% ( 48 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 36 prp; 0-5 aty)
% Number of functors : 20 ( 20 usr; 3 con; 0-4 aty)
% Number of variables : 382 ( 342 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aElement0(sz10),
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(f22,definition,
! [W0,W1] :
( ( aSet0(W1)
& aSet0(W0) )
=> ! [W2] :
( W2 = sdtpldt1(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4,W5] :
( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,W1)
& aElementOf0(W4,W0) ) )
& aSet0(W2) ) ) ),
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(f25,hypothesis,
( aIdeal0(xJ)
& aIdeal0(xI) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,conjecture,
( ! [W0,W1,W2] :
( ( aElement0(W2)
& aElementOf0(W1,sdtpldt1(xI,xJ))
& aElementOf0(W0,sdtpldt1(xI,xJ)) )
=> ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
=> aIdeal0(sdtpldt1(xI,xJ)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
~ ( ! [W0,W1,W2] :
( ( aElement0(W2)
& aElementOf0(W1,sdtpldt1(xI,xJ))
& aElementOf0(W0,sdtpldt1(xI,xJ)) )
=> ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) ) )
=> aIdeal0(sdtpldt1(xI,xJ)) ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f32,plain,
aElement0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f71,plain,
! [W0] :
( ! [W1] :
( aElement0(W1)
| ~ aElementOf0(W1,W0) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f72,plain,
! [X0,X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f79,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtpldt1(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4,W5] :
( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,W1)
& aElementOf0(W4,W0) ) )
& aSet0(W2) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f80,definition,
! [W0,W1,W3,W4,W5] :
( sP1_prd(W5,W4,W3,W1,W0)
<=> ( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,W1)
& aElementOf0(W4,W0) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f81,plain,
! [W0,W1] :
( ! [W2] :
( W2 = sdtpldt1(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4,W5] : sP1_prd(W5,W4,W3,W1,W0) )
& aSet0(W2) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(formula_renaming,[status(thm)],[f79,f80]) ).
fof(f82,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] :
( ( ? [W4,W5] : sP1_prd(W5,W4,W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ! [W4,W5] : ~ sP1_prd(W5,W4,W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtpldt1(W0,W1) )
& ( ( ! [W3] :
( ( ! [W4,W5] : ~ sP1_prd(W5,W4,W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ? [W4,W5] : sP1_prd(W5,W4,W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtpldt1(W0,W1) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [W0,W1] :
( ( ! [W2] :
( ? [W3] :
( ( ? [W4,W5] : sP1_prd(W5,W4,W3,W1,W0)
| aElementOf0(W3,W2) )
& ( ! [W4,W5] : ~ sP1_prd(W5,W4,W3,W1,W0)
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtpldt1(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4,W5] : ~ sP1_prd(W5,W4,W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( ? [W4,W5] : sP1_prd(W5,W4,W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtpldt1(W0,W1) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f82]) ).
fof(f84,plain,
! [W0,W1] :
( ( ! [W2] :
( ( ( sP1_prd(sK6_skl(W2,W1,W0),sK5_skl(W2,W1,W0),sK4_skl(W2,W1,W0),W1,W0)
| aElementOf0(sK4_skl(W2,W1,W0),W2) )
& ( ! [W4,W5] : ~ sP1_prd(W5,W4,sK4_skl(W2,W1,W0),W1,W0)
| ~ aElementOf0(sK4_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtpldt1(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4,W5] : ~ sP1_prd(W5,W4,W3,W1,W0)
| aElementOf0(W3,W2) )
& ! [W3] :
( sP1_prd(sK3_skl(W3,W2,W1,W0),sK2_skl(W3,W2,W1,W0),W3,W1,W0)
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtpldt1(W0,W1) ) )
| ~ aSet0(W1)
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(W4,sK2_skl(W3,W2,W1,W0)),skolemize(W5,sK3_skl(W3,W2,W1,W0)),skolemize(W3,sK4_skl(W2,W1,W0)),skolemize(W4,sK5_skl(W2,W1,W0)),skolemize(W5,sK6_skl(W2,W1,W0))],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != sdtpldt1(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f90,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(f91,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)],[f90]) ).
fof(f92,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)],[f91]) ).
fof(f93,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))],[f92]) ).
fof(f94,plain,
! [X0,X1,X2] :
( aSet0(X2)
| X2 != sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( aElementOf0(X3,X0)
| ~ aElementOf0(X3,X2)
| X2 != sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f96,plain,
! [X0,X1,X2,X3] :
( aElementOf0(X3,X1)
| ~ aElementOf0(X3,X2)
| X2 != sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f99,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)],[f93]) ).
fof(f100,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)],[f93]) ).
fof(f101,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(f102,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)],[f101]) ).
fof(f103,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)],[f102]) ).
fof(f104,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))],[f103]) ).
fof(f105,plain,
! [X0] :
( aSet0(X0)
| ~ aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f108,plain,
! [X0] :
( aElementOf0(sK8_skl(X0),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f109,plain,
! [X0] :
( aElement0(sK10_skl(X0))
| aElementOf0(sK9_skl(X0),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f110,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)],[f104]) ).
fof(f111,plain,
! [X0] :
( aElement0(sK10_skl(X0))
| ~ aElementOf0(sdtpldt0(sK8_skl(X0),sK9_skl(X0)),X0)
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f112,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)],[f104]) ).
fof(f113,plain,
aIdeal0(xI),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f114,plain,
aIdeal0(xJ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f115,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ? [W3,W4] :
( ? [W5,W6] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) )
| ~ aElement0(W2)
| ~ aElementOf0(W1,sdtpldt1(xI,xJ))
| ~ aElementOf0(W0,sdtpldt1(xI,xJ)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f116,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ? [W3,W4] :
( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& ? [W5,W6] :
( sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(W3,W5),sdtpldt0(W4,W6))
& aElementOf0(sdtasdt0(W2,W4),xJ)
& aElementOf0(sdtasdt0(W2,W3),xI)
& aElementOf0(sdtpldt0(W4,W6),xJ)
& aElementOf0(sdtpldt0(W3,W5),xI)
& W1 = sdtpldt0(W5,W6)
& aElementOf0(W6,xJ)
& aElementOf0(W5,xI) )
& W0 = sdtpldt0(W3,W4)
& aElementOf0(W4,xJ)
& aElementOf0(W3,xI) )
| ~ aElement0(W2)
| ~ aElementOf0(W1,sdtpldt1(xI,xJ))
| ~ aElementOf0(W0,sdtpldt1(xI,xJ)) ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f117,plain,
( ~ aIdeal0(sdtpldt1(xI,xJ))
& ! [W0,W1,W2] :
( ( aElementOf0(sdtasdt0(W2,W0),sdtpldt1(xI,xJ))
& aElementOf0(sdtpldt0(W0,W1),sdtpldt1(xI,xJ))
& sdtpldt0(W0,W1) = sdtpldt0(sdtpldt0(sK11_skl(W2,W1,W0),sK13_skl(W2,W1,W0)),sdtpldt0(sK12_skl(W2,W1,W0),sK14_skl(W2,W1,W0)))
& aElementOf0(sdtasdt0(W2,sK12_skl(W2,W1,W0)),xJ)
& aElementOf0(sdtasdt0(W2,sK11_skl(W2,W1,W0)),xI)
& aElementOf0(sdtpldt0(sK12_skl(W2,W1,W0),sK14_skl(W2,W1,W0)),xJ)
& aElementOf0(sdtpldt0(sK11_skl(W2,W1,W0),sK13_skl(W2,W1,W0)),xI)
& W1 = sdtpldt0(sK13_skl(W2,W1,W0),sK14_skl(W2,W1,W0))
& aElementOf0(sK14_skl(W2,W1,W0),xJ)
& aElementOf0(sK13_skl(W2,W1,W0),xI)
& W0 = sdtpldt0(sK11_skl(W2,W1,W0),sK12_skl(W2,W1,W0))
& aElementOf0(sK12_skl(W2,W1,W0),xJ)
& aElementOf0(sK11_skl(W2,W1,W0),xI) )
| ~ aElement0(W2)
| ~ aElementOf0(W1,sdtpldt1(xI,xJ))
| ~ aElementOf0(W0,sdtpldt1(xI,xJ)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(W3,sK11_skl(W2,W1,W0)),skolemize(W4,sK12_skl(W2,W1,W0)),skolemize(W5,sK13_skl(W2,W1,W0)),skolemize(W6,sK14_skl(W2,W1,W0))],[f116]) ).
fof(f118,plain,
! [X0,X1,X2] :
( aElementOf0(sK11_skl(X2,X1,X0),xI)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
! [X0,X1,X2] :
( aElementOf0(sK12_skl(X2,X1,X0),xJ)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f121,plain,
! [X0,X1,X2] :
( aElementOf0(sK13_skl(X2,X1,X0),xI)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f122,plain,
! [X0,X1,X2] :
( aElementOf0(sK14_skl(X2,X1,X0),xJ)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f124,plain,
! [X0,X1,X2] :
( aElementOf0(sdtpldt0(sK11_skl(X2,X1,X0),sK13_skl(X2,X1,X0)),xI)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f125,plain,
! [X0,X1,X2] :
( aElementOf0(sdtpldt0(sK12_skl(X2,X1,X0),sK14_skl(X2,X1,X0)),xJ)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f126,plain,
! [X0,X1,X2] :
( aElementOf0(sdtasdt0(X2,sK11_skl(X2,X1,X0)),xI)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f127,plain,
! [X0,X1,X2] :
( aElementOf0(sdtasdt0(X2,sK12_skl(X2,X1,X0)),xJ)
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f129,plain,
! [X0,X1,X2] :
( aElementOf0(sdtpldt0(X0,X1),sdtpldt1(xI,xJ))
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f130,plain,
! [X0,X1,X2] :
( aElementOf0(sdtasdt0(X2,X0),sdtpldt1(xI,xJ))
| ~ aElement0(X2)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f131,plain,
~ aIdeal0(sdtpldt1(xI,xJ)),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f137,plain,
! [W0,W1,W3,W4,W5] :
( ( sdtpldt0(W4,W5) != W3
| ~ aElementOf0(W5,W1)
| ~ aElementOf0(W4,W0)
| sP1_prd(W5,W4,W3,W1,W0) )
& ( ( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,W1)
& aElementOf0(W4,W0) )
| ~ sP1_prd(W5,W4,W3,W1,W0) ) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f138,plain,
( ! [W0,W1,W3,W4,W5] :
( sdtpldt0(W4,W5) != W3
| ~ aElementOf0(W5,W1)
| ~ aElementOf0(W4,W0)
| sP1_prd(W5,W4,W3,W1,W0) )
& ! [W0,W1,W3,W4,W5] :
( ( sdtpldt0(W4,W5) = W3
& aElementOf0(W5,W1)
& aElementOf0(W4,W0) )
| ~ sP1_prd(W5,W4,W3,W1,W0) ) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f140,plain,
! [X0,X1,X2,X3,X4] :
( aElementOf0(X0,X3)
| ~ sP1_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f142,plain,
! [X0,X1,X2,X3,X4] :
( sdtpldt0(X1,X0) != X2
| ~ aElementOf0(X0,X3)
| ~ aElementOf0(X1,X4)
| sP1_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f143,definition,
! [X0,X1] :
( sQ0_spl
<=> ( aElementOf0(sdtpldt0(X0,X1),sdtpldt1(xI,xJ))
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f144,plain,
! [X0,X1] :
( ~ sQ0_spl
| aElementOf0(sdtpldt0(X0,X1),sdtpldt1(xI,xJ))
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f143]) ).
fof(f146,definition,
! [X2] :
( sQ1_spl
<=> ~ aElement0(X2) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f147,plain,
! [X0] :
( ~ sQ1_spl
| ~ aElement0(X0) ),
inference(component_clause,[status(thm)],[f146]) ).
fof(f149,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f129,f143,f146]) ).
fof(f150,definition,
! [X0,X2] :
( sQ2_spl
<=> ( aElementOf0(sdtasdt0(X2,X0),sdtpldt1(xI,xJ))
| ~ aElement0(X2)
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f151,plain,
! [X0,X1] :
( ~ sQ2_spl
| aElementOf0(sdtasdt0(X1,X0),sdtpldt1(xI,xJ))
| ~ aElement0(X1)
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f153,definition,
! [X1] :
( sQ3_spl
<=> ~ aElementOf0(X1,sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f154,plain,
! [X0] :
( ~ sQ3_spl
| ~ aElementOf0(X0,sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f156,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f130,f150,f153]) ).
fof(f157,plain,
! [X0,X1] :
( aSet0(sdtpldt1(X0,X1))
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f85]) ).
fof(f160,plain,
! [X0,X1] :
( aSet0(sdtasasdt0(X0,X1))
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f94]) ).
fof(f161,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,sdtasasdt0(X0,X1))
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f95]) ).
fof(f162,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X1)
| ~ aElementOf0(X2,sdtasasdt0(X0,X1))
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f96]) ).
fof(f164,plain,
! [X0,X1,X2,X3] :
( ~ aElementOf0(X0,X2)
| ~ aElementOf0(X1,X3)
| sP1_prd(X0,X1,sdtpldt0(X1,X0),X2,X3) ),
inference(destructive_equality_resolution,[status(thm)],[f142]) ).
fof(f165,plain,
aSet0(xJ),
inference(resolution,[status(thm)],[f105,f114]) ).
fof(f166,plain,
aSet0(xI),
inference(resolution,[status(thm)],[f105,f113]) ).
fof(f167,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK14_skl(X0,X1,X2))
| ~ aSet0(xJ) ),
inference(resolution,[status(thm)],[f72,f122]) ).
fof(f168,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(sK12_skl(X0,X1,X2),sK14_skl(X0,X1,X2)))
| ~ aSet0(xJ) ),
inference(resolution,[status(thm)],[f72,f125]) ).
fof(f169,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(sK11_skl(X0,X1,X2),sK13_skl(X0,X1,X2)))
| ~ aSet0(xI) ),
inference(resolution,[status(thm)],[f72,f124]) ).
fof(f170,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X0,X1))
| ~ aSet0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f72,f144]) ).
fof(f172,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK13_skl(X0,X1,X2))
| ~ aSet0(xI) ),
inference(resolution,[status(thm)],[f72,f121]) ).
fof(f173,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK12_skl(X0,X1,X2))
| ~ aSet0(xJ) ),
inference(resolution,[status(thm)],[f72,f119]) ).
fof(f174,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK11_skl(X0,X1,X2))
| ~ aSet0(xI) ),
inference(resolution,[status(thm)],[f72,f118]) ).
fof(f175,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtasdt0(X0,sK12_skl(X0,X1,X2)))
| ~ aSet0(xJ) ),
inference(resolution,[status(thm)],[f72,f127]) ).
fof(f176,plain,
! [X0,X1,X2] :
( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtasdt0(X0,sK11_skl(X0,X1,X2)))
| ~ aSet0(xI) ),
inference(resolution,[status(thm)],[f72,f126]) ).
fof(f177,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| aElement0(sdtasdt0(X0,X1))
| ~ aSet0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f72,f151]) ).
fof(f179,definition,
( sQ4_spl
<=> aSet0(xJ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f181,plain,
( sQ4_spl
| ~ aSet0(xJ) ),
inference(component_clause,[status(thm)],[f179]) ).
fof(f182,definition,
! [X0,X1,X2] :
( sQ5_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK14_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f167,f179,f182]) ).
fof(f186,definition,
! [X0,X1,X2] :
( sQ6_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(sK12_skl(X0,X1,X2),sK14_skl(X0,X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f189,plain,
( sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f168,f179,f186]) ).
fof(f190,definition,
( sQ7_spl
<=> aSet0(xI) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( sQ7_spl
| ~ aSet0(xI) ),
inference(component_clause,[status(thm)],[f190]) ).
fof(f193,definition,
! [X0,X1,X2] :
( sQ8_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(sK11_skl(X0,X1,X2),sK13_skl(X0,X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( sQ8_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f169,f190,f193]) ).
fof(f197,definition,
( sQ9_spl
<=> aSet0(sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( ~ sQ9_spl
| aSet0(sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f199,plain,
( sQ9_spl
| ~ aSet0(sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f200,definition,
! [X0,X1] :
( sQ10_spl
<=> ( ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f201,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X0,X1)) ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f203,plain,
( ~ sQ0_spl
| sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f170,f197,f200,f143]) ).
fof(f205,definition,
! [X0,X1,X2] :
( sQ11_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK13_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f208,plain,
( sQ11_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f172,f190,f205]) ).
fof(f209,definition,
! [X0,X1,X2] :
( sQ12_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK12_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f212,plain,
( sQ12_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f173,f179,f209]) ).
fof(f213,definition,
! [X0,X1,X2] :
( sQ13_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sK11_skl(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f216,plain,
( sQ13_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f174,f190,f213]) ).
fof(f217,definition,
! [X0,X1,X2] :
( sQ14_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtasdt0(X0,sK12_skl(X0,X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( sQ14_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f175,f179,f217]) ).
fof(f221,definition,
! [X0,X1,X2] :
( sQ15_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtasdt0(X0,sK11_skl(X0,X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( sQ15_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f176,f190,f221]) ).
fof(f225,definition,
! [X0,X1] :
( sQ16_spl
<=> ( ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| aElement0(sdtasdt0(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f226,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ aElement0(X0)
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| aElement0(sdtasdt0(X0,X1)) ),
inference(component_clause,[status(thm)],[f225]) ).
fof(f228,plain,
( ~ sQ2_spl
| sQ16_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f177,f197,f225,f150]) ).
fof(f230,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192,f166]) ).
fof(f231,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f230]) ).
fof(f232,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f181,f165]) ).
fof(f233,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f232]) ).
fof(f235,plain,
( ~ sQ1_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f32,f147]) ).
fof(f237,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f235]) ).
fof(f238,plain,
( sQ9_spl
| ~ aSet0(xJ)
| ~ aSet0(xI) ),
inference(resolution,[status(thm)],[f199,f157]) ).
fof(f239,plain,
( sQ9_spl
| ~ sQ4_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f238,f190,f179,f197]) ).
fof(f243,definition,
( sQ17_spl
<=> aIdeal0(sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( ~ sQ17_spl
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f288,plain,
! [X0,X1] :
( aElementOf0(sK8_skl(sdtasasdt0(X0,X1)),X0)
| ~ aSet0(X1)
| ~ aSet0(X0)
| ~ aSet0(sdtasasdt0(X0,X1))
| aIdeal0(sdtasasdt0(X0,X1)) ),
inference(resolution,[status(thm)],[f108,f161]) ).
fof(f289,plain,
( ~ sQ3_spl
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f108,f154]) ).
fof(f291,plain,
! [X0,X1] :
( aElementOf0(sK8_skl(sdtasasdt0(X0,X1)),X0)
| ~ aSet0(X1)
| ~ aSet0(X0)
| aIdeal0(sdtasasdt0(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f288,f160]) ).
fof(f292,plain,
( ~ sQ3_spl
| ~ sQ9_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f289,f243,f197,f153]) ).
fof(f294,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f244,f131]) ).
fof(f295,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f294]) ).
fof(f300,plain,
! [X0,X1] :
( ~ aSet0(sdtasasdt0(X0,X1))
| aIdeal0(sdtasasdt0(X0,X1))
| aElementOf0(sK8_skl(sdtasasdt0(X0,X1)),X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f162,f108]) ).
fof(f303,plain,
! [X0,X1] :
( aIdeal0(sdtasasdt0(X0,X1))
| aElementOf0(sK8_skl(sdtasasdt0(X0,X1)),X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f300,f160]) ).
fof(f317,plain,
! [X0,X1,X2] :
( ~ sQ16_spl
| aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X2),X2)
| ~ aSet0(sdtpldt1(xI,xJ))
| sdtpldt1(xI,xJ) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sK7_skl(sdtpldt1(xI,xJ),X1,X2))) ),
inference(resolution,[status(thm)],[f226,f99]) ).
fof(f318,plain,
! [X0] :
( ~ sQ16_spl
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ))
| ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sK8_skl(sdtpldt1(xI,xJ)))) ),
inference(resolution,[status(thm)],[f226,f108]) ).
fof(f321,definition,
! [X0,X1,X2] :
( sQ23_spl
<=> ( aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X2),X2)
| sdtpldt1(xI,xJ) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sK7_skl(sdtpldt1(xI,xJ),X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f324,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f317,f321,f197,f225]) ).
fof(f325,definition,
! [X0] :
( sQ24_spl
<=> ( ~ aElement0(X0)
| aElement0(sdtasdt0(X0,sK8_skl(sdtpldt1(xI,xJ)))) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f328,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| sQ17_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f318,f325,f243,f197,f225]) ).
fof(f342,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X2),X2)
| ~ aSet0(sdtpldt1(xI,xJ))
| sdtpldt1(xI,xJ) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X0,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X0,sK7_skl(sdtpldt1(xI,xJ),X1,X2))) ),
inference(resolution,[status(thm)],[f201,f99]) ).
fof(f343,plain,
! [X0] :
( ~ sQ10_spl
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ))
| ~ aElementOf0(X0,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X0,sK8_skl(sdtpldt1(xI,xJ)))) ),
inference(resolution,[status(thm)],[f201,f108]) ).
fof(f347,definition,
! [X0,X1,X2] :
( sQ27_spl
<=> ( aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X2),X2)
| sdtpldt1(xI,xJ) = sdtasasdt0(X2,X1)
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aElementOf0(X0,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X0,sK7_skl(sdtpldt1(xI,xJ),X1,X2))) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f350,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f342,f347,f197,f200]) ).
fof(f351,definition,
! [X0] :
( sQ28_spl
<=> ( ~ aElementOf0(X0,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X0,sK8_skl(sdtpldt1(xI,xJ)))) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| sQ17_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f343,f351,f243,f197,f200]) ).
fof(f374,definition,
( sQ31_spl
<=> aElement0(sK10_skl(sdtpldt1(xI,xJ))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f389,plain,
! [X0,X1,X2,X3] :
( aElementOf0(X2,X3)
| ~ aElementOf0(X2,X3)
| ~ aElementOf0(X0,X1) ),
inference(resolution,[status(thm)],[f164,f140]) ).
fof(f392,definition,
! [X0,X1] :
( sQ34_spl
<=> ~ aElementOf0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f393,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ aElementOf0(X0,X1) ),
inference(component_clause,[status(thm)],[f392]) ).
fof(f395,definition,
! [X2,X3] :
( sQ35_spl
<=> ( aElementOf0(X2,X3)
| ~ aElementOf0(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f398,plain,
( sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f389,f392,f395]) ).
fof(f408,plain,
! [X0] :
( ~ sQ34_spl
| ~ aSet0(X0)
| aIdeal0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f108,f393]) ).
fof(f413,plain,
( ~ sQ9_spl
| ~ sQ34_spl
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f408,f198]) ).
fof(f417,plain,
( ~ sQ9_spl
| ~ sQ34_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f413,f243,f392,f197]) ).
fof(f457,plain,
( ~ sQ2_spl
| ~ aElementOf0(sdtpldt0(sK8_skl(sdtpldt1(xI,xJ)),sK9_skl(sdtpldt1(xI,xJ))),sdtpldt1(xI,xJ))
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ))
| ~ aElement0(sK10_skl(sdtpldt1(xI,xJ)))
| ~ aElementOf0(sK8_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f151,f112]) ).
fof(f461,definition,
( sQ36_spl
<=> aElementOf0(sK8_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( ~ sQ36_spl
| aElementOf0(sK8_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f463,plain,
( sQ36_spl
| ~ aElementOf0(sK8_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,definition,
( sQ37_spl
<=> aElementOf0(sdtpldt0(sK8_skl(sdtpldt1(xI,xJ)),sK9_skl(sdtpldt1(xI,xJ))),sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( sQ37_spl
| ~ aElementOf0(sdtpldt0(sK8_skl(sdtpldt1(xI,xJ)),sK9_skl(sdtpldt1(xI,xJ))),sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f467,plain,
( ~ sQ2_spl
| ~ sQ37_spl
| ~ sQ9_spl
| sQ17_spl
| ~ sQ31_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f457,f461,f374,f243,f197,f464,f150]) ).
fof(f469,plain,
( sQ36_spl
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f463,f108]) ).
fof(f470,plain,
( sQ36_spl
| ~ sQ9_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f469,f243,f197,f461]) ).
fof(f473,plain,
( ~ sQ36_spl
| aElement0(sK8_skl(sdtpldt1(xI,xJ)))
| ~ aSet0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f462,f72]) ).
fof(f474,definition,
( sQ38_spl
<=> aElement0(sK8_skl(sdtpldt1(xI,xJ))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( ~ sQ36_spl
| sQ38_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f473,f197,f474,f461]) ).
fof(f502,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X1,sK8_skl(sdtasasdt0(sdtpldt1(xI,xJ),X0))))
| ~ aSet0(X0)
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtasasdt0(sdtpldt1(xI,xJ),X0)) ),
inference(resolution,[status(thm)],[f291,f201]) ).
fof(f503,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ aElement0(X1)
| aElement0(sdtasdt0(X1,sK8_skl(sdtasasdt0(sdtpldt1(xI,xJ),X0))))
| ~ aSet0(X0)
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtasasdt0(sdtpldt1(xI,xJ),X0)) ),
inference(resolution,[status(thm)],[f291,f226]) ).
fof(f507,definition,
! [X0,X1] :
( sQ39_spl
<=> ( ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X1,sK8_skl(sdtasasdt0(sdtpldt1(xI,xJ),X0))))
| ~ aSet0(X0)
| aIdeal0(sdtasasdt0(sdtpldt1(xI,xJ),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f502,f507,f197,f200]) ).
fof(f511,definition,
! [X0,X1] :
( sQ40_spl
<=> ( ~ aElement0(X1)
| aElement0(sdtasdt0(X1,sK8_skl(sdtasasdt0(sdtpldt1(xI,xJ),X0))))
| ~ aSet0(X0)
| aIdeal0(sdtasasdt0(sdtpldt1(xI,xJ),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f503,f511,f197,f225]) ).
fof(f518,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X1,sK8_skl(sdtasasdt0(X0,sdtpldt1(xI,xJ)))))
| aIdeal0(sdtasasdt0(X0,sdtpldt1(xI,xJ)))
| ~ aSet0(sdtpldt1(xI,xJ))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f303,f201]) ).
fof(f519,plain,
! [X0,X1] :
( ~ sQ16_spl
| ~ aElement0(X1)
| aElement0(sdtasdt0(X1,sK8_skl(sdtasasdt0(X0,sdtpldt1(xI,xJ)))))
| aIdeal0(sdtasasdt0(X0,sdtpldt1(xI,xJ)))
| ~ aSet0(sdtpldt1(xI,xJ))
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f303,f226]) ).
fof(f523,definition,
! [X0,X1] :
( sQ41_spl
<=> ( ~ aElementOf0(X1,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X1,sK8_skl(sdtasasdt0(X0,sdtpldt1(xI,xJ)))))
| aIdeal0(sdtasasdt0(X0,sdtpldt1(xI,xJ)))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f526,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f518,f523,f197,f200]) ).
fof(f527,definition,
! [X0,X1] :
( sQ42_spl
<=> ( ~ aElement0(X1)
| aElement0(sdtasdt0(X1,sK8_skl(sdtasasdt0(X0,sdtpldt1(xI,xJ)))))
| aIdeal0(sdtasasdt0(X0,sdtpldt1(xI,xJ)))
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f530,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f519,f527,f197,f225]) ).
fof(f532,plain,
( ~ sQ0_spl
| ~ aElementOf0(sK9_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ))
| ~ aElementOf0(sK8_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ))
| aElement0(sK10_skl(sdtpldt1(xI,xJ)))
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f111,f144]) ).
fof(f534,definition,
( sQ43_spl
<=> aElementOf0(sK9_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f536,plain,
( sQ43_spl
| ~ aElementOf0(sK9_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ)) ),
inference(component_clause,[status(thm)],[f534]) ).
fof(f537,plain,
( ~ sQ0_spl
| ~ sQ43_spl
| ~ sQ36_spl
| sQ31_spl
| ~ sQ9_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f532,f243,f197,f374,f461,f534,f143]) ).
fof(f538,plain,
( ~ sQ2_spl
| ~ aElement0(sK10_skl(sdtpldt1(xI,xJ)))
| ~ aElementOf0(sK8_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ))
| aElementOf0(sK9_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ))
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f110,f151]) ).
fof(f540,plain,
( ~ sQ2_spl
| ~ sQ31_spl
| ~ sQ36_spl
| sQ43_spl
| ~ sQ9_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f538,f243,f197,f534,f461,f374,f150]) ).
fof(f543,plain,
! [X0,X1,X2] :
( ~ sQ10_spl
| ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X2,sK7_skl(sdtpldt1(xI,xJ),X1,X0)))
| aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X0),X1)
| ~ aSet0(sdtpldt1(xI,xJ))
| sdtpldt1(xI,xJ) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f100,f201]) ).
fof(f544,plain,
! [X0,X1,X2] :
( ~ sQ16_spl
| ~ aElement0(X2)
| aElement0(sdtasdt0(X2,sK7_skl(sdtpldt1(xI,xJ),X1,X0)))
| aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X0),X1)
| ~ aSet0(sdtpldt1(xI,xJ))
| sdtpldt1(xI,xJ) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f100,f226]) ).
fof(f548,definition,
! [X0,X1,X2] :
( sQ44_spl
<=> ( ~ aElementOf0(X2,sdtpldt1(xI,xJ))
| aElement0(sdtpldt0(X2,sK7_skl(sdtpldt1(xI,xJ),X1,X0)))
| aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X0),X1)
| sdtpldt1(xI,xJ) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f551,plain,
( ~ sQ10_spl
| ~ sQ9_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f543,f548,f197,f200]) ).
fof(f552,definition,
! [X0,X1,X2] :
( sQ45_spl
<=> ( ~ aElement0(X2)
| aElement0(sdtasdt0(X2,sK7_skl(sdtpldt1(xI,xJ),X1,X0)))
| aElementOf0(sK7_skl(sdtpldt1(xI,xJ),X1,X0),X1)
| sdtpldt1(xI,xJ) = sdtasasdt0(X0,X1)
| ~ aSet0(X1)
| ~ aSet0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f544,f552,f197,f225]) ).
fof(f567,plain,
( ~ sQ0_spl
| sQ37_spl
| ~ aElementOf0(sK9_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ))
| ~ aElementOf0(sK8_skl(sdtpldt1(xI,xJ)),sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f466,f144]) ).
fof(f569,plain,
( ~ sQ0_spl
| sQ37_spl
| ~ sQ43_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f567,f461,f534,f464,f143]) ).
fof(f573,plain,
( sQ43_spl
| aElement0(sK10_skl(sdtpldt1(xI,xJ)))
| ~ aSet0(sdtpldt1(xI,xJ))
| aIdeal0(sdtpldt1(xI,xJ)) ),
inference(resolution,[status(thm)],[f536,f109]) ).
fof(f574,plain,
( sQ43_spl
| sQ31_spl
| ~ sQ9_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f573,f243,f197,f374,f534]) ).
fof(f575,plain,
$false,
inference(sat_refutation,[status(thm)],[f149,f156,f185,f189,f196,f203,f208,f212,f216,f220,f224,f228,f231,f233,f237,f239,f292,f295,f324,f328,f350,f354,f398,f417,f467,f470,f477,f510,f514,f526,f530,f537,f540,f551,f555,f569,f574]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG092+1 : 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 : n013.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.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Mon Sep 21 04:18:39 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.45 % Refutation found
% 0.13/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.48 % Elapsed time: 0.105505 seconds
% 0.13/0.48 % CPU time: 0.633221 seconds
% 0.13/0.48 % Total memory used: 95.861 MB
% 0.13/0.48 % Net memory used: 95.004 MB
%------------------------------------------------------------------------------