%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM523+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:40:51 PM UTC 2026
% Result : Theorem 0.06s 0.39s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 127
% Syntax : Number of formulae : 480 ( 23 unt; 101 def)
% Number of atoms : 2041 ( 436 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 2664 (1103 ~;1279 |; 136 &)
% ( 104 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 105 ( 103 usr; 99 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 383 ( 365 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtpldt0(W1,W0) = sdtpldt0(W2,W0)
| sdtpldt0(W0,W1) = sdtpldt0(W0,W2) )
=> W1 = W2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 != sz00
=> ! [W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1) )
=> ( ( sdtasdt0(W1,W0) = sdtasdt0(W2,W0)
| sdtasdt0(W0,W1) = sdtasdt0(W0,W2) )
=> W1 = W2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtpldt0(W0,W1) = sz00
=> ( W1 = sz00
& W0 = sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| W0 = sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W0,W1)
& W0 != W1 )
=> ! [W2] :
( aNaturalNumber0(W2)
=> ( sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2))
& sdtpldt0(W0,W2) != sdtpldt0(W1,W2)
& sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1))
& sdtpldt0(W2,W0) != sdtpldt0(W2,W1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( ( sdtlseqdt0(sz10,W0)
& sz10 != W0 )
| W0 = sz10
| W0 = sz00 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,definition,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W1,W2)
& doDivides0(W0,W1) )
=> doDivides0(W0,W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,sdtpldt0(W1,W2))
& doDivides0(W0,W1) )
=> doDivides0(W0,W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( W1 != sz00
& doDivides0(W0,W1) )
=> sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,definition,
! [W0] :
( aNaturalNumber0(W0)
=> ( isPrime0(W0)
<=> ( ! [W1] :
( ( doDivides0(W1,W0)
& aNaturalNumber0(W1) )
=> ( W1 = W0
| W1 = sz10 ) )
& W0 != sz10
& W0 != sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [W0] :
( ( W0 != sz10
& W0 != sz00
& aNaturalNumber0(W0) )
=> ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W2,sdtasdt0(W0,W1))
& isPrime0(W2) )
=> ( doDivides0(W2,W1)
| doDivides0(W2,W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
( xp != sz00
& xm != sz00
& xn != sz00
& aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
! [W0,W1,W2] :
( ( W2 != sz00
& W1 != sz00
& W0 != sz00
& aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtasdt0(W2,sdtasdt0(W1,W1)) = sdtasdt0(W0,W0)
=> ( iLess0(W0,xn)
=> ~ ( isPrime0(W2)
| ( ! [W3] :
( ( doDivides0(W3,W2)
& ? [W4] :
( W2 = sdtasdt0(W3,W4)
& aNaturalNumber0(W4) )
& aNaturalNumber0(W3) )
=> ( W3 = W2
| W3 = sz10 ) )
& W2 != sz10 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
( isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,conjecture,
( ( doDivides0(xp,xn)
| ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) )
& ( doDivides0(xp,sdtasdt0(xn,xn))
| ? [W0] :
( sdtasdt0(xn,xn) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
~ ( ( doDivides0(xp,xn)
| ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) )
& ( doDivides0(xp,sdtasdt0(xn,xn))
| ? [W0] :
( sdtasdt0(xn,xn) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f49,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f50,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f51,plain,
sz10 != sz00,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f54,plain,
! [W0,W1] :
( aNaturalNumber0(sdtasdt0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f55,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f60,plain,
! [W0] :
( ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f62,plain,
! [X0] :
( X0 = sdtpldt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f65,plain,
! [W0,W1,W2] :
( sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f66,plain,
! [X0,X1,X2] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [W0] :
( ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f68,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0] :
( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f70,plain,
! [W0] :
( ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f71,plain,
! [X0] :
( sdtasdt0(X0,sz00) = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f72,plain,
! [X0] :
( sz00 = sdtasdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f76,plain,
! [W0,W1,W2] :
( W1 = W2
| ( sdtpldt0(W1,W0) != sdtpldt0(W2,W0)
& sdtpldt0(W0,W1) != sdtpldt0(W0,W2) )
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f77,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f79,plain,
! [W0] :
( ! [W1,W2] :
( W1 = W2
| ( sdtasdt0(W1,W0) != sdtasdt0(W2,W0)
& sdtasdt0(W0,W1) != sdtasdt0(W0,W2) )
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1) )
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f80,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [X0,X1,X2] :
( X1 = X2
| sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
! [W0,W1] :
( ( W1 = sz00
& W0 = sz00 )
| sdtpldt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f83,plain,
! [X0,X1] :
( X0 = sz00
| sdtpldt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
! [X0,X1] :
( X1 = sz00
| sdtpldt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f85,plain,
! [W0,W1] :
( W1 = sz00
| W0 = sz00
| sdtasdt0(W0,W1) != sz00
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f86,plain,
! [X0,X1] :
( X1 = sz00
| X0 = sz00
| sdtasdt0(X0,X1) != sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
! [W0,W1] :
( ( sdtlseqdt0(W0,W1)
<=> ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f88,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| sdtlseqdt0(W0,W1) )
& ( ? [W2] :
( sdtpldt0(W0,W2) = W1
& aNaturalNumber0(W2) )
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtpldt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| sdtlseqdt0(W0,W1) )
& ( ( sdtpldt0(W0,sK0_skl(W1,W0)) = W1
& aNaturalNumber0(sK0_skl(W1,W0)) )
| ~ sdtlseqdt0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f88]) ).
fof(f91,plain,
! [X0,X1] :
( sdtpldt0(X0,sK0_skl(X1,X0)) = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f92,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f101,plain,
! [W0,W1] :
( W0 = W1
| ~ sdtlseqdt0(W1,W0)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f102,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [W0,W1,W2] :
( sdtlseqdt0(W0,W2)
| ~ sdtlseqdt0(W1,W2)
| ~ sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f104,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [W0,W1] :
( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f107,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f108,plain,
! [W0,W1] :
( ! [W2] :
( ( sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2))
& sdtpldt0(W0,W2) != sdtpldt0(W1,W2)
& sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1))
& sdtpldt0(W2,W0) != sdtpldt0(W2,W1) )
| ~ aNaturalNumber0(W2) )
| ~ sdtlseqdt0(W0,W1)
| W0 = W1
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f109,plain,
! [X0,X1,X2] :
( sdtpldt0(X2,X0) != sdtpldt0(X2,X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f118,plain,
! [W0] :
( ( sdtlseqdt0(sz10,W0)
& sz10 != W0 )
| W0 = sz10
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f120,plain,
! [X0] :
( sdtlseqdt0(sz10,X0)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f127,plain,
! [W0,W1] :
( ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f128,plain,
! [W0,W1] :
( ( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [W0,W1] :
( ( ( ! [W2] :
( W1 != sdtasdt0(W0,W2)
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ( W1 = sdtasdt0(W0,sK1_skl(W1,W0))
& aNaturalNumber0(sK1_skl(W1,W0)) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f128]) ).
fof(f131,plain,
! [X0,X1] :
( X1 = sdtasdt0(X0,sK1_skl(X1,X0))
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f132,plain,
! [X0,X1,X2] :
( X1 != sdtasdt0(X0,X2)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f139,plain,
! [W0,W1,W2] :
( doDivides0(W0,W2)
| ~ doDivides0(W1,W2)
| ~ doDivides0(W0,W1)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f140,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f143,plain,
! [W0,W1,W2] :
( doDivides0(W0,W2)
| ~ doDivides0(W0,sdtpldt0(W1,W2))
| ~ doDivides0(W0,W1)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f144,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X0,sdtpldt0(X1,X2))
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f145,plain,
! [W0,W1] :
( sdtlseqdt0(W0,W1)
| W1 = sz00
| ~ doDivides0(W0,W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f146,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| X1 = sz00
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f149,plain,
! [W0] :
( ( isPrime0(W0)
<=> ( ! [W1] :
( W1 = W0
| W1 = sz10
| ~ doDivides0(W1,W0)
| ~ aNaturalNumber0(W1) )
& W0 != sz10
& W0 != sz00 ) )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f150,plain,
! [W0] :
( ( ( ? [W1] :
( W1 != W0
& W1 != sz10
& doDivides0(W1,W0)
& aNaturalNumber0(W1) )
| W0 = sz10
| W0 = sz00
| isPrime0(W0) )
& ( ( ! [W1] :
( W1 = W0
| W1 = sz10
| ~ doDivides0(W1,W0)
| ~ aNaturalNumber0(W1) )
& W0 != sz10
& W0 != sz00 )
| ~ isPrime0(W0) ) )
| ~ aNaturalNumber0(W0) ),
inference(NNF_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
! [W0] :
( ( ( ( sK2_skl(W0) != W0
& sK2_skl(W0) != sz10
& doDivides0(sK2_skl(W0),W0)
& aNaturalNumber0(sK2_skl(W0)) )
| W0 = sz10
| W0 = sz00
| isPrime0(W0) )
& ( ( ! [W1] :
( W1 = W0
| W1 = sz10
| ~ doDivides0(W1,W0)
| ~ aNaturalNumber0(W1) )
& W0 != sz10
& W0 != sz00 )
| ~ isPrime0(W0) ) )
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W1,sK2_skl(W0))],[f150]) ).
fof(f152,plain,
! [X0] :
( X0 != sz00
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [X0] :
( X0 != sz10
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,plain,
! [X0] :
( aNaturalNumber0(sK2_skl(X0))
| X0 = sz10
| X0 = sz00
| isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f156,plain,
! [X0] :
( doDivides0(sK2_skl(X0),X0)
| X0 = sz10
| X0 = sz00
| isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f157,plain,
! [X0] :
( sK2_skl(X0) != sz10
| X0 = sz10
| X0 = sz00
| isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f158,plain,
! [X0] :
( sK2_skl(X0) != X0
| X0 = sz10
| X0 = sz00
| isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f159,plain,
! [W0] :
( ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) )
| W0 = sz10
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f160,plain,
! [W0] :
( ( isPrime0(sK3_skl(W0))
& doDivides0(sK3_skl(W0),W0)
& aNaturalNumber0(sK3_skl(W0)) )
| W0 = sz10
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W1,sK3_skl(W0))],[f159]) ).
fof(f161,plain,
! [X0] :
( aNaturalNumber0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
! [X0] :
( doDivides0(sK3_skl(X0),X0)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f163,plain,
! [X0] :
( isPrime0(sK3_skl(X0))
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f164,plain,
! [W0,W1,W2] :
( doDivides0(W2,W1)
| doDivides0(W2,W0)
| ~ doDivides0(W2,sdtasdt0(W0,W1))
| ~ isPrime0(W2)
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f165,plain,
! [X0,X1,X2] :
( doDivides0(X2,X1)
| doDivides0(X2,X0)
| ~ doDivides0(X2,sdtasdt0(X0,X1))
| ~ isPrime0(X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f166,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f167,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f168,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f169,plain,
xn != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f170,plain,
xm != sz00,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f172,plain,
! [W0,W1,W2] :
( ( ~ isPrime0(W2)
& ( ? [W3] :
( W3 != W2
& W3 != sz10
& doDivides0(W3,W2)
& ? [W4] :
( W2 = sdtasdt0(W3,W4)
& aNaturalNumber0(W4) )
& aNaturalNumber0(W3) )
| W2 = sz10 ) )
| ~ iLess0(W0,xn)
| sdtasdt0(W2,sdtasdt0(W1,W1)) != sdtasdt0(W0,W0)
| W2 = sz00
| W1 = sz00
| W0 = sz00
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f173,plain,
! [W0,W1,W2] :
( ( ~ isPrime0(W2)
& ( ( sK4_skl(W2,W1,W0) != W2
& sK4_skl(W2,W1,W0) != sz10
& doDivides0(sK4_skl(W2,W1,W0),W2)
& W2 = sdtasdt0(sK4_skl(W2,W1,W0),sK5_skl(W2,W1,W0))
& aNaturalNumber0(sK5_skl(W2,W1,W0))
& aNaturalNumber0(sK4_skl(W2,W1,W0)) )
| W2 = sz10 ) )
| ~ iLess0(W0,xn)
| sdtasdt0(W2,sdtasdt0(W1,W1)) != sdtasdt0(W0,W0)
| W2 = sz00
| W1 = sz00
| W0 = sz00
| ~ aNaturalNumber0(W2)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(W3,sK4_skl(W2,W1,W0)),skolemize(W4,sK5_skl(W2,W1,W0))],[f172]) ).
fof(f174,plain,
! [X0,X1,X2] :
( aNaturalNumber0(sK4_skl(X2,X1,X0))
| X2 = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f175,plain,
! [X0,X1,X2] :
( aNaturalNumber0(sK5_skl(X2,X1,X0))
| X2 = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f176,plain,
! [X0,X1,X2] :
( X2 = sdtasdt0(sK4_skl(X2,X1,X0),sK5_skl(X2,X1,X0))
| X2 = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f177,plain,
! [X0,X1,X2] :
( doDivides0(sK4_skl(X2,X1,X0),X2)
| X2 = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f178,plain,
! [X0,X1,X2] :
( sK4_skl(X2,X1,X0) != sz10
| X2 = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f179,plain,
! [X0,X1,X2] :
( sK4_skl(X2,X1,X0) != X2
| X2 = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f180,plain,
! [X0,X1,X2] :
( ~ isPrime0(X2)
| ~ iLess0(X0,xn)
| sdtasdt0(X2,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X2 = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f181,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f182,plain,
( isPrime0(xp)
& ! [W0] :
( W0 = xp
| W0 = sz10
| ( ~ doDivides0(W0,xp)
& ! [W1] :
( xp != sdtasdt0(W0,W1)
| ~ aNaturalNumber0(W1) ) )
| ~ aNaturalNumber0(W0) )
& xp != sz10 ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f184,plain,
! [X0,X1] :
( X0 = xp
| X0 = sz10
| xp != sdtasdt0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f185,plain,
! [X0] :
( X0 = xp
| X0 = sz10
| ~ doDivides0(X0,xp)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f186,plain,
isPrime0(xp),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f187,plain,
( ( ~ doDivides0(xp,xn)
& ! [W0] :
( xn != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) )
| ( ~ doDivides0(xp,sdtasdt0(xn,xn))
& ! [W0] :
( sdtasdt0(xn,xn) != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f188,definition,
( sP0_prd
<=> ( ~ doDivides0(xp,sdtasdt0(xn,xn))
& ! [W0] :
( sdtasdt0(xn,xn) != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f189,plain,
( ( ~ doDivides0(xp,xn)
& ! [W0] :
( xn != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f187,f188]) ).
fof(f190,plain,
! [X0] :
( xn != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f191,plain,
( ~ doDivides0(xp,xn)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f192,plain,
( ( doDivides0(xp,sdtasdt0(xn,xn))
| ? [W0] :
( sdtasdt0(xn,xn) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
| sP0_prd )
& ( ( ~ doDivides0(xp,sdtasdt0(xn,xn))
& ! [W0] :
( sdtasdt0(xn,xn) != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) )
| ~ sP0_prd ) ),
inference(NNF_transformation,[status(thm)],[f188]) ).
fof(f193,plain,
( ( doDivides0(xp,sdtasdt0(xn,xn))
| ( sdtasdt0(xn,xn) = sdtasdt0(xp,sK6_skl)
& aNaturalNumber0(sK6_skl) )
| sP0_prd )
& ( ( ~ doDivides0(xp,sdtasdt0(xn,xn))
& ! [W0] :
( sdtasdt0(xn,xn) != sdtasdt0(xp,W0)
| ~ aNaturalNumber0(W0) ) )
| ~ sP0_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W0,sK6_skl)],[f192]) ).
fof(f194,plain,
! [X0] :
( sdtasdt0(xn,xn) != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f196,plain,
( doDivides0(xp,sdtasdt0(xn,xn))
| aNaturalNumber0(sK6_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f197,plain,
( doDivides0(xp,sdtasdt0(xn,xn))
| sdtasdt0(xn,xn) = sdtasdt0(xp,sK6_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f198,definition,
( sQ0_spl
<=> sP0_prd ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f201,definition,
! [X0] :
( sQ1_spl
<=> ( xn != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f204,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f190,f198,f201]) ).
fof(f205,definition,
( sQ2_spl
<=> doDivides0(xp,xn) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( sQ2_spl
| ~ doDivides0(xp,xn) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,plain,
( ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f191,f198,f205]) ).
fof(f209,definition,
! [X0] :
( sQ3_spl
<=> ( sdtasdt0(xn,xn) != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f210,plain,
! [X0] :
( ~ sQ3_spl
| sdtasdt0(xn,xn) != sdtasdt0(xp,X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f209]) ).
fof(f212,plain,
( sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f194,f198,f209]) ).
fof(f213,definition,
( sQ4_spl
<=> doDivides0(xp,sdtasdt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( ~ sQ4_spl
| doDivides0(xp,sdtasdt0(xn,xn)) ),
inference(component_clause,[status(thm)],[f213]) ).
fof(f217,definition,
( sQ5_spl
<=> aNaturalNumber0(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( sQ4_spl
| sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f196,f198,f217,f213]) ).
fof(f221,definition,
( sQ6_spl
<=> sdtasdt0(xn,xn) = sdtasdt0(xp,sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f222,plain,
( ~ sQ6_spl
| sdtasdt0(xn,xn) = sdtasdt0(xp,sK6_skl) ),
inference(component_clause,[status(thm)],[f221]) ).
fof(f224,plain,
( sQ4_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f197,f198,f221,f213]) ).
fof(f229,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(sdtasdt0(X0,X1),sdtasdt0(X0,sdtasdt0(X1,X2)))
| ~ aNaturalNumber0(sdtasdt0(X0,sdtasdt0(X1,X2)))
| ~ aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(resolution,[status(thm)],[f132,f66]) ).
fof(f236,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(sdtasdt0(X0,X1),sdtasdt0(X0,sdtasdt0(X1,X2)))
| ~ aNaturalNumber0(sdtasdt0(X0,sdtasdt0(X1,X2)))
| ~ aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f229]) ).
fof(f237,plain,
! [X0,X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(sdtasdt0(X0,X1),sdtasdt0(X0,sdtasdt0(X1,X2)))
| ~ aNaturalNumber0(sdtasdt0(X0,sdtasdt0(X1,X2))) ),
inference(forward_subsumption_resolution,[status(thm)],[f236,f55]) ).
fof(f246,plain,
! [X0] :
( ~ aNaturalNumber0(sz10)
| doDivides0(X0,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f68,f132]) ).
fof(f248,definition,
! [X0] :
( sQ7_spl
<=> ( doDivides0(X0,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f249,plain,
! [X0] :
( ~ sQ7_spl
| doDivides0(X0,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f248]) ).
fof(f251,definition,
( sQ8_spl
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f253,plain,
( sQ8_spl
| ~ aNaturalNumber0(sz10) ),
inference(component_clause,[status(thm)],[f251]) ).
fof(f254,plain,
( ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f246,f248,f251]) ).
fof(f255,plain,
! [X0] :
( ~ sQ7_spl
| doDivides0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f249]) ).
fof(f261,definition,
( sQ9_spl
<=> aNaturalNumber0(xp) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( sQ9_spl
| ~ aNaturalNumber0(xp) ),
inference(component_clause,[status(thm)],[f261]) ).
fof(f267,definition,
( sQ11_spl
<=> aNaturalNumber0(sdtasdt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( ~ sQ11_spl
| aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(component_clause,[status(thm)],[f267]) ).
fof(f269,plain,
( sQ11_spl
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(component_clause,[status(thm)],[f267]) ).
fof(f275,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f69,f132]) ).
fof(f277,definition,
! [X0] :
( sQ12_spl
<=> ( ~ aNaturalNumber0(X0)
| doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f278,plain,
! [X0] :
( ~ sQ12_spl
| ~ aNaturalNumber0(X0)
| doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,plain,
( ~ sQ8_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f275,f277,f251]) ).
fof(f282,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f253,f50]) ).
fof(f283,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f282]) ).
fof(f284,plain,
! [X0] :
( ~ sQ12_spl
| doDivides0(sz10,X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f278]) ).
fof(f285,plain,
! [X0] :
( ~ aNaturalNumber0(sz00)
| doDivides0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f71,f132]) ).
fof(f286,definition,
! [X0] :
( sQ13_spl
<=> ( doDivides0(X0,sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f287,plain,
! [X0] :
( ~ sQ13_spl
| doDivides0(X0,sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f286]) ).
fof(f289,definition,
( sQ14_spl
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f291,plain,
( sQ14_spl
| ~ aNaturalNumber0(sz00) ),
inference(component_clause,[status(thm)],[f289]) ).
fof(f292,plain,
( ~ sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f285,f286,f289]) ).
fof(f293,plain,
! [X0] :
( ~ sQ13_spl
| doDivides0(X0,sz00)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f287]) ).
fof(f294,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f291,f49]) ).
fof(f295,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f294]) ).
fof(f296,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| doDivides0(sz00,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f72,f132]) ).
fof(f297,definition,
! [X0] :
( sQ15_spl
<=> ( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f298,plain,
! [X0] :
( ~ sQ15_spl
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f297]) ).
fof(f300,definition,
( sQ16_spl
<=> doDivides0(sz00,sz00) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f301,plain,
( ~ sQ16_spl
| doDivides0(sz00,sz00) ),
inference(component_clause,[status(thm)],[f300]) ).
fof(f303,plain,
( sQ16_spl
| ~ sQ14_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f296,f297,f289,f300]) ).
fof(f304,plain,
! [X0] :
( ~ sQ15_spl
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f298]) ).
fof(f305,plain,
( sQ11_spl
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f269,f55]) ).
fof(f306,definition,
( sQ17_spl
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( sQ17_spl
| ~ aNaturalNumber0(xn) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f309,plain,
( sQ11_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f305,f306,f267]) ).
fof(f310,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f166]) ).
fof(f311,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f310]) ).
fof(f312,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f263,f168]) ).
fof(f313,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f312]) ).
fof(f314,plain,
( ~ sQ15_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f167,f304]) ).
fof(f319,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f314]) ).
fof(f320,plain,
! [X0,X1] :
( X1 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(equality_resolution,[status(thm)],[f77]) ).
fof(f321,definition,
! [X0] :
( sQ18_spl
<=> ~ aNaturalNumber0(X0) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f322,plain,
! [X0] :
( ~ sQ18_spl
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f321]) ).
fof(f324,definition,
! [X1] :
( sQ19_spl
<=> ( X1 = X1
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f327,plain,
( sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f320,f321,f324]) ).
fof(f328,plain,
( ~ sQ4_spl
| sdtlseqdt0(xp,sdtasdt0(xn,xn))
| sdtasdt0(xn,xn) = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f214,f146]) ).
fof(f329,definition,
( sQ20_spl
<=> sdtasdt0(xn,xn) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( ~ sQ20_spl
| sdtasdt0(xn,xn) = sz00 ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,definition,
( sQ21_spl
<=> sdtlseqdt0(xp,sdtasdt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f333,plain,
( ~ sQ21_spl
| sdtlseqdt0(xp,sdtasdt0(xn,xn)) ),
inference(component_clause,[status(thm)],[f332]) ).
fof(f335,plain,
( ~ sQ4_spl
| sQ21_spl
| sQ20_spl
| ~ sQ11_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f328,f261,f267,f329,f332,f213]) ).
fof(f336,plain,
( ~ sQ18_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f166,f322]) ).
fof(f341,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f336]) ).
fof(f351,plain,
! [X0] :
( ~ sQ16_spl
| doDivides0(X0,sz00)
| ~ doDivides0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f140,f301]) ).
fof(f355,definition,
! [X0] :
( sQ23_spl
<=> ( doDivides0(X0,sz00)
| ~ doDivides0(X0,sz00)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f358,plain,
( ~ sQ16_spl
| ~ sQ14_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f351,f355,f289,f300]) ).
fof(f370,plain,
! [X0] :
( sQ2_spl
| ~ doDivides0(X0,xn)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f207,f140]) ).
fof(f371,definition,
! [X0] :
( sQ25_spl
<=> ( ~ doDivides0(X0,xn)
| ~ doDivides0(xp,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( sQ2_spl
| ~ sQ17_spl
| sQ25_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f370,f261,f371,f306,f205]) ).
fof(f381,plain,
! [X0,X1] :
( ~ sQ12_spl
| doDivides0(X1,X0)
| ~ doDivides0(X1,sz10)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f284,f140]) ).
fof(f382,definition,
! [X0,X1] :
( sQ26_spl
<=> ( doDivides0(X1,X0)
| ~ doDivides0(X1,sz10)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( ~ sQ12_spl
| ~ sQ8_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f381,f382,f251,f277]) ).
fof(f387,plain,
! [X0] :
( sK0_skl(sz00,X0) = sz00
| ~ aNaturalNumber0(sK0_skl(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f91,f84]) ).
fof(f388,plain,
! [X0] :
( X0 = sz00
| ~ aNaturalNumber0(sK0_skl(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f91,f83]) ).
fof(f390,definition,
! [X0] :
( sQ27_spl
<=> ( sK0_skl(sz00,X0) = sz00
| ~ aNaturalNumber0(sK0_skl(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( ~ sQ14_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f387,f390,f289]) ).
fof(f394,definition,
! [X0] :
( sQ28_spl
<=> ( X0 = sz00
| ~ aNaturalNumber0(sK0_skl(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( ~ sQ14_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f388,f394,f289]) ).
fof(f404,plain,
( ~ sQ20_spl
| xn = sz00
| xn = sz00
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f330,f86]) ).
fof(f413,definition,
( sQ29_spl
<=> xn = sz00 ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f414,plain,
( ~ sQ29_spl
| xn = sz00 ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f416,plain,
( ~ sQ20_spl
| sQ29_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f404,f306,f413,f329]) ).
fof(f429,definition,
( sQ33_spl
<=> sz00 = sz00 ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f443,plain,
( ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f169]) ).
fof(f444,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f443]) ).
fof(f445,plain,
! [X0,X1] :
( ~ sQ13_spl
| doDivides0(X1,sz00)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f293,f140]) ).
fof(f446,definition,
! [X0,X1] :
( sQ36_spl
<=> ( doDivides0(X1,sz00)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ13_spl
| ~ sQ14_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f445,f446,f289,f286]) ).
fof(f459,plain,
( xp != sz00
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f152,f186]) ).
fof(f460,definition,
( sQ37_spl
<=> xp = sz00 ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( ~ sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f459,f261,f460]) ).
fof(f464,plain,
( xp != sz10
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f153,f186]) ).
fof(f465,definition,
( sQ38_spl
<=> xp = sz10 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( ~ sQ38_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f464,f261,f465]) ).
fof(f486,plain,
( ~ sQ6_spl
| ~ aNaturalNumber0(sK6_skl)
| doDivides0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f222,f132]) ).
fof(f497,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| sQ4_spl
| ~ sQ11_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f486,f261,f267,f213,f217,f221]) ).
fof(f533,plain,
( ~ sQ7_spl
| ~ aNaturalNumber0(xp)
| xp = xp
| xp = sz10
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f185,f255]) ).
fof(f534,plain,
! [X0,X1] :
( ~ doDivides0(X1,xp)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| X0 = xp
| X0 = sz10
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f185,f140]) ).
fof(f535,definition,
( sQ48_spl
<=> sz10 = sz10 ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f539,definition,
( sQ49_spl
<=> xp = xp ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f542,plain,
( ~ sQ7_spl
| sQ49_spl
| sQ38_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f533,f261,f465,f539,f248]) ).
fof(f543,definition,
! [X0,X1] :
( sQ50_spl
<=> ( ~ doDivides0(X1,xp)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| X0 = xp
| X0 = sz10
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( ~ sQ9_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f534,f543,f261]) ).
fof(f548,plain,
! [X0] :
( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(sdtasdt0(sz10,X0))
| ~ aNaturalNumber0(X0)
| sz10 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtasdt0(sz10,X0)) ),
inference(resolution,[status(thm)],[f69,f80]) ).
fof(f550,plain,
( sz10 = xp
| sz10 = sz10
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f69,f184]) ).
fof(f557,definition,
! [X0] :
( sQ51_spl
<=> ( X0 = sdtasdt0(sz10,X0)
| ~ aNaturalNumber0(sdtasdt0(sz10,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(sz10,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f560,definition,
( sQ52_spl
<=> sz10 = sz00 ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f561,plain,
( ~ sQ52_spl
| sz10 = sz00 ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f563,plain,
( sQ52_spl
| ~ sQ8_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f548,f557,f251,f560]) ).
fof(f564,plain,
( sQ38_spl
| sQ48_spl
| ~ sQ8_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f550,f261,f251,f535,f465]) ).
fof(f569,plain,
( ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f561,f51]) ).
fof(f570,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f569]) ).
fof(f572,plain,
( ~ sQ21_spl
| sdtasdt0(xn,xn) = xp
| ~ sdtlseqdt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolution,[status(thm)],[f102,f333]) ).
fof(f574,definition,
( sQ53_spl
<=> sdtlseqdt0(sdtasdt0(xn,xn),xp) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( sQ53_spl
| ~ sdtlseqdt0(sdtasdt0(xn,xn),xp) ),
inference(component_clause,[status(thm)],[f574]) ).
fof(f577,definition,
( sQ54_spl
<=> sdtasdt0(xn,xn) = xp ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( ~ sQ54_spl
| sdtasdt0(xn,xn) = xp ),
inference(component_clause,[status(thm)],[f577]) ).
fof(f580,plain,
( ~ sQ21_spl
| sQ54_spl
| ~ sQ53_spl
| ~ sQ9_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f572,f267,f261,f574,f577,f332]) ).
fof(f596,plain,
( ~ sQ54_spl
| xn = xp
| xn = sz10
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f578,f184]) ).
fof(f597,plain,
( ~ sQ54_spl
| ~ aNaturalNumber0(xn)
| doDivides0(xn,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f578,f132]) ).
fof(f600,plain,
! [X0] :
( ~ sQ54_spl
| sdtasdt0(xp,X0) = sdtasdt0(xn,sdtasdt0(xn,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f578,f66]) ).
fof(f601,plain,
! [X0] :
( ~ sQ54_spl
| X0 != xp
| ~ aNaturalNumber0(xn)
| doDivides0(xn,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f578,f132]) ).
fof(f603,plain,
! [X0] :
( ~ sQ54_spl
| X0 = xn
| sdtasdt0(X0,xn) != xp
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0)
| xn = sz00
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f578,f81]) ).
fof(f605,plain,
! [X0] :
( ~ sQ54_spl
| X0 = xn
| sdtasdt0(xn,X0) != xp
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(X0)
| xn = sz00
| ~ aNaturalNumber0(xn) ),
inference(paramodulation,[status(thm)],[f578,f80]) ).
fof(f607,definition,
( sQ55_spl
<=> xn = sz10 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f608,plain,
( ~ sQ55_spl
| xn = sz10 ),
inference(component_clause,[status(thm)],[f607]) ).
fof(f610,definition,
( sQ56_spl
<=> xn = xp ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( ~ sQ56_spl
| xn = xp ),
inference(component_clause,[status(thm)],[f610]) ).
fof(f613,plain,
( ~ sQ54_spl
| sQ56_spl
| sQ55_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f596,f306,f607,f610,f577]) ).
fof(f614,definition,
( sQ57_spl
<=> doDivides0(xn,xp) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f615,plain,
( ~ sQ57_spl
| doDivides0(xn,xp) ),
inference(component_clause,[status(thm)],[f614]) ).
fof(f617,plain,
( ~ sQ54_spl
| sQ57_spl
| ~ sQ9_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f597,f306,f261,f614,f577]) ).
fof(f620,definition,
! [X0] :
( sQ58_spl
<=> ( sdtasdt0(xp,X0) = sdtasdt0(xn,sdtasdt0(xn,X0))
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( ~ sQ54_spl
| sQ58_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f600,f306,f620,f577]) ).
fof(f624,definition,
! [X0] :
( sQ59_spl
<=> ( X0 != xp
| doDivides0(xn,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( ~ sQ54_spl
| sQ59_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f601,f306,f624,f577]) ).
fof(f629,definition,
! [X0] :
( sQ60_spl
<=> ( X0 = xn
| sdtasdt0(X0,xn) != xp
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( ~ sQ54_spl
| sQ60_spl
| sQ29_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f603,f306,f413,f629,f577]) ).
fof(f634,definition,
! [X0] :
( sQ61_spl
<=> ( X0 = xn
| sdtasdt0(xn,X0) != xp
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( ~ sQ54_spl
| sQ61_spl
| sQ29_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f605,f306,f413,f634,f577]) ).
fof(f639,plain,
! [X0] :
( ~ sQ12_spl
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(sz10,X0)
| X0 = sz00
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f146,f284]) ).
fof(f645,definition,
! [X0] :
( sQ62_spl
<=> ( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sz10,X0)
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f648,plain,
( ~ sQ12_spl
| sQ62_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f639,f251,f645,f277]) ).
fof(f661,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| doDivides0(sz10,X1)
| ~ doDivides0(sz10,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f144,f284]) ).
fof(f665,definition,
! [X0,X1] :
( sQ65_spl
<=> ( ~ aNaturalNumber0(sdtpldt0(X0,X1))
| doDivides0(sz10,X1)
| ~ doDivides0(sz10,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( ~ sQ12_spl
| sQ65_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f661,f251,f665,f277]) ).
fof(f673,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X0,X0)
| X0 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(equality_resolution,[status(thm)],[f109]) ).
fof(f678,definition,
! [X0] :
( sQ66_spl
<=> ( ~ sdtlseqdt0(X0,X0)
| X0 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f681,plain,
( sQ18_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f673,f678,f321]) ).
fof(f687,plain,
( sQ53_spl
| sdtlseqdt0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f576,f107]) ).
fof(f688,plain,
! [X0] :
( sQ53_spl
| ~ sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(sdtasdt0(xn,xn),X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolution,[status(thm)],[f576,f104]) ).
fof(f689,plain,
( sQ53_spl
| sQ21_spl
| ~ sQ11_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f687,f261,f267,f332,f574]) ).
fof(f690,definition,
! [X0] :
( sQ67_spl
<=> ( ~ sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(sdtasdt0(xn,xn),X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f693,plain,
( sQ53_spl
| ~ sQ9_spl
| sQ67_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f688,f267,f690,f261,f574]) ).
fof(f714,plain,
( ~ sQ57_spl
| ~ sQ55_spl
| doDivides0(sz10,xp) ),
inference(forward_demodulation,[status(thm)],[f608,f615]) ).
fof(f716,plain,
( ~ sQ57_spl
| ~ sQ55_spl
| sdtlseqdt0(sz10,xp)
| xp = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f714,f146]) ).
fof(f717,plain,
! [X0] :
( ~ sQ57_spl
| ~ sQ55_spl
| doDivides0(X0,xp)
| ~ doDivides0(X0,sz10)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f714,f140]) ).
fof(f719,definition,
( sQ68_spl
<=> sdtlseqdt0(sz10,xp) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f720,plain,
( ~ sQ68_spl
| sdtlseqdt0(sz10,xp) ),
inference(component_clause,[status(thm)],[f719]) ).
fof(f722,plain,
( ~ sQ57_spl
| ~ sQ55_spl
| sQ68_spl
| sQ37_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f716,f251,f261,f460,f719,f607,f614]) ).
fof(f723,definition,
! [X0] :
( sQ69_spl
<=> ( doDivides0(X0,xp)
| ~ doDivides0(X0,sz10)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f726,plain,
( ~ sQ57_spl
| ~ sQ55_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f717,f723,f251,f261,f607,f614]) ).
fof(f743,plain,
( sQ2_spl
| ~ sQ56_spl
| ~ doDivides0(xn,xn) ),
inference(forward_demodulation,[status(thm)],[f611,f207]) ).
fof(f744,plain,
( ~ sQ7_spl
| sQ2_spl
| ~ sQ56_spl
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f743,f255]) ).
fof(f746,plain,
( ~ sQ7_spl
| sQ2_spl
| ~ sQ56_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f744,f306,f610,f205,f248]) ).
fof(f759,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X1,sz10)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X1)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f120,f104]) ).
fof(f760,plain,
! [X0] :
( X0 = sz10
| ~ sdtlseqdt0(X0,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f120,f102]) ).
fof(f761,definition,
! [X0,X1] :
( sQ71_spl
<=> ( sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X1,sz10)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f764,plain,
( ~ sQ8_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f759,f761,f251]) ).
fof(f765,definition,
! [X0] :
( sQ72_spl
<=> ( X0 = sz10
| ~ sdtlseqdt0(X0,sz10)
| ~ aNaturalNumber0(X0)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f768,plain,
( ~ sQ8_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f760,f765,f251]) ).
fof(f806,definition,
( sQ75_spl
<=> sdtlseqdt0(xp,xn) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f807,plain,
( ~ sQ75_spl
| sdtlseqdt0(xp,xn) ),
inference(component_clause,[status(thm)],[f806]) ).
fof(f810,definition,
! [X0] :
( sQ76_spl
<=> ( doDivides0(X0,xn)
| ~ doDivides0(X0,xp)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f811,plain,
! [X0] :
( ~ sQ76_spl
| doDivides0(X0,xn)
| ~ doDivides0(X0,xp)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f818,plain,
! [X0] :
( sK1_skl(sz00,X0) = sz00
| X0 = sz00
| ~ aNaturalNumber0(sK1_skl(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f131,f86]) ).
fof(f825,definition,
! [X0] :
( sQ77_spl
<=> ( sK1_skl(sz00,X0) = sz00
| X0 = sz00
| ~ aNaturalNumber0(sK1_skl(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sz00)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f828,plain,
( ~ sQ14_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f818,f825,f289]) ).
fof(f844,plain,
! [X0] :
( ~ sQ68_spl
| sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(X0,sz10)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f720,f104]) ).
fof(f845,plain,
( ~ sQ68_spl
| xp = sz10
| ~ sdtlseqdt0(xp,sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f720,f102]) ).
fof(f846,definition,
! [X0] :
( sQ78_spl
<=> ( sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(X0,sz10)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f849,plain,
( ~ sQ68_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f844,f846,f251,f261,f719]) ).
fof(f850,definition,
( sQ79_spl
<=> sdtlseqdt0(xp,sz10) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f852,plain,
( sQ79_spl
| ~ sdtlseqdt0(xp,sz10) ),
inference(component_clause,[status(thm)],[f850]) ).
fof(f853,plain,
( ~ sQ68_spl
| sQ38_spl
| ~ sQ79_spl
| ~ sQ8_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f845,f261,f251,f850,f465,f719]) ).
fof(f859,plain,
! [X0] :
( ~ sQ75_spl
| sdtlseqdt0(X0,xn)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f807,f104]) ).
fof(f860,plain,
( ~ sQ75_spl
| xn = xp
| ~ sdtlseqdt0(xn,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f807,f102]) ).
fof(f861,definition,
! [X0] :
( sQ80_spl
<=> ( sdtlseqdt0(X0,xn)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( ~ sQ75_spl
| ~ sQ17_spl
| ~ sQ9_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f859,f861,f261,f306,f806]) ).
fof(f865,definition,
( sQ81_spl
<=> sdtlseqdt0(xn,xp) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f867,plain,
( sQ81_spl
| ~ sdtlseqdt0(xn,xp) ),
inference(component_clause,[status(thm)],[f865]) ).
fof(f868,plain,
( ~ sQ75_spl
| sQ56_spl
| ~ sQ81_spl
| ~ sQ9_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f860,f306,f261,f865,f610,f806]) ).
fof(f870,plain,
! [X0] :
( ~ doDivides0(X0,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| X0 = xp
| X0 = sz10
| ~ aNaturalNumber0(sK1_skl(xp,X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f184,f131]) ).
fof(f872,definition,
! [X0] :
( sQ82_spl
<=> ( ~ doDivides0(X0,xp)
| ~ aNaturalNumber0(X0)
| X0 = xp
| X0 = sz10
| ~ aNaturalNumber0(sK1_skl(xp,X0))
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f875,plain,
( ~ sQ9_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f870,f872,f261]) ).
fof(f883,plain,
( sQ79_spl
| sdtlseqdt0(sz10,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f852,f107]) ).
fof(f884,plain,
! [X0] :
( sQ79_spl
| ~ sdtlseqdt0(X0,sz10)
| ~ sdtlseqdt0(xp,X0)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f852,f104]) ).
fof(f885,plain,
( sQ79_spl
| sQ68_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f883,f251,f261,f719,f850]) ).
fof(f886,definition,
! [X0] :
( sQ83_spl
<=> ( ~ sdtlseqdt0(X0,sz10)
| ~ sdtlseqdt0(xp,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f889,plain,
( sQ79_spl
| ~ sQ8_spl
| sQ83_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f884,f261,f886,f251,f850]) ).
fof(f890,plain,
( sQ81_spl
| sdtlseqdt0(xp,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f867,f107]) ).
fof(f891,plain,
! [X0] :
( sQ81_spl
| ~ sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f867,f104]) ).
fof(f892,plain,
( sQ81_spl
| sQ75_spl
| ~ sQ17_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f890,f261,f306,f806,f865]) ).
fof(f893,definition,
! [X0] :
( sQ84_spl
<=> ( ~ sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(xn,X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f896,plain,
( sQ81_spl
| ~ sQ9_spl
| sQ84_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f891,f306,f893,f261,f865]) ).
fof(f925,definition,
! [X0] :
( sQ85_spl
<=> ( ~ aNaturalNumber0(X0)
| sz10 = X0
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f926,plain,
! [X0] :
( ~ sQ85_spl
| ~ aNaturalNumber0(X0)
| sz10 = X0
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f925]) ).
fof(f940,plain,
! [X0] :
( ~ sQ85_spl
| sz10 = X0
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f926]) ).
fof(f941,plain,
! [X0] :
( ~ sQ85_spl
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f940,f153]) ).
fof(f944,plain,
( ~ sQ85_spl
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f941,f186]) ).
fof(f945,plain,
( ~ sQ85_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f944,f261,f925]) ).
fof(f955,plain,
( sQ81_spl
| ~ sQ55_spl
| ~ sdtlseqdt0(sz10,xp) ),
inference(backward_demodulation,[status(thm)],[f608,f867]) ).
fof(f964,plain,
( sQ81_spl
| ~ sQ55_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f955,f720]) ).
fof(f965,plain,
( sQ81_spl
| ~ sQ55_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f964]) ).
fof(f966,plain,
( sK2_skl(xp) = xp
| sK2_skl(xp) = sz10
| ~ aNaturalNumber0(sK2_skl(xp))
| xp = sz10
| xp = sz00
| isPrime0(xp)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f156,f185]) ).
fof(f970,definition,
( sQ89_spl
<=> isPrime0(xp) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f973,definition,
( sQ90_spl
<=> aNaturalNumber0(sK2_skl(xp)) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f975,plain,
( sQ90_spl
| ~ aNaturalNumber0(sK2_skl(xp)) ),
inference(component_clause,[status(thm)],[f973]) ).
fof(f976,definition,
( sQ91_spl
<=> sK2_skl(xp) = sz10 ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f977,plain,
( ~ sQ91_spl
| sK2_skl(xp) = sz10 ),
inference(component_clause,[status(thm)],[f976]) ).
fof(f979,definition,
( sQ92_spl
<=> sK2_skl(xp) = xp ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f980,plain,
( ~ sQ92_spl
| sK2_skl(xp) = xp ),
inference(component_clause,[status(thm)],[f979]) ).
fof(f982,plain,
( sQ92_spl
| sQ91_spl
| ~ sQ90_spl
| sQ38_spl
| sQ37_spl
| sQ89_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f966,f261,f970,f460,f465,f973,f976,f979]) ).
fof(f1014,plain,
( sK3_skl(xp) = xp
| sK3_skl(xp) = sz10
| ~ aNaturalNumber0(sK3_skl(xp))
| xp = sz10
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f162,f185]) ).
fof(f1018,definition,
( sQ95_spl
<=> aNaturalNumber0(sK3_skl(xp)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1020,plain,
( sQ95_spl
| ~ aNaturalNumber0(sK3_skl(xp)) ),
inference(component_clause,[status(thm)],[f1018]) ).
fof(f1021,definition,
( sQ96_spl
<=> sK3_skl(xp) = sz10 ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1022,plain,
( ~ sQ96_spl
| sK3_skl(xp) = sz10 ),
inference(component_clause,[status(thm)],[f1021]) ).
fof(f1024,definition,
( sQ97_spl
<=> sK3_skl(xp) = xp ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1025,plain,
( ~ sQ97_spl
| sK3_skl(xp) = xp ),
inference(component_clause,[status(thm)],[f1024]) ).
fof(f1027,plain,
( sQ97_spl
| sQ96_spl
| ~ sQ95_spl
| sQ38_spl
| sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1014,f261,f460,f465,f1018,f1021,f1024]) ).
fof(f1037,plain,
! [X0] :
( ~ sQ21_spl
| sdtlseqdt0(X0,sdtasdt0(xn,xn))
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f333,f104]) ).
fof(f1039,definition,
! [X0] :
( sQ98_spl
<=> ( sdtlseqdt0(X0,sdtasdt0(xn,xn))
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( ~ sQ21_spl
| ~ sQ11_spl
| ~ sQ9_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1037,f1039,f261,f267,f332]) ).
fof(f1044,plain,
( ~ sQ92_spl
| xp = sz10
| xp = sz00
| isPrime0(xp)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f980,f158]) ).
fof(f1049,plain,
( ~ sQ92_spl
| sQ38_spl
| sQ37_spl
| sQ89_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1044,f261,f970,f460,f465,f979]) ).
fof(f1052,definition,
( sQ99_spl
<=> doDivides0(xp,xp) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1053,plain,
( ~ sQ99_spl
| doDivides0(xp,xp) ),
inference(component_clause,[status(thm)],[f1052]) ).
fof(f1057,plain,
( ~ sQ91_spl
| xp = sz10
| xp = sz00
| isPrime0(xp)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f977,f157]) ).
fof(f1062,plain,
( ~ sQ91_spl
| sQ38_spl
| sQ37_spl
| sQ89_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1057,f261,f970,f460,f465,f976]) ).
fof(f1065,definition,
( sQ100_spl
<=> doDivides0(sz10,xp) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1066,plain,
( ~ sQ100_spl
| doDivides0(sz10,xp) ),
inference(component_clause,[status(thm)],[f1065]) ).
fof(f1080,plain,
( sQ90_spl
| xp = sz10
| xp = sz00
| isPrime0(xp)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f975,f155]) ).
fof(f1081,plain,
( sQ90_spl
| sQ38_spl
| sQ37_spl
| sQ89_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1080,f261,f970,f460,f465,f973]) ).
fof(f1082,plain,
( ~ sQ97_spl
| doDivides0(xp,xp)
| xp = sz10
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f1025,f162]) ).
fof(f1084,plain,
( ~ sQ97_spl
| sQ99_spl
| sQ38_spl
| sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1082,f261,f460,f465,f1052,f1024]) ).
fof(f1086,plain,
( ~ sQ96_spl
| doDivides0(sz10,xp)
| xp = sz10
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f1022,f162]) ).
fof(f1088,plain,
( ~ sQ96_spl
| sQ100_spl
| sQ38_spl
| sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1086,f261,f460,f465,f1065,f1021]) ).
fof(f1091,plain,
( ~ sQ4_spl
| doDivides0(xp,xn)
| doDivides0(xp,xn)
| ~ isPrime0(xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f165,f214]) ).
fof(f1093,plain,
! [X0,X1] :
( ~ sQ12_spl
| ~ aNaturalNumber0(sdtasdt0(X0,X1))
| doDivides0(sz10,X1)
| doDivides0(sz10,X0)
| ~ isPrime0(sz10)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f165,f284]) ).
fof(f1099,plain,
( ~ sQ4_spl
| sQ2_spl
| ~ sQ89_spl
| ~ sQ9_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1091,f306,f261,f970,f205,f213]) ).
fof(f1101,definition,
! [X0,X1] :
( sQ101_spl
<=> ( ~ aNaturalNumber0(sdtasdt0(X0,X1))
| doDivides0(sz10,X1)
| doDivides0(sz10,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1104,definition,
( sQ102_spl
<=> isPrime0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1107,plain,
( ~ sQ12_spl
| ~ sQ102_spl
| ~ sQ8_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1093,f1101,f251,f1104,f277]) ).
fof(f1131,plain,
( sQ95_spl
| xp = sz10
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f1020,f161]) ).
fof(f1132,plain,
( sQ95_spl
| sQ38_spl
| sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1131,f261,f460,f465,f1018]) ).
fof(f1140,plain,
( ~ sQ99_spl
| sdtlseqdt0(xp,xp)
| xp = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f1053,f146]) ).
fof(f1141,plain,
! [X0] :
( ~ sQ99_spl
| doDivides0(X0,xp)
| ~ doDivides0(X0,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f1053,f140]) ).
fof(f1143,definition,
( sQ104_spl
<=> sdtlseqdt0(xp,xp) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1144,plain,
( ~ sQ104_spl
| sdtlseqdt0(xp,xp) ),
inference(component_clause,[status(thm)],[f1143]) ).
fof(f1146,plain,
( ~ sQ99_spl
| sQ104_spl
| sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1140,f261,f460,f1143,f1052]) ).
fof(f1147,definition,
! [X0] :
( sQ105_spl
<=> ( doDivides0(X0,xp)
| ~ doDivides0(X0,xp)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( ~ sQ99_spl
| ~ sQ9_spl
| sQ105_spl ),
inference(split_clause,[status(thm)],[f1141,f1147,f261,f1052]) ).
fof(f1152,plain,
( ~ sQ100_spl
| sdtlseqdt0(sz10,xp)
| xp = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(resolution,[status(thm)],[f1066,f146]) ).
fof(f1153,plain,
! [X0] :
( ~ sQ100_spl
| doDivides0(X0,xp)
| ~ doDivides0(X0,sz10)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f1066,f140]) ).
fof(f1155,plain,
( ~ sQ100_spl
| sQ68_spl
| sQ37_spl
| ~ sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1152,f251,f261,f460,f719,f1065]) ).
fof(f1156,plain,
( ~ sQ100_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1153,f723,f251,f261,f1065]) ).
fof(f1157,plain,
( ~ sQ96_spl
| isPrime0(sz10)
| xp = sz10
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(paramodulation,[status(thm)],[f1022,f163]) ).
fof(f1160,plain,
( ~ sQ96_spl
| sQ102_spl
| sQ38_spl
| sQ37_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1157,f261,f460,f465,f1104,f1021]) ).
fof(f1177,plain,
! [X0,X1] :
( sK4_skl(xp,X1,X0) = xp
| sK4_skl(xp,X1,X0) = sz10
| ~ aNaturalNumber0(sK5_skl(xp,X1,X0))
| ~ aNaturalNumber0(sK4_skl(xp,X1,X0))
| xp = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(xp,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| xp = sz00
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f176,f184]) ).
fof(f1186,definition,
! [X0,X1] :
( sQ107_spl
<=> ( sK4_skl(xp,X1,X0) = xp
| sK4_skl(xp,X1,X0) = sz10
| ~ aNaturalNumber0(sK5_skl(xp,X1,X0))
| ~ aNaturalNumber0(sK4_skl(xp,X1,X0))
| ~ iLess0(X0,xn)
| sdtasdt0(xp,sdtasdt0(X1,X1)) != sdtasdt0(X0,X0)
| X1 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1189,plain,
( sQ38_spl
| sQ37_spl
| ~ sQ9_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1177,f1186,f261,f460,f465]) ).
fof(f1223,plain,
! [X0] :
( ~ sQ104_spl
| sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f1144,f104]) ).
fof(f1225,definition,
! [X0] :
( sQ110_spl
<=> ( sdtlseqdt0(X0,xp)
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1228,plain,
( ~ sQ104_spl
| ~ sQ9_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f1223,f1225,f261,f1143]) ).
fof(f1258,plain,
! [X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X0))
| ~ isPrime0(sz10)
| ~ iLess0(X0,xn)
| sz10 = sz00
| X0 = sz00
| X0 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f180,f69]) ).
fof(f1264,definition,
! [X0] :
( sQ112_spl
<=> ( ~ aNaturalNumber0(sdtasdt0(X0,X0))
| ~ iLess0(X0,xn)
| X0 = sz00
| X0 = sz00
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1267,plain,
( ~ sQ102_spl
| sQ52_spl
| ~ sQ8_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1258,f1264,f251,f560,f1104]) ).
fof(f1277,plain,
( ~ sQ7_spl
| ~ sQ76_spl
| ~ aNaturalNumber0(xp)
| doDivides0(xp,xn)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[status(thm)],[f811,f255]) ).
fof(f1293,plain,
( ~ sQ7_spl
| ~ sQ76_spl
| sQ2_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1277,f261,f205,f810,f248]) ).
fof(f1309,plain,
! [X0] :
( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,sz10))
| sz10 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sdtasdt0(X0,sz10)) ),
inference(resolution,[status(thm)],[f68,f81]) ).
fof(f1320,definition,
! [X0] :
( sQ117_spl
<=> ( sdtasdt0(X0,sz10) = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,sz10))
| ~ aNaturalNumber0(sdtasdt0(X0,sz10)) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1323,plain,
( sQ52_spl
| ~ sQ8_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f1309,f1320,f251,f560]) ).
fof(f1329,plain,
! [X0] :
( ~ aNaturalNumber0(sz00)
| ~ sdtlseqdt0(X0,sdtpldt0(sz00,X0))
| X0 = sdtpldt0(sz00,X0)
| ~ aNaturalNumber0(sdtpldt0(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sz00,X0)) ),
inference(resolution,[status(thm)],[f62,f109]) ).
fof(f1331,plain,
( sz00 = sz00
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sz00) ),
inference(resolution,[status(thm)],[f62,f84]) ).
fof(f1333,plain,
! [X0] :
( ~ aNaturalNumber0(sz00)
| ~ sdtlseqdt0(sdtpldt0(sz00,X0),X0)
| sdtpldt0(sz00,X0) = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sz00,X0))
| ~ aNaturalNumber0(sdtpldt0(sz00,X0)) ),
inference(resolution,[status(thm)],[f62,f109]) ).
fof(f1334,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f62,f92]) ).
fof(f1340,definition,
! [X0] :
( sQ118_spl
<=> ( ~ sdtlseqdt0(X0,sdtpldt0(sz00,X0))
| X0 = sdtpldt0(sz00,X0)
| ~ aNaturalNumber0(sdtpldt0(sz00,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sz00,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1343,plain,
( ~ sQ14_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1329,f1340,f289]) ).
fof(f1344,plain,
( sQ33_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1331,f289,f429]) ).
fof(f1346,definition,
! [X0] :
( sQ119_spl
<=> ( ~ sdtlseqdt0(sdtpldt0(sz00,X0),X0)
| sdtpldt0(sz00,X0) = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtpldt0(sz00,X0))
| ~ aNaturalNumber0(sdtpldt0(sz00,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1349,plain,
( ~ sQ14_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f1333,f1346,f289]) ).
fof(f1350,definition,
! [X0] :
( sQ120_spl
<=> ( ~ aNaturalNumber0(X0)
| sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1351,plain,
! [X0] :
( ~ sQ120_spl
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(component_clause,[status(thm)],[f1350]) ).
fof(f1353,plain,
( ~ sQ14_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f1334,f1350,f289]) ).
fof(f1357,plain,
! [X0] :
( ~ sQ120_spl
| sdtlseqdt0(sz00,X0)
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1351]) ).
fof(f1358,plain,
! [X0,X1] :
( ~ sQ120_spl
| sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X1,sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f1357,f104]) ).
fof(f1359,plain,
! [X0] :
( ~ sQ120_spl
| X0 = sz00
| ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f1357,f102]) ).
fof(f1360,definition,
! [X0,X1] :
( sQ121_spl
<=> ( sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X1,sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1363,plain,
( ~ sQ120_spl
| ~ sQ14_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f1358,f1360,f289,f1350]) ).
fof(f1364,definition,
! [X0] :
( sQ122_spl
<=> ( X0 = sz00
| ~ sdtlseqdt0(X0,sz00)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1367,plain,
( ~ sQ120_spl
| ~ sQ14_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f1359,f1364,f289,f1350]) ).
fof(f1376,plain,
( ~ aNaturalNumber0(xn)
| doDivides0(xn,sdtasdt0(xp,sdtasdt0(xm,xm)))
| ~ aNaturalNumber0(sdtasdt0(xp,sdtasdt0(xm,xm)))
| ~ aNaturalNumber0(xn) ),
inference(resolution,[status(thm)],[f181,f132]) ).
fof(f1377,plain,
( ~ sQ3_spl
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(resolution,[status(thm)],[f181,f210]) ).
fof(f1381,plain,
! [X0] :
( sK4_skl(xp,xm,X0) != xp
| xp = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| xp = sz00
| xm = sz00
| X0 = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0) ),
inference(paramodulation,[status(thm)],[f181,f179]) ).
fof(f1382,plain,
! [X0] :
( sK4_skl(xp,xm,X0) != sz10
| xp = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| xp = sz00
| xm = sz00
| X0 = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0) ),
inference(paramodulation,[status(thm)],[f181,f178]) ).
fof(f1383,plain,
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| doDivides0(sdtasdt0(xp,xm),sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xp,sdtasdt0(xm,xm))) ),
inference(paramodulation,[status(thm)],[f181,f237]) ).
fof(f1384,plain,
! [X0] :
( doDivides0(sK4_skl(xp,xm,X0),xp)
| xp = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| xp = sz00
| xm = sz00
| X0 = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0) ),
inference(paramodulation,[status(thm)],[f181,f177]) ).
fof(f1385,plain,
! [X0] :
( aNaturalNumber0(sK5_skl(xp,xm,X0))
| xp = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| xp = sz00
| xm = sz00
| X0 = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0) ),
inference(paramodulation,[status(thm)],[f181,f175]) ).
fof(f1386,plain,
! [X0] :
( aNaturalNumber0(sK4_skl(xp,xm,X0))
| xp = sz10
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| xp = sz00
| xm = sz00
| X0 = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0) ),
inference(paramodulation,[status(thm)],[f181,f174]) ).
fof(f1408,definition,
( sQ123_spl
<=> aNaturalNumber0(xm) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1410,plain,
( sQ123_spl
| ~ aNaturalNumber0(xm) ),
inference(component_clause,[status(thm)],[f1408]) ).
fof(f1411,definition,
( sQ124_spl
<=> xm = sz00 ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1412,plain,
( ~ sQ124_spl
| xm = sz00 ),
inference(component_clause,[status(thm)],[f1411]) ).
fof(f1438,definition,
( sQ131_spl
<=> aNaturalNumber0(sdtasdt0(xp,sdtasdt0(xm,xm))) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1440,plain,
( sQ131_spl
| ~ aNaturalNumber0(sdtasdt0(xp,sdtasdt0(xm,xm))) ),
inference(component_clause,[status(thm)],[f1438]) ).
fof(f1441,definition,
( sQ132_spl
<=> doDivides0(xn,sdtasdt0(xp,sdtasdt0(xm,xm))) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1444,plain,
( sQ132_spl
| ~ sQ131_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1376,f306,f1438,f1441]) ).
fof(f1457,definition,
! [X0] :
( sQ136_spl
<=> ( sK4_skl(xp,xm,X0) != xp
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1460,plain,
( sQ38_spl
| sQ37_spl
| sQ124_spl
| ~ sQ9_spl
| ~ sQ123_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f1381,f1457,f1408,f261,f1411,f460,f465]) ).
fof(f1461,definition,
! [X0] :
( sQ137_spl
<=> ( sK4_skl(xp,xm,X0) != sz10
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1464,plain,
( sQ38_spl
| sQ37_spl
| sQ124_spl
| ~ sQ9_spl
| ~ sQ123_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f1382,f1461,f1408,f261,f1411,f460,f465]) ).
fof(f1465,definition,
( sQ138_spl
<=> doDivides0(sdtasdt0(xp,xm),sdtasdt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1468,plain,
( ~ sQ9_spl
| ~ sQ123_spl
| sQ138_spl
| ~ sQ131_spl ),
inference(split_clause,[status(thm)],[f1383,f1438,f1465,f1408,f261]) ).
fof(f1469,definition,
! [X0] :
( sQ139_spl
<=> ( doDivides0(sK4_skl(xp,xm,X0),xp)
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1472,plain,
( sQ38_spl
| sQ37_spl
| sQ124_spl
| ~ sQ9_spl
| ~ sQ123_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f1384,f1469,f1408,f261,f1411,f460,f465]) ).
fof(f1473,definition,
! [X0] :
( sQ140_spl
<=> ( aNaturalNumber0(sK5_skl(xp,xm,X0))
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f1476,plain,
( sQ38_spl
| sQ37_spl
| sQ124_spl
| ~ sQ9_spl
| ~ sQ123_spl
| sQ140_spl ),
inference(split_clause,[status(thm)],[f1385,f1473,f1408,f261,f1411,f460,f465]) ).
fof(f1477,definition,
! [X0] :
( sQ141_spl
<=> ( aNaturalNumber0(sK4_skl(xp,xm,X0))
| ~ iLess0(X0,xn)
| sdtasdt0(xn,xn) != sdtasdt0(X0,X0)
| X0 = sz00
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1480,plain,
( sQ38_spl
| sQ37_spl
| sQ124_spl
| ~ sQ9_spl
| ~ sQ123_spl
| sQ141_spl ),
inference(split_clause,[status(thm)],[f1386,f1477,f1408,f261,f1411,f460,f465]) ).
fof(f1544,plain,
( sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1410,f167]) ).
fof(f1545,plain,
sQ123_spl,
inference(contradiction_clause,[status(thm)],[f1544]) ).
fof(f1546,plain,
( sQ131_spl
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(forward_demodulation,[status(thm)],[f181,f1440]) ).
fof(f1547,plain,
( sQ131_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1546,f268]) ).
fof(f1548,plain,
( sQ131_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f1547]) ).
fof(f1549,plain,
( ~ sQ124_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1412,f170]) ).
fof(f1550,plain,
~ sQ124_spl,
inference(contradiction_clause,[status(thm)],[f1549]) ).
fof(f1564,plain,
( ~ sQ3_spl
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[status(thm)],[f1377,f55]) ).
fof(f1565,plain,
( ~ sQ3_spl
| ~ sQ123_spl ),
inference(split_clause,[status(thm)],[f1564,f1408,f209]) ).
fof(f1566,plain,
$false,
inference(sat_refutation,[status(thm)],[f204,f208,f212,f220,f224,f254,f280,f283,f292,f295,f303,f309,f311,f313,f319,f327,f335,f341,f358,f374,f385,f393,f397,f416,f444,f449,f463,f468,f497,f542,f546,f563,f564,f570,f580,f613,f617,f623,f627,f632,f637,f648,f668,f681,f689,f693,f722,f726,f746,f764,f768,f828,f849,f853,f864,f868,f875,f885,f889,f892,f896,f945,f965,f982,f1027,f1042,f1049,f1062,f1081,f1084,f1088,f1099,f1107,f1132,f1146,f1150,f1155,f1156,f1160,f1189,f1228,f1267,f1293,f1323,f1343,f1344,f1349,f1353,f1363,f1367,f1444,f1460,f1464,f1468,f1472,f1476,f1480,f1545,f1548,f1550,f1565]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM523+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 02:37:06 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.06/0.39 % Refutation found
% 0.06/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.06/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.06/0.41 % Elapsed time: 0.118057 seconds
% 0.06/0.41 % CPU time: 0.668998 seconds
% 0.06/0.41 % Total memory used: 119.514 MB
% 0.06/0.41 % Net memory used: 117.872 MB
%------------------------------------------------------------------------------