%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV486+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 : n018.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:48:02 PM UTC 2026
% Result : Theorem 0.67s 1.29s
% Output : CNFRefutation 0.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 58
% Syntax : Number of formulae : 281 ( 46 unt; 46 def)
% Number of atoms : 706 ( 114 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 729 ( 304 ~; 328 |; 37 &)
% ( 49 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 47 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 184 ( 179 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [I,J] :
( int_leq(I,J)
<=> ( I = J
| int_less(I,J) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,K] :
( ( int_less(J,K)
& int_less(I,J) )
=> int_less(I,K) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [I,J] :
( int_less(I,J)
=> I != J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [I,J] :
( int_leq(J,I)
| int_less(I,J) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
int_less(int_zero,int_one),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [I,J] : plus(I,J) = plus(J,I),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [I] : plus(I,int_zero) = I,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [I1,J1,I2,J2] :
( ( int_leq(I2,J2)
& int_less(I1,J1) )
=> int_leq(plus(I1,I2),plus(J1,J2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [I,J] :
( int_less(I,J)
<=> ? [K] :
( int_less(int_zero,K)
& plus(I,K) = J ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [I] :
( int_less(int_zero,I)
<=> int_leq(int_one,I) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
! [I,J] :
( ( int_leq(J,n)
& int_leq(int_one,J)
& int_leq(I,n)
& int_leq(int_one,I) )
=> ( ! [C] :
( ( J = plus(I,C)
& int_less(int_zero,C) )
=> ! [K] :
( ( int_leq(K,I)
& int_leq(int_one,K) )
=> a(K,plus(K,C)) = real_zero ) )
& ! [K] :
( ( int_leq(K,J)
& int_leq(int_one,K) )
=> a(K,K) = real_one )
& ! [C] :
( ( I = plus(J,C)
& int_less(int_zero,C) )
=> ! [K] :
( ( int_leq(K,J)
& int_leq(int_one,K) )
=> a(plus(K,C),K) = real_zero ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,conjecture,
! [I,J] :
( ( int_leq(J,n)
& int_less(I,J)
& int_leq(int_one,I) )
=> a(I,J) = real_zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
~ ! [I,J] :
( ( int_leq(J,n)
& int_less(I,J)
& int_leq(int_one,I) )
=> a(I,J) = real_zero ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f15,plain,
! [I,J] :
( ( ( I != J
& ~ int_less(I,J) )
| int_leq(I,J) )
& ( I = J
| int_less(I,J)
| ~ int_leq(I,J) ) ),
inference(NNF_transformation,[status(thm)],[f1]) ).
fof(f16,plain,
( ! [I,J] :
( ( I != J
& ~ int_less(I,J) )
| int_leq(I,J) )
& ! [I,J] :
( I = J
| int_less(I,J)
| ~ int_leq(I,J) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f17,plain,
! [X0,X1] :
( X0 = X1
| int_less(X0,X1)
| ~ int_leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f19,plain,
! [X0,X1] :
( X0 != X1
| int_leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f20,plain,
! [I,J,K] :
( int_less(I,K)
| ~ int_less(J,K)
| ~ int_less(I,J) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f21,plain,
! [I,K] :
( int_less(I,K)
| ! [J] :
( ~ int_less(J,K)
| ~ int_less(I,J) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f22,plain,
! [X0,X1,X2] :
( int_less(X0,X2)
| ~ int_less(X1,X2)
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f23,plain,
! [I,J] :
( I != J
| ~ int_less(I,J) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f24,plain,
! [X0,X1] :
( X0 != X1
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f25,plain,
! [X0,X1] :
( int_leq(X1,X0)
| int_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f26,plain,
int_less(int_zero,int_one),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f27,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f28,plain,
! [X0] : plus(X0,int_zero) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f29,plain,
! [I1,J1,I2,J2] :
( int_leq(plus(I1,I2),plus(J1,J2))
| ~ int_leq(I2,J2)
| ~ int_less(I1,J1) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( int_leq(plus(X0,X2),plus(X1,X3))
| ~ int_leq(X2,X3)
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
! [I,J] :
( ( ! [K] :
( ~ int_less(int_zero,K)
| plus(I,K) != J )
| int_less(I,J) )
& ( ? [K] :
( int_less(int_zero,K)
& plus(I,K) = J )
| ~ int_less(I,J) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f32,plain,
( ! [I,J] :
( ! [K] :
( ~ int_less(int_zero,K)
| plus(I,K) != J )
| int_less(I,J) )
& ! [I,J] :
( ? [K] :
( int_less(int_zero,K)
& plus(I,K) = J )
| ~ int_less(I,J) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f33,plain,
( ! [I,J] :
( ! [K] :
( ~ int_less(int_zero,K)
| plus(I,K) != J )
| int_less(I,J) )
& ! [I,J] :
( ( int_less(int_zero,sK0_skl(J,I))
& plus(I,sK0_skl(J,I)) = J )
| ~ int_less(I,J) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(K,sK0_skl(J,I))],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( plus(X0,sK0_skl(X1,X0)) = X1
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [X0,X1] :
( int_less(int_zero,sK0_skl(X1,X0))
| ~ int_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ~ int_less(int_zero,X2)
| plus(X0,X2) != X1
| int_less(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f37,plain,
! [I] :
( ( ~ int_leq(int_one,I)
| int_less(int_zero,I) )
& ( int_leq(int_one,I)
| ~ int_less(int_zero,I) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f38,plain,
( ! [I] :
( ~ int_leq(int_one,I)
| int_less(int_zero,I) )
& ! [I] :
( int_leq(int_one,I)
| ~ int_less(int_zero,I) ) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f39,plain,
! [X0] :
( int_leq(int_one,X0)
| ~ int_less(int_zero,X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0] :
( ~ int_leq(int_one,X0)
| int_less(int_zero,X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f42,plain,
! [I,J] :
( ( ! [C] :
( ! [K] :
( a(K,plus(K,C)) = real_zero
| ~ int_leq(K,I)
| ~ int_leq(int_one,K) )
| J != plus(I,C)
| ~ int_less(int_zero,C) )
& ! [K] :
( a(K,K) = real_one
| ~ int_leq(K,J)
| ~ int_leq(int_one,K) )
& ! [C] :
( ! [K] :
( a(plus(K,C),K) = real_zero
| ~ int_leq(K,J)
| ~ int_leq(int_one,K) )
| I != plus(J,C)
| ~ int_less(int_zero,C) ) )
| ~ int_leq(J,n)
| ~ int_leq(int_one,J)
| ~ int_leq(I,n)
| ~ int_leq(int_one,I) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( a(plus(X3,X2),X3) = real_zero
| ~ int_leq(X3,X1)
| ~ int_leq(int_one,X3)
| X0 != plus(X1,X2)
| ~ int_less(int_zero,X2)
| ~ int_leq(X1,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f45,plain,
! [X0,X1,X2,X3] :
( a(X3,plus(X3,X2)) = real_zero
| ~ int_leq(X3,X0)
| ~ int_leq(int_one,X3)
| X1 != plus(X0,X2)
| ~ int_less(int_zero,X2)
| ~ int_leq(X1,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f46,plain,
? [I,J] :
( a(I,J) != real_zero
& int_leq(J,n)
& int_less(I,J)
& int_leq(int_one,I) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f47,plain,
( a(sK1_skl,sK2_skl) != real_zero
& int_leq(sK2_skl,n)
& int_less(sK1_skl,sK2_skl)
& int_leq(int_one,sK1_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(I,sK1_skl),skolemize(J,sK2_skl)],[f46]) ).
fof(f48,plain,
int_leq(int_one,sK1_skl),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
int_less(sK1_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f50,plain,
int_leq(sK2_skl,n),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f51,plain,
a(sK1_skl,sK2_skl) != real_zero,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f59,plain,
! [X0] : int_leq(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f19]) ).
fof(f60,plain,
! [X0] : ~ int_less(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f24]) ).
fof(f61,plain,
! [X0,X1] :
( ~ int_less(int_zero,X1)
| int_less(X0,plus(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f36]) ).
fof(f62,plain,
! [X0,X1,X2] :
( a(plus(X2,X1),X2) = real_zero
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_less(int_zero,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,X1),n)
| ~ int_leq(int_one,plus(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f43]) ).
fof(f63,plain,
! [X0,X1,X2] :
( a(X2,plus(X2,X1)) = real_zero
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_less(int_zero,X1)
| ~ int_leq(plus(X0,X1),n)
| ~ int_leq(int_one,plus(X0,X1))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f45]) ).
fof(f65,plain,
! [X0,X1] :
( ~ int_less(X1,X0)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f22,f60]) ).
fof(f66,plain,
~ int_less(sK2_skl,sK1_skl),
inference(resolution,[status(thm)],[f65,f49]) ).
fof(f68,plain,
! [X0,X1] :
( X1 = X0
| ~ int_leq(X1,X0)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f65,f17]) ).
fof(f69,plain,
! [X0] :
( ~ int_less(X0,sK1_skl)
| ~ int_less(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f66,f22]) ).
fof(f96,definition,
( sQ6_spl
<=> int_leq(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f98,plain,
( sQ6_spl
| ~ int_leq(int_one,int_zero) ),
inference(component_clause,[status(thm)],[f96]) ).
fof(f99,definition,
( sQ7_spl
<=> int_one = int_zero ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f100,plain,
( ~ sQ7_spl
| int_one = int_zero ),
inference(component_clause,[status(thm)],[f99]) ).
fof(f101,plain,
( sQ7_spl
| int_one != int_zero ),
inference(component_clause,[status(thm)],[f99]) ).
fof(f105,plain,
! [X0] : X0 = plus(int_zero,X0),
inference(paramodulation,[status(thm)],[f28,f27]) ).
fof(f134,plain,
! [X0] :
( ~ int_less(X0,int_zero)
| ~ int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f40,f65]) ).
fof(f136,plain,
! [X0,X1] :
( int_leq(plus(int_zero,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f30,f26]) ).
fof(f140,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ int_leq(X2,X3)
| int_leq(plus(X2,X0),plus(X3,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f30,f17]) ).
fof(f141,plain,
! [X0,X1] :
( int_leq(X0,plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f105,f136]) ).
fof(f143,plain,
plus(int_zero,sK0_skl(int_one,int_zero)) = int_one,
inference(resolution,[status(thm)],[f34,f26]) ).
fof(f144,plain,
! [X0] :
( ~ int_leq(int_one,X0)
| plus(int_zero,sK0_skl(X0,int_zero)) = X0 ),
inference(resolution,[status(thm)],[f34,f40]) ).
fof(f145,plain,
plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl,
inference(resolution,[status(thm)],[f34,f49]) ).
fof(f147,plain,
! [X0,X1] :
( X0 = X1
| ~ int_leq(X0,X1)
| plus(X0,sK0_skl(X1,X0)) = X1 ),
inference(resolution,[status(thm)],[f34,f17]) ).
fof(f148,plain,
sK0_skl(int_one,int_zero) = int_one,
inference(forward_demodulation,[status(thm)],[f105,f143]) ).
fof(f149,plain,
! [X0] :
( ~ int_leq(int_one,X0)
| sK0_skl(X0,int_zero) = X0 ),
inference(forward_demodulation,[status(thm)],[f105,f144]) ).
fof(f150,plain,
! [X0,X1] :
( plus(int_zero,sK0_skl(sK0_skl(X1,X0),int_zero)) = sK0_skl(X1,X0)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f35,f34]) ).
fof(f152,plain,
! [X0,X1] :
( ~ int_less(sK0_skl(X1,X0),int_zero)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f35,f65]) ).
fof(f153,plain,
! [X0,X1] :
( sK0_skl(sK0_skl(X1,X0),int_zero) = sK0_skl(X1,X0)
| ~ int_less(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f105,f150]) ).
fof(f157,plain,
! [X0] :
( a(sK1_skl,sK2_skl) = real_zero
| ~ int_leq(sK1_skl,X0)
| ~ int_leq(int_one,sK1_skl)
| ~ int_less(int_zero,sK0_skl(sK2_skl,sK1_skl))
| ~ int_leq(plus(X0,sK0_skl(sK2_skl,sK1_skl)),n)
| ~ int_leq(int_one,plus(X0,sK0_skl(sK2_skl,sK1_skl)))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(paramodulation,[status(thm)],[f145,f63]) ).
fof(f159,definition,
! [X0] :
( sQ10_spl
<=> ( ~ int_leq(sK1_skl,X0)
| ~ int_leq(plus(X0,sK0_skl(sK2_skl,sK1_skl)),n)
| ~ int_leq(int_one,plus(X0,sK0_skl(sK2_skl,sK1_skl)))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f160,plain,
! [X0] :
( ~ sQ10_spl
| ~ int_leq(sK1_skl,X0)
| ~ int_leq(plus(X0,sK0_skl(sK2_skl,sK1_skl)),n)
| ~ int_leq(int_one,plus(X0,sK0_skl(sK2_skl,sK1_skl)))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(component_clause,[status(thm)],[f159]) ).
fof(f162,definition,
( sQ11_spl
<=> int_less(int_zero,sK0_skl(sK2_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( sQ11_spl
| ~ int_less(int_zero,sK0_skl(sK2_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f165,definition,
( sQ12_spl
<=> int_leq(int_one,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f167,plain,
( sQ12_spl
| ~ int_leq(int_one,sK1_skl) ),
inference(component_clause,[status(thm)],[f165]) ).
fof(f168,definition,
( sQ13_spl
<=> a(sK1_skl,sK2_skl) = real_zero ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f169,plain,
( ~ sQ13_spl
| a(sK1_skl,sK2_skl) = real_zero ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,plain,
( sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f157,f159,f162,f165,f168]) ).
fof(f176,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f167,f48]) ).
fof(f177,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f176]) ).
fof(f178,plain,
( sQ11_spl
| ~ int_less(sK1_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f164,f35]) ).
fof(f182,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f178,f49]) ).
fof(f183,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f182]) ).
fof(f195,plain,
( sK2_skl = n
| ~ int_less(n,sK2_skl) ),
inference(resolution,[status(thm)],[f68,f50]) ).
fof(f196,plain,
( int_one = sK1_skl
| ~ int_less(sK1_skl,int_one) ),
inference(resolution,[status(thm)],[f68,f48]) ).
fof(f201,definition,
( sQ15_spl
<=> int_less(n,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f203,plain,
( sQ15_spl
| ~ int_less(n,sK2_skl) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,definition,
( sQ16_spl
<=> sK2_skl = n ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f205,plain,
( ~ sQ16_spl
| sK2_skl = n ),
inference(component_clause,[status(thm)],[f204]) ).
fof(f207,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f195,f201,f204]) ).
fof(f208,definition,
( sQ17_spl
<=> int_less(sK1_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f210,plain,
( sQ17_spl
| ~ int_less(sK1_skl,int_one) ),
inference(component_clause,[status(thm)],[f208]) ).
fof(f211,definition,
( sQ18_spl
<=> int_one = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f212,plain,
( ~ sQ18_spl
| int_one = sK1_skl ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,plain,
( sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f196,f208,f211]) ).
fof(f216,plain,
( sQ17_spl
| sK1_skl = int_one
| ~ int_leq(sK1_skl,int_one) ),
inference(resolution,[status(thm)],[f210,f17]) ).
fof(f217,definition,
( sQ19_spl
<=> int_leq(sK1_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f219,plain,
( sQ19_spl
| ~ int_leq(sK1_skl,int_one) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f220,plain,
( sQ17_spl
| sQ18_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f216,f217,f211,f208]) ).
fof(f226,plain,
( ~ sQ18_spl
| ~ int_less(sK2_skl,int_one) ),
inference(backward_demodulation,[status(thm)],[f212,f66]) ).
fof(f231,plain,
! [X0] :
( sQ15_spl
| ~ int_less(X0,sK2_skl)
| ~ int_less(n,X0) ),
inference(resolution,[status(thm)],[f203,f22]) ).
fof(f257,definition,
( sQ23_spl
<=> int_less(int_zero,int_one) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f259,plain,
( sQ23_spl
| ~ int_less(int_zero,int_one) ),
inference(component_clause,[status(thm)],[f257]) ).
fof(f280,plain,
( sQ19_spl
| int_less(int_one,sK1_skl) ),
inference(resolution,[status(thm)],[f219,f25]) ).
fof(f292,plain,
! [X0,X1] :
( int_zero = X1
| ~ int_leq(int_zero,X1)
| int_less(X0,plus(X0,X1)) ),
inference(resolution,[status(thm)],[f61,f17]) ).
fof(f341,plain,
! [X0,X1,X2] :
( int_zero = X1
| ~ int_leq(int_zero,X1)
| a(plus(X2,X1),X2) = real_zero
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,X1),n)
| ~ int_leq(int_one,plus(X0,X1)) ),
inference(resolution,[status(thm)],[f62,f17]) ).
fof(f379,plain,
int_less(int_zero,sK1_skl),
inference(resolution,[status(thm)],[f40,f48]) ).
fof(f396,plain,
~ int_less(sK1_skl,int_zero),
inference(resolution,[status(thm)],[f379,f65]) ).
fof(f402,plain,
( sK1_skl = int_zero
| ~ int_leq(sK1_skl,int_zero) ),
inference(resolution,[status(thm)],[f396,f17]) ).
fof(f403,definition,
( sQ27_spl
<=> int_leq(sK1_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f406,definition,
( sQ28_spl
<=> sK1_skl = int_zero ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f407,plain,
( ~ sQ28_spl
| sK1_skl = int_zero ),
inference(component_clause,[status(thm)],[f406]) ).
fof(f409,plain,
( sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f402,f403,f406]) ).
fof(f415,definition,
( sQ29_spl
<=> int_leq(sK1_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ29_spl
| ~ int_leq(sK1_skl,n) ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f438,definition,
( sQ31_spl
<=> int_less(int_zero,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( sQ31_spl
| ~ int_less(int_zero,sK1_skl) ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f495,plain,
! [X0] : int_leq(X0,plus(int_one,X0)),
inference(resolution,[status(thm)],[f141,f59]) ).
fof(f500,plain,
( sQ15_spl
| ~ int_less(n,sK1_skl) ),
inference(resolution,[status(thm)],[f231,f49]) ).
fof(f529,plain,
( ~ sQ28_spl
| int_leq(int_one,int_zero) ),
inference(forward_demodulation,[status(thm)],[f407,f48]) ).
fof(f530,plain,
( ~ sQ28_spl
| sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f98]) ).
fof(f531,plain,
( ~ sQ28_spl
| sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f530]) ).
fof(f596,plain,
~ int_less(sK2_skl,sK1_skl),
inference(resolution,[status(thm)],[f49,f65]) ).
fof(f702,plain,
( ~ sQ16_spl
| ~ int_less(n,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f205,f596]) ).
fof(f716,plain,
( sQ29_spl
| int_less(n,sK1_skl) ),
inference(resolution,[status(thm)],[f417,f25]) ).
fof(f718,plain,
( sQ29_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f716,f702]) ).
fof(f719,plain,
( sQ29_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f718]) ).
fof(f839,plain,
int_leq(int_zero,int_one),
inference(paramodulation,[status(thm)],[f28,f495]) ).
fof(f840,plain,
! [X0] : int_leq(X0,plus(X0,int_one)),
inference(paramodulation,[status(thm)],[f27,f495]) ).
fof(f843,plain,
( int_zero = int_one
| ~ int_less(int_one,int_zero) ),
inference(resolution,[status(thm)],[f839,f68]) ).
fof(f845,definition,
( sQ41_spl
<=> int_less(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f848,plain,
( sQ7_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f843,f845,f99]) ).
fof(f878,plain,
! [X0,X1] :
( int_zero = int_one
| int_leq(plus(int_zero,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f140,f839]) ).
fof(f887,definition,
! [X0,X1] :
( sQ42_spl
<=> ( int_leq(plus(int_zero,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f890,plain,
( sQ7_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f878,f887,f99]) ).
fof(f916,plain,
( ~ sQ7_spl
| int_less(int_one,int_one) ),
inference(backward_demodulation,[status(thm)],[f100,f26]) ).
fof(f1007,plain,
plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl,
inference(resolution,[status(thm)],[f49,f34]) ).
fof(f1059,plain,
! [X0] :
( int_zero = X0
| ~ int_leq(int_zero,X0)
| int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f39,f17]) ).
fof(f1067,plain,
int_less(int_zero,sK1_skl),
inference(resolution,[status(thm)],[f48,f40]) ).
fof(f1109,definition,
( sQ50_spl
<=> int_leq(int_one,int_one) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1111,plain,
( sQ50_spl
| ~ int_leq(int_one,int_one) ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1174,definition,
( sQ53_spl
<=> int_leq(int_one,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1175,plain,
( ~ sQ53_spl
| int_leq(int_one,sK2_skl) ),
inference(component_clause,[status(thm)],[f1174]) ).
fof(f1176,plain,
( sQ53_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(component_clause,[status(thm)],[f1174]) ).
fof(f1242,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1111,f59]) ).
fof(f1243,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f1242]) ).
fof(f1311,plain,
( sQ29_spl
| sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f716,f500]) ).
fof(f1312,plain,
( sQ29_spl
| sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f1311]) ).
fof(f1356,plain,
plus(int_zero,sK0_skl(sK1_skl,int_zero)) = sK1_skl,
inference(resolution,[status(thm)],[f1067,f34]) ).
fof(f1359,plain,
sK0_skl(sK1_skl,int_zero) = sK1_skl,
inference(forward_demodulation,[status(thm)],[f105,f1356]) ).
fof(f1454,plain,
( int_zero = int_one
| plus(int_zero,sK0_skl(int_one,int_zero)) = int_one ),
inference(resolution,[status(thm)],[f147,f839]) ).
fof(f1471,definition,
( sQ60_spl
<=> plus(int_zero,sK0_skl(int_one,int_zero)) = int_one ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1474,plain,
( sQ7_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f1454,f1471,f99]) ).
fof(f1479,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f916,f60]) ).
fof(f1480,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1479]) ).
fof(f1586,plain,
( sK0_skl(int_one,int_zero) = sK0_skl(int_one,int_zero)
| ~ int_less(int_zero,int_one) ),
inference(paramodulation,[status(thm)],[f148,f153]) ).
fof(f1587,definition,
( sQ62_spl
<=> sK0_skl(int_one,int_zero) = sK0_skl(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1590,plain,
( sQ62_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f1586,f257,f1587]) ).
fof(f1591,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f259,f26]) ).
fof(f1592,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1591]) ).
fof(f1639,plain,
! [X0] :
( int_zero = int_one
| int_less(X0,plus(X0,int_one)) ),
inference(resolution,[status(thm)],[f292,f839]) ).
fof(f1640,plain,
! [X0] :
( int_zero = plus(int_one,int_zero)
| int_less(X0,plus(X0,plus(int_one,int_zero))) ),
inference(resolution,[status(thm)],[f292,f495]) ).
fof(f1641,plain,
! [X0] :
( int_zero = plus(int_zero,int_one)
| int_less(X0,plus(X0,plus(int_zero,int_one))) ),
inference(resolution,[status(thm)],[f292,f840]) ).
fof(f1644,plain,
! [X0] :
( int_zero = int_zero
| int_less(X0,plus(X0,int_zero)) ),
inference(resolution,[status(thm)],[f292,f59]) ).
fof(f1645,definition,
! [X0] :
( sQ65_spl
<=> int_less(X0,plus(X0,int_one)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1648,plain,
( sQ7_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1639,f1645,f99]) ).
fof(f1649,definition,
! [X0] :
( sQ66_spl
<=> int_less(X0,plus(X0,plus(int_one,int_zero))) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1652,definition,
( sQ67_spl
<=> int_zero = plus(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1653,plain,
( ~ sQ67_spl
| int_zero = plus(int_one,int_zero) ),
inference(component_clause,[status(thm)],[f1652]) ).
fof(f1655,plain,
( sQ67_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f1640,f1649,f1652]) ).
fof(f1656,definition,
! [X0] :
( sQ68_spl
<=> int_less(X0,plus(X0,plus(int_zero,int_one))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1659,definition,
( sQ69_spl
<=> int_zero = plus(int_zero,int_one) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1660,plain,
( ~ sQ69_spl
| int_zero = plus(int_zero,int_one) ),
inference(component_clause,[status(thm)],[f1659]) ).
fof(f1662,plain,
( sQ69_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f1641,f1656,f1659]) ).
fof(f1663,definition,
! [X0] :
( sQ70_spl
<=> int_less(X0,plus(X0,int_zero)) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1664,plain,
! [X0] :
( ~ sQ70_spl
| int_less(X0,plus(X0,int_zero)) ),
inference(component_clause,[status(thm)],[f1663]) ).
fof(f1666,definition,
( sQ71_spl
<=> int_zero = int_zero ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1669,plain,
( sQ71_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1644,f1663,f1666]) ).
fof(f1670,plain,
! [X0] :
( ~ sQ70_spl
| int_less(X0,X0) ),
inference(forward_demodulation,[status(thm)],[f28,f1664]) ).
fof(f1671,plain,
( ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1670,f60]) ).
fof(f1672,plain,
~ sQ70_spl,
inference(contradiction_clause,[status(thm)],[f1671]) ).
fof(f1844,plain,
( sQ53_spl
| int_less(sK2_skl,int_one) ),
inference(resolution,[status(thm)],[f1176,f25]) ).
fof(f1846,plain,
( sQ53_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1844,f226]) ).
fof(f1847,plain,
( sQ53_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f1846]) ).
fof(f1862,definition,
( sQ89_spl
<=> int_less(sK2_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1864,plain,
( sQ89_spl
| ~ int_less(sK2_skl,int_one) ),
inference(component_clause,[status(thm)],[f1862]) ).
fof(f1935,definition,
( sQ90_spl
<=> int_less(int_zero,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1936,plain,
( ~ sQ90_spl
| int_less(int_zero,sK2_skl) ),
inference(component_clause,[status(thm)],[f1935]) ).
fof(f1937,plain,
( sQ90_spl
| ~ int_less(int_zero,sK2_skl) ),
inference(component_clause,[status(thm)],[f1935]) ).
fof(f1943,plain,
( sQ90_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(resolution,[status(thm)],[f1937,f40]) ).
fof(f1945,plain,
( sQ90_spl
| int_zero = sK2_skl
| ~ int_leq(int_zero,sK2_skl) ),
inference(resolution,[status(thm)],[f1937,f17]) ).
fof(f1946,plain,
( sQ90_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f1943,f1174,f1935]) ).
fof(f1947,definition,
( sQ92_spl
<=> int_leq(int_zero,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1949,plain,
( sQ92_spl
| ~ int_leq(int_zero,sK2_skl) ),
inference(component_clause,[status(thm)],[f1947]) ).
fof(f1950,definition,
( sQ93_spl
<=> int_zero = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1951,plain,
( ~ sQ93_spl
| int_zero = sK2_skl ),
inference(component_clause,[status(thm)],[f1950]) ).
fof(f1953,plain,
( sQ90_spl
| sQ93_spl
| ~ sQ92_spl ),
inference(split_clause,[status(thm)],[f1945,f1947,f1950,f1935]) ).
fof(f2016,plain,
( ~ sQ90_spl
| ~ sQ93_spl
| int_less(int_zero,int_zero) ),
inference(backward_demodulation,[status(thm)],[f1951,f1936]) ).
fof(f2027,plain,
( sQ89_spl
| ~ sQ93_spl
| ~ int_less(int_zero,int_one) ),
inference(backward_demodulation,[status(thm)],[f1951,f1864]) ).
fof(f2030,plain,
( ~ sQ90_spl
| ~ sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2016,f60]) ).
fof(f2031,plain,
( ~ sQ90_spl
| ~ sQ93_spl ),
inference(contradiction_clause,[status(thm)],[f2030]) ).
fof(f2098,definition,
( sQ102_spl
<=> int_leq(sK2_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2100,plain,
( sQ102_spl
| ~ int_leq(sK2_skl,n) ),
inference(component_clause,[status(thm)],[f2098]) ).
fof(f2126,plain,
! [X0,X1] :
( int_zero = int_one
| a(plus(X1,int_one),X1) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,int_one),n)
| ~ int_leq(int_one,plus(X0,int_one)) ),
inference(resolution,[status(thm)],[f341,f839]) ).
fof(f2127,plain,
! [X0,X1] :
( int_zero = plus(int_one,int_zero)
| a(plus(X1,plus(int_one,int_zero)),X1) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,plus(int_one,int_zero)),n)
| ~ int_leq(int_one,plus(X0,plus(int_one,int_zero))) ),
inference(resolution,[status(thm)],[f341,f495]) ).
fof(f2128,plain,
! [X0,X1] :
( int_zero = plus(int_zero,int_one)
| a(plus(X1,plus(int_zero,int_one)),X1) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,plus(int_zero,int_one)),n)
| ~ int_leq(int_one,plus(X0,plus(int_zero,int_one))) ),
inference(resolution,[status(thm)],[f341,f840]) ).
fof(f2132,definition,
! [X0,X1] :
( sQ109_spl
<=> ( a(plus(X1,int_one),X1) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,int_one),n)
| ~ int_leq(int_one,plus(X0,int_one)) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f2135,plain,
( sQ7_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f2126,f2132,f99]) ).
fof(f2136,definition,
! [X0,X1] :
( sQ110_spl
<=> ( a(plus(X1,plus(int_one,int_zero)),X1) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,plus(int_one,int_zero)),n)
| ~ int_leq(int_one,plus(X0,plus(int_one,int_zero))) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f2139,plain,
( sQ67_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f2127,f2136,f1652]) ).
fof(f2140,definition,
! [X0,X1] :
( sQ111_spl
<=> ( a(plus(X1,plus(int_zero,int_one)),X1) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,plus(int_zero,int_one)),n)
| ~ int_leq(int_one,plus(X0,plus(int_zero,int_one))) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f2143,plain,
( sQ69_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f2128,f2140,f1659]) ).
fof(f2148,plain,
( ~ sQ69_spl
| int_zero = int_one ),
inference(forward_demodulation,[status(thm)],[f105,f1660]) ).
fof(f2149,plain,
( ~ sQ69_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2148,f101]) ).
fof(f2150,plain,
( ~ sQ69_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f2149]) ).
fof(f2151,plain,
( ~ sQ67_spl
| int_zero = int_one ),
inference(forward_demodulation,[status(thm)],[f28,f1653]) ).
fof(f2152,plain,
( ~ sQ67_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2151,f101]) ).
fof(f2153,plain,
( ~ sQ67_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f2152]) ).
fof(f2171,definition,
( sQ113_spl
<=> int_leq(int_one,plus(int_zero,int_one)) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f2173,plain,
( sQ113_spl
| ~ int_leq(int_one,plus(int_zero,int_one)) ),
inference(component_clause,[status(thm)],[f2171]) ).
fof(f2190,plain,
( sQ92_spl
| int_less(sK2_skl,int_zero) ),
inference(resolution,[status(thm)],[f1949,f25]) ).
fof(f2239,definition,
( sQ115_spl
<=> int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f2241,plain,
( sQ115_spl
| ~ int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))) ),
inference(component_clause,[status(thm)],[f2239]) ).
fof(f2251,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2100,f50]) ).
fof(f2252,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f2251]) ).
fof(f2311,plain,
( sQ113_spl
| ~ int_leq(int_one,int_one) ),
inference(forward_demodulation,[status(thm)],[f105,f2173]) ).
fof(f2312,plain,
( sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2311,f59]) ).
fof(f2313,plain,
sQ113_spl,
inference(contradiction_clause,[status(thm)],[f2312]) ).
fof(f2472,plain,
( sQ53_spl
| ~ int_less(int_zero,sK2_skl) ),
inference(resolution,[status(thm)],[f1176,f39]) ).
fof(f2475,plain,
( sQ53_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f2472,f1935,f1174]) ).
fof(f2495,plain,
( sQ115_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f1007,f2241]) ).
fof(f2534,definition,
( sQ141_spl
<=> int_less(sK2_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f2673,plain,
( sK0_skl(sK1_skl,int_zero) = sK0_skl(sK1_skl,int_zero)
| ~ int_less(int_zero,sK1_skl) ),
inference(paramodulation,[status(thm)],[f1359,f153]) ).
fof(f2675,definition,
( sQ154_spl
<=> sK0_skl(sK1_skl,int_zero) = sK0_skl(sK1_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f2678,plain,
( sQ154_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2673,f438,f2675]) ).
fof(f2680,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f440,f1067]) ).
fof(f2681,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f2680]) ).
fof(f2707,plain,
( sQ19_spl
| ~ int_less(sK2_skl,int_one) ),
inference(resolution,[status(thm)],[f69,f280]) ).
fof(f2708,plain,
~ int_less(sK2_skl,int_zero),
inference(resolution,[status(thm)],[f69,f1067]) ).
fof(f2710,plain,
( ~ int_leq(int_one,sK1_skl)
| ~ int_less(sK2_skl,int_zero) ),
inference(resolution,[status(thm)],[f69,f40]) ).
fof(f2713,plain,
( sQ19_spl
| ~ sQ89_spl ),
inference(split_clause,[status(thm)],[f2707,f1862,f217]) ).
fof(f2714,plain,
( sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2708,f2190]) ).
fof(f2715,plain,
sQ92_spl,
inference(contradiction_clause,[status(thm)],[f2714]) ).
fof(f2717,plain,
( ~ sQ12_spl
| ~ sQ141_spl ),
inference(split_clause,[status(thm)],[f2710,f2534,f165]) ).
fof(f2722,plain,
( ~ sQ53_spl
| sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1175,f2495]) ).
fof(f2723,plain,
( ~ sQ53_spl
| sQ115_spl ),
inference(contradiction_clause,[status(thm)],[f2722]) ).
fof(f2729,plain,
( sQ89_spl
| ~ sQ93_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f2027,f257,f1950,f1862]) ).
fof(f2928,plain,
plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl,
inference(resolution,[status(thm)],[f49,f34]) ).
fof(f2951,plain,
sK0_skl(sK1_skl,int_zero) = sK1_skl,
inference(resolution,[status(thm)],[f48,f149]) ).
fof(f3366,plain,
( int_zero = plus(int_one,int_zero)
| int_leq(int_one,plus(int_one,int_zero)) ),
inference(resolution,[status(thm)],[f1059,f495]) ).
fof(f3374,definition,
( sQ177_spl
<=> int_leq(int_one,plus(int_one,int_zero)) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f3377,plain,
( sQ67_spl
| sQ177_spl ),
inference(split_clause,[status(thm)],[f3366,f3374,f1652]) ).
fof(f3474,definition,
( sQ179_spl
<=> int_less(int_one,int_one) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f3475,plain,
( ~ sQ179_spl
| int_less(int_one,int_one) ),
inference(component_clause,[status(thm)],[f3474]) ).
fof(f3568,plain,
( ~ int_leq(int_one,int_zero)
| ~ int_leq(int_one,int_zero) ),
inference(resolution,[status(thm)],[f134,f40]) ).
fof(f3572,plain,
~ sQ6_spl,
inference(split_clause,[status(thm)],[f3568,f96]) ).
fof(f3730,plain,
( ~ sQ179_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3475,f60]) ).
fof(f3731,plain,
~ sQ179_spl,
inference(contradiction_clause,[status(thm)],[f3730]) ).
fof(f3765,definition,
( sQ189_spl
<=> int_leq(n,n) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f3767,plain,
( sQ189_spl
| ~ int_leq(n,n) ),
inference(component_clause,[status(thm)],[f3765]) ).
fof(f3790,plain,
( sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3767,f59]) ).
fof(f3791,plain,
sQ189_spl,
inference(contradiction_clause,[status(thm)],[f3790]) ).
fof(f4478,plain,
( ~ int_less(sK1_skl,int_zero)
| ~ int_less(int_zero,sK1_skl) ),
inference(paramodulation,[status(thm)],[f2951,f152]) ).
fof(f4482,definition,
( sQ203_spl
<=> int_less(sK1_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f4485,plain,
( ~ sQ203_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f4478,f438,f4482]) ).
fof(f4490,plain,
( ~ sQ10_spl
| ~ int_leq(sK1_skl,sK1_skl)
| ~ int_leq(sK2_skl,n)
| ~ int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)))
| ~ int_leq(sK1_skl,n)
| ~ int_leq(int_one,sK1_skl) ),
inference(paramodulation,[status(thm)],[f2928,f160]) ).
fof(f4494,definition,
( sQ204_spl
<=> int_leq(sK1_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f4496,plain,
( sQ204_spl
| ~ int_leq(sK1_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f4494]) ).
fof(f4497,plain,
( ~ sQ10_spl
| ~ sQ204_spl
| ~ sQ102_spl
| ~ sQ115_spl
| ~ sQ29_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f4490,f165,f415,f2239,f2098,f4494,f159]) ).
fof(f4505,plain,
( sQ204_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4496,f59]) ).
fof(f4506,plain,
sQ204_spl,
inference(contradiction_clause,[status(thm)],[f4505]) ).
fof(f4507,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f169,f51]) ).
fof(f4508,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f4507]) ).
fof(f4509,plain,
$false,
inference(sat_refutation,[status(thm)],[f171,f177,f183,f207,f214,f220,f409,f531,f719,f848,f890,f1243,f1312,f1474,f1480,f1590,f1592,f1648,f1655,f1662,f1669,f1672,f1847,f1946,f1953,f2031,f2135,f2139,f2143,f2150,f2153,f2252,f2313,f2475,f2678,f2681,f2713,f2715,f2717,f2723,f2729,f3377,f3572,f3731,f3791,f4485,f4497,f4506,f4508]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV486+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n018.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 08:55:43 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.67/1.29 % Refutation found
% 0.67/1.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.67/1.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.39/1.34 % Elapsed time: 0.877397 seconds
% 0.39/1.34 % CPU time: 6.504051 seconds
% 0.39/1.34 % Total memory used: 136.745 MB
% 0.39/1.34 % Net memory used: 129.173 MB
%------------------------------------------------------------------------------