%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV486+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 3.81s 1.04s
% Output : CNFRefutation 3.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 69
% Syntax : Number of formulae : 326 ( 50 unt; 57 def)
% Number of atoms : 816 ( 137 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 807 ( 317 ~; 382 |; 37 &)
% ( 60 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 61 ( 59 usr; 58 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 206 ( 201 !; 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) = lu(plus(K,C),K) ) ) ) ),
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(f18,plain,
! [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) = lu(plus(K,C),K)
| ~ 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(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(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(f67,plain,
! [X0,X1,X2] :
( ~ int_less(X2,X0)
| ~ int_less(X1,X2)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f65,f22]) ).
fof(f68,plain,
! [X0,X1] :
( X1 = X0
| ~ int_leq(X1,X0)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f65,f17]) ).
fof(f70,plain,
( sK2_skl = sK1_skl
| ~ int_leq(sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f66,f17]) ).
fof(f71,definition,
( sQ2_spl
<=> int_leq(sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f74,definition,
( sQ3_spl
<=> sK2_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f75,plain,
( ~ sQ3_spl
| sK2_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f74]) ).
fof(f77,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f70,f71,f74]) ).
fof(f90,plain,
~ int_less(int_one,int_zero),
inference(resolution,[status(thm)],[f26,f65]) ).
fof(f103,plain,
( int_one = int_zero
| ~ int_leq(int_one,int_zero) ),
inference(resolution,[status(thm)],[f90,f17]) ).
fof(f104,definition,
( sQ6_spl
<=> int_leq(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f107,definition,
( sQ7_spl
<=> int_one = int_zero ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f108,plain,
( ~ sQ7_spl
| int_one = int_zero ),
inference(component_clause,[status(thm)],[f107]) ).
fof(f109,plain,
( sQ7_spl
| int_one != int_zero ),
inference(component_clause,[status(thm)],[f107]) ).
fof(f110,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f103,f104,f107]) ).
fof(f113,plain,
! [X0] : X0 = plus(int_zero,X0),
inference(paramodulation,[status(thm)],[f28,f27]) ).
fof(f143,plain,
! [X0,X1] :
( int_leq(plus(int_zero,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f30,f26]) ).
fof(f147,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(f148,plain,
! [X0,X1] :
( int_leq(X0,plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f113,f143]) ).
fof(f150,plain,
plus(int_zero,sK0_skl(int_one,int_zero)) = int_one,
inference(resolution,[status(thm)],[f34,f26]) ).
fof(f152,plain,
plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl,
inference(resolution,[status(thm)],[f34,f49]) ).
fof(f154,plain,
! [X0,X1] :
( X0 = X1
| ~ int_leq(X0,X1)
| plus(X0,sK0_skl(X1,X0)) = X1 ),
inference(resolution,[status(thm)],[f34,f17]) ).
fof(f155,plain,
sK0_skl(int_one,int_zero) = int_one,
inference(forward_demodulation,[status(thm)],[f113,f150]) ).
fof(f157,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(f162,plain,
! [X0,X1] :
( sK0_skl(sK0_skl(X1,X0),int_zero) = sK0_skl(X1,X0)
| ~ int_less(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f113,f157]) ).
fof(f166,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)],[f152,f63]) ).
fof(f167,definition,
! [X0] :
( sQ9_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,[sQ9_spl])],[split_symbol_definition]) ).
fof(f170,definition,
( sQ10_spl
<=> int_less(int_zero,sK0_skl(sK2_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f173,definition,
( sQ11_spl
<=> int_leq(int_one,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f175,plain,
( sQ11_spl
| ~ int_leq(int_one,sK1_skl) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f176,definition,
( sQ12_spl
<=> a(sK1_skl,sK2_skl) = real_zero ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f177,plain,
( ~ sQ12_spl
| a(sK1_skl,sK2_skl) = real_zero ),
inference(component_clause,[status(thm)],[f176]) ).
fof(f179,plain,
( sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f166,f167,f170,f173,f176]) ).
fof(f180,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f177,f51]) ).
fof(f181,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f180]) ).
fof(f182,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f175,f48]) ).
fof(f183,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f182]) ).
fof(f190,plain,
( sK2_skl = n
| ~ int_less(n,sK2_skl) ),
inference(resolution,[status(thm)],[f68,f50]) ).
fof(f191,plain,
( int_one = sK1_skl
| ~ int_less(sK1_skl,int_one) ),
inference(resolution,[status(thm)],[f68,f48]) ).
fof(f196,definition,
( sQ13_spl
<=> int_less(n,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( sQ13_spl
| ~ int_less(n,sK2_skl) ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,definition,
( sQ14_spl
<=> sK2_skl = n ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f200,plain,
( ~ sQ14_spl
| sK2_skl = n ),
inference(component_clause,[status(thm)],[f199]) ).
fof(f202,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f190,f196,f199]) ).
fof(f203,definition,
( sQ15_spl
<=> int_less(sK1_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f205,plain,
( sQ15_spl
| ~ int_less(sK1_skl,int_one) ),
inference(component_clause,[status(thm)],[f203]) ).
fof(f206,definition,
( sQ16_spl
<=> int_one = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( ~ sQ16_spl
| int_one = sK1_skl ),
inference(component_clause,[status(thm)],[f206]) ).
fof(f209,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f191,f203,f206]) ).
fof(f211,plain,
( sQ15_spl
| sK1_skl = int_one
| ~ int_leq(sK1_skl,int_one) ),
inference(resolution,[status(thm)],[f205,f17]) ).
fof(f212,definition,
( sQ17_spl
<=> int_leq(sK1_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( sQ17_spl
| ~ int_leq(sK1_skl,int_one) ),
inference(component_clause,[status(thm)],[f212]) ).
fof(f215,plain,
( sQ15_spl
| sQ16_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f211,f212,f206,f203]) ).
fof(f226,plain,
( sQ13_spl
| n = sK2_skl
| ~ int_leq(n,sK2_skl) ),
inference(resolution,[status(thm)],[f198,f17]) ).
fof(f227,definition,
( sQ18_spl
<=> int_leq(n,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f229,plain,
( sQ18_spl
| ~ int_leq(n,sK2_skl) ),
inference(component_clause,[status(thm)],[f227]) ).
fof(f230,plain,
( sQ13_spl
| sQ14_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f226,f227,f199,f196]) ).
fof(f258,definition,
( sQ21_spl
<=> int_less(int_zero,int_one) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( sQ21_spl
| ~ int_less(int_zero,int_one) ),
inference(component_clause,[status(thm)],[f258]) ).
fof(f281,plain,
( sQ17_spl
| int_less(int_one,sK1_skl) ),
inference(resolution,[status(thm)],[f214,f25]) ).
fof(f283,plain,
( sQ18_spl
| int_less(sK2_skl,n) ),
inference(resolution,[status(thm)],[f229,f25]) ).
fof(f291,plain,
! [X0,X1,X2] :
( ~ int_less(X2,X1)
| int_less(X0,plus(X0,sK0_skl(X1,X2))) ),
inference(resolution,[status(thm)],[f61,f35]) ).
fof(f293,plain,
! [X0,X1] :
( int_zero = X1
| ~ int_leq(int_zero,X1)
| int_less(X0,plus(X0,X1)) ),
inference(resolution,[status(thm)],[f61,f17]) ).
fof(f302,plain,
! [X0] :
( ~ int_less(X0,sK1_skl)
| ~ int_less(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f66,f22]) ).
fof(f306,plain,
! [X0,X1] :
( int_leq(plus(sK1_skl,X0),plus(sK2_skl,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f49,f30]) ).
fof(f325,plain,
! [X0] :
( sQ18_spl
| ~ int_less(X0,sK2_skl)
| ~ int_less(n,X0) ),
inference(resolution,[status(thm)],[f283,f67]) ).
fof(f351,plain,
! [X0] : int_less(X0,plus(X0,int_one)),
inference(resolution,[status(thm)],[f26,f61]) ).
fof(f394,plain,
int_less(int_zero,sK1_skl),
inference(resolution,[status(thm)],[f40,f48]) ).
fof(f396,plain,
! [X0] :
( ~ int_less(int_one,X0)
| int_less(int_zero,X0) ),
inference(resolution,[status(thm)],[f40,f18]) ).
fof(f440,definition,
( sQ27_spl
<=> int_leq(sK1_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( sQ27_spl
| ~ int_leq(sK1_skl,n) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f465,definition,
( sQ29_spl
<=> int_less(int_zero,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f467,plain,
( sQ29_spl
| ~ int_less(int_zero,sK1_skl) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f516,definition,
( sQ32_spl
<=> int_leq(sK2_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ32_spl
| ~ int_leq(sK2_skl,int_one) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f519,definition,
( sQ33_spl
<=> sK2_skl = int_one ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( ~ sQ33_spl
| sK2_skl = int_one ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f536,plain,
( sQ17_spl
| ~ int_less(sK1_skl,int_one) ),
inference(resolution,[status(thm)],[f281,f65]) ).
fof(f573,plain,
plus(int_zero,sK0_skl(sK1_skl,int_zero)) = sK1_skl,
inference(resolution,[status(thm)],[f394,f34]) ).
fof(f578,plain,
sK0_skl(sK1_skl,int_zero) = sK1_skl,
inference(forward_demodulation,[status(thm)],[f113,f573]) ).
fof(f585,plain,
( sQ32_spl
| int_less(int_one,sK2_skl) ),
inference(resolution,[status(thm)],[f518,f25]) ).
fof(f627,plain,
( ~ sQ14_spl
| int_less(sK1_skl,n) ),
inference(backward_demodulation,[status(thm)],[f200,f49]) ).
fof(f699,plain,
! [X0] : int_leq(X0,plus(int_one,X0)),
inference(resolution,[status(thm)],[f148,f59]) ).
fof(f719,plain,
( sQ17_spl
| int_less(int_one,sK1_skl) ),
inference(resolution,[status(thm)],[f214,f25]) ).
fof(f775,definition,
( sQ39_spl
<=> int_less(sK2_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( sQ39_spl
| ~ int_less(sK2_skl,int_one) ),
inference(component_clause,[status(thm)],[f775]) ).
fof(f808,plain,
( ~ sQ33_spl
| int_less(sK1_skl,int_one) ),
inference(forward_demodulation,[status(thm)],[f520,f49]) ).
fof(f809,plain,
( ~ sQ33_spl
| sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f808,f536]) ).
fof(f810,plain,
( ~ sQ33_spl
| sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f809]) ).
fof(f875,plain,
! [X0] :
( int_zero = X0
| ~ int_leq(int_zero,X0)
| int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f39,f17]) ).
fof(f930,plain,
! [X0,X1] :
( int_zero = X1
| ~ int_leq(int_zero,X1)
| int_less(X0,plus(X0,X1)) ),
inference(resolution,[status(thm)],[f61,f17]) ).
fof(f933,plain,
! [X0,X1] :
( X1 = X0
| ~ int_leq(X1,X0)
| int_less(int_zero,sK0_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f35,f17]) ).
fof(f960,plain,
( sQ39_spl
| sK2_skl = int_one
| ~ int_leq(sK2_skl,int_one) ),
inference(resolution,[status(thm)],[f777,f17]) ).
fof(f961,plain,
( sQ39_spl
| sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f960,f516,f519,f775]) ).
fof(f974,plain,
~ int_less(sK2_skl,sK1_skl),
inference(resolution,[status(thm)],[f49,f65]) ).
fof(f975,plain,
int_less(int_zero,sK1_skl),
inference(resolution,[status(thm)],[f48,f40]) ).
fof(f976,plain,
! [X0,X1] :
( a(sK1_skl,plus(sK1_skl,X1)) = real_zero
| ~ int_leq(sK1_skl,X0)
| ~ 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(resolution,[status(thm)],[f48,f63]) ).
fof(f1044,plain,
! [X0,X1,X2] :
( int_less(n,X0)
| 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(int_one,X0) ),
inference(resolution,[status(thm)],[f63,f25]) ).
fof(f1053,plain,
plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl,
inference(resolution,[status(thm)],[f49,f34]) ).
fof(f1057,plain,
~ int_less(sK2_skl,sK1_skl),
inference(resolution,[status(thm)],[f49,f65]) ).
fof(f1079,plain,
( ~ sQ16_spl
| ~ int_less(sK2_skl,int_one) ),
inference(forward_demodulation,[status(thm)],[f207,f974]) ).
fof(f1124,definition,
( sQ45_spl
<=> int_leq(int_one,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1125,plain,
( ~ sQ45_spl
| int_leq(int_one,sK2_skl) ),
inference(component_clause,[status(thm)],[f1124]) ).
fof(f1126,plain,
( sQ45_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(component_clause,[status(thm)],[f1124]) ).
fof(f1169,plain,
( sQ45_spl
| int_less(sK2_skl,int_one) ),
inference(resolution,[status(thm)],[f1126,f25]) ).
fof(f1171,plain,
( sQ45_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1169,f1079]) ).
fof(f1172,plain,
( sQ45_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f1171]) ).
fof(f1238,plain,
! [X0,X1,X2] :
( int_zero = X1
| ~ int_leq(int_zero,X1)
| a(X2,plus(X2,X1)) = real_zero
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_leq(plus(X0,X1),n)
| ~ int_leq(int_one,plus(X0,X1))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f63,f17]) ).
fof(f1241,plain,
! [X0] :
( int_zero = int_zero
| int_less(X0,plus(X0,int_zero)) ),
inference(resolution,[status(thm)],[f293,f59]) ).
fof(f1242,definition,
! [X0] :
( sQ47_spl
<=> int_less(X0,plus(X0,int_zero)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1243,plain,
! [X0] :
( ~ sQ47_spl
| int_less(X0,plus(X0,int_zero)) ),
inference(component_clause,[status(thm)],[f1242]) ).
fof(f1245,definition,
( sQ48_spl
<=> int_zero = int_zero ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1248,plain,
( sQ48_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f1241,f1242,f1245]) ).
fof(f1249,plain,
! [X0] :
( ~ sQ47_spl
| int_less(X0,X0) ),
inference(forward_demodulation,[status(thm)],[f28,f1243]) ).
fof(f1250,plain,
( ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1249,f60]) ).
fof(f1251,plain,
~ sQ47_spl,
inference(contradiction_clause,[status(thm)],[f1250]) ).
fof(f1365,plain,
! [X0] :
( int_zero = plus(int_one,int_zero)
| int_less(X0,plus(X0,plus(int_one,int_zero))) ),
inference(resolution,[status(thm)],[f699,f293]) ).
fof(f1372,plain,
int_leq(int_zero,int_one),
inference(paramodulation,[status(thm)],[f28,f699]) ).
fof(f1373,plain,
! [X0] : int_leq(X0,plus(X0,int_one)),
inference(paramodulation,[status(thm)],[f27,f699]) ).
fof(f1375,definition,
! [X0] :
( sQ49_spl
<=> int_less(X0,plus(X0,plus(int_one,int_zero))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1378,definition,
( sQ50_spl
<=> int_zero = plus(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1379,plain,
( ~ sQ50_spl
| int_zero = plus(int_one,int_zero) ),
inference(component_clause,[status(thm)],[f1378]) ).
fof(f1381,plain,
( sQ50_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1365,f1375,f1378]) ).
fof(f1383,plain,
! [X0] :
( int_zero = int_one
| int_less(X0,plus(X0,int_one)) ),
inference(resolution,[status(thm)],[f1372,f293]) ).
fof(f1385,plain,
int_leq(plus(sK1_skl,int_zero),plus(sK2_skl,int_one)),
inference(resolution,[status(thm)],[f1372,f306]) ).
fof(f1386,plain,
( int_zero = int_one
| plus(int_zero,sK0_skl(int_one,int_zero)) = int_one ),
inference(resolution,[status(thm)],[f1372,f154]) ).
fof(f1387,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)],[f1372,f147]) ).
fof(f1389,plain,
( int_zero = int_one
| ~ int_less(int_one,int_zero) ),
inference(resolution,[status(thm)],[f1372,f68]) ).
fof(f1390,definition,
! [X0] :
( sQ51_spl
<=> int_less(X0,plus(X0,int_one)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
( sQ7_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1383,f1390,f107]) ).
fof(f1394,plain,
int_leq(sK1_skl,plus(sK2_skl,int_one)),
inference(forward_demodulation,[status(thm)],[f28,f1385]) ).
fof(f1395,definition,
( sQ52_spl
<=> plus(int_zero,sK0_skl(int_one,int_zero)) = int_one ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1398,plain,
( sQ7_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1386,f1395,f107]) ).
fof(f1399,definition,
! [X0,X1] :
( sQ53_spl
<=> ( int_leq(plus(int_zero,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( sQ7_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1387,f1399,f107]) ).
fof(f1404,definition,
( sQ54_spl
<=> int_less(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1407,plain,
( sQ7_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1389,f1404,f107]) ).
fof(f1412,plain,
( ~ sQ7_spl
| int_less(int_one,int_one) ),
inference(backward_demodulation,[status(thm)],[f108,f26]) ).
fof(f1428,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1412,f60]) ).
fof(f1429,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f1428]) ).
fof(f1486,plain,
! [X0,X1] :
( int_leq(int_one,sK0_skl(X1,X0))
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f35,f39]) ).
fof(f1588,plain,
! [X0] :
( ~ int_less(int_zero,sK1_skl)
| int_less(X0,plus(X0,sK1_skl)) ),
inference(paramodulation,[status(thm)],[f578,f291]) ).
fof(f1596,definition,
! [X0] :
( sQ56_spl
<=> int_less(X0,plus(X0,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1599,plain,
( ~ sQ29_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f1588,f1596,f465]) ).
fof(f1634,plain,
( sQ32_spl
| int_less(int_zero,sK2_skl) ),
inference(resolution,[status(thm)],[f396,f585]) ).
fof(f1667,plain,
( sQ27_spl
| ~ int_less(sK1_skl,n) ),
inference(resolution,[status(thm)],[f442,f18]) ).
fof(f1744,definition,
( sQ59_spl
<=> int_leq(int_one,int_one) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1746,plain,
( sQ59_spl
| ~ int_leq(int_one,int_one) ),
inference(component_clause,[status(thm)],[f1744]) ).
fof(f1767,plain,
( sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1746,f59]) ).
fof(f1768,plain,
sQ59_spl,
inference(contradiction_clause,[status(thm)],[f1767]) ).
fof(f2010,definition,
( sQ80_spl
<=> int_less(int_zero,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f2012,plain,
( sQ80_spl
| ~ int_less(int_zero,sK2_skl) ),
inference(component_clause,[status(thm)],[f2010]) ).
fof(f2129,plain,
( sQ17_spl
| ~ int_less(sK2_skl,int_one) ),
inference(resolution,[status(thm)],[f302,f719]) ).
fof(f2186,plain,
( int_zero = plus(int_one,int_zero)
| int_leq(int_one,plus(int_one,int_zero)) ),
inference(resolution,[status(thm)],[f875,f699]) ).
fof(f2187,plain,
( int_zero = plus(int_zero,int_one)
| int_leq(int_one,plus(int_zero,int_one)) ),
inference(resolution,[status(thm)],[f875,f1373]) ).
fof(f2192,definition,
( sQ89_spl
<=> int_leq(int_one,plus(int_one,int_zero)) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2195,plain,
( sQ50_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f2186,f2192,f1378]) ).
fof(f2196,definition,
( sQ90_spl
<=> int_leq(int_one,plus(int_zero,int_one)) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2199,definition,
( sQ91_spl
<=> int_zero = plus(int_zero,int_one) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2200,plain,
( ~ sQ91_spl
| int_zero = plus(int_zero,int_one) ),
inference(component_clause,[status(thm)],[f2199]) ).
fof(f2202,plain,
( sQ91_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2187,f2196,f2199]) ).
fof(f2204,plain,
( ~ sQ50_spl
| int_zero = int_one ),
inference(forward_demodulation,[status(thm)],[f28,f1379]) ).
fof(f2205,plain,
( ~ sQ50_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2204,f109]) ).
fof(f2206,plain,
( ~ sQ50_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f2205]) ).
fof(f2218,definition,
( sQ93_spl
<=> int_leq(sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f2219,plain,
( ~ sQ93_spl
| int_leq(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f2218]) ).
fof(f2220,plain,
( sQ93_spl
| ~ int_leq(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f2218]) ).
fof(f2251,plain,
! [X0] :
( int_zero = plus(int_zero,int_one)
| int_less(X0,plus(X0,plus(int_zero,int_one))) ),
inference(resolution,[status(thm)],[f930,f1373]) ).
fof(f2257,definition,
! [X0] :
( sQ95_spl
<=> int_less(X0,plus(X0,plus(int_zero,int_one))) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f2260,plain,
( sQ91_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f2251,f2257,f2199]) ).
fof(f2262,plain,
( ~ sQ91_spl
| int_zero = int_one ),
inference(forward_demodulation,[status(thm)],[f113,f2200]) ).
fof(f2263,plain,
( ~ sQ91_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2262,f109]) ).
fof(f2264,plain,
( ~ sQ91_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f2263]) ).
fof(f2282,plain,
( sK1_skl = plus(sK2_skl,int_one)
| plus(sK1_skl,sK0_skl(plus(sK2_skl,int_one),sK1_skl)) = plus(sK2_skl,int_one) ),
inference(resolution,[status(thm)],[f1394,f154]) ).
fof(f2283,plain,
! [X0,X1] :
( sK1_skl = plus(sK2_skl,int_one)
| int_leq(plus(sK1_skl,X0),plus(plus(sK2_skl,int_one),X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f1394,f147]) ).
fof(f2285,plain,
( sK1_skl = plus(sK2_skl,int_one)
| ~ int_less(plus(sK2_skl,int_one),sK1_skl) ),
inference(resolution,[status(thm)],[f1394,f68]) ).
fof(f2288,definition,
( sQ96_spl
<=> plus(sK1_skl,sK0_skl(plus(sK2_skl,int_one),sK1_skl)) = plus(sK2_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f2291,definition,
( sQ97_spl
<=> sK1_skl = plus(sK2_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f2292,plain,
( ~ sQ97_spl
| sK1_skl = plus(sK2_skl,int_one) ),
inference(component_clause,[status(thm)],[f2291]) ).
fof(f2294,plain,
( sQ97_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f2282,f2288,f2291]) ).
fof(f2295,definition,
! [X0,X1] :
( sQ98_spl
<=> ( int_leq(plus(sK1_skl,X0),plus(plus(sK2_skl,int_one),X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2298,plain,
( sQ97_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f2283,f2295,f2291]) ).
fof(f2299,definition,
( sQ99_spl
<=> int_less(plus(sK2_skl,int_one),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2302,plain,
( sQ97_spl
| ~ sQ99_spl ),
inference(split_clause,[status(thm)],[f2285,f2299,f2291]) ).
fof(f2309,plain,
( ~ sQ97_spl
| int_less(sK2_skl,sK1_skl) ),
inference(paramodulation,[status(thm)],[f2292,f351]) ).
fof(f2347,plain,
( int_zero = int_one
| int_less(int_zero,sK0_skl(int_one,int_zero)) ),
inference(resolution,[status(thm)],[f933,f1372]) ).
fof(f2367,definition,
( sQ106_spl
<=> int_less(int_zero,sK0_skl(int_one,int_zero)) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f2370,plain,
( sQ7_spl
| sQ106_spl ),
inference(split_clause,[status(thm)],[f2347,f2367,f107]) ).
fof(f2388,plain,
( sQ93_spl
| int_less(sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f2220,f25]) ).
fof(f2390,plain,
( sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2388,f1057]) ).
fof(f2391,plain,
sQ93_spl,
inference(contradiction_clause,[status(thm)],[f2390]) ).
fof(f2392,plain,
( ~ sQ93_spl
| sK1_skl = sK2_skl
| int_less(int_zero,sK0_skl(sK2_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f2219,f933]) ).
fof(f2395,plain,
( ~ sQ93_spl
| sK1_skl = sK2_skl
| plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl ),
inference(resolution,[status(thm)],[f2219,f154]) ).
fof(f2396,plain,
! [X0,X1] :
( ~ sQ93_spl
| sK1_skl = sK2_skl
| int_leq(plus(sK1_skl,X0),plus(sK2_skl,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f2219,f147]) ).
fof(f2398,plain,
( ~ sQ93_spl
| sK1_skl = sK2_skl
| ~ int_less(sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f2219,f68]) ).
fof(f2399,plain,
( ~ sQ93_spl
| sQ3_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f2392,f170,f74,f2218]) ).
fof(f2400,definition,
( sQ110_spl
<=> plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f2403,plain,
( ~ sQ93_spl
| sQ3_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f2395,f2400,f74,f2218]) ).
fof(f2404,definition,
! [X0,X1] :
( sQ111_spl
<=> ( int_leq(plus(sK1_skl,X0),plus(sK2_skl,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f2407,plain,
( ~ sQ93_spl
| sQ3_spl
| sQ111_spl ),
inference(split_clause,[status(thm)],[f2396,f2404,f74,f2218]) ).
fof(f2408,definition,
( sQ112_spl
<=> int_less(sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f2411,plain,
( ~ sQ93_spl
| sQ3_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f2398,f2408,f74,f2218]) ).
fof(f2412,plain,
( ~ sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2309,f1057]) ).
fof(f2413,plain,
~ sQ97_spl,
inference(contradiction_clause,[status(thm)],[f2412]) ).
fof(f2435,plain,
( ~ sQ3_spl
| int_less(sK2_skl,sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f75,f49]) ).
fof(f2447,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2435,f60]) ).
fof(f2448,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f2447]) ).
fof(f2579,plain,
! [X0] :
( int_less(n,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(int_one,X0) ),
inference(paramodulation,[status(thm)],[f1053,f1044]) ).
fof(f2581,definition,
! [X0] :
( sQ116_spl
<=> ( int_less(n,X0)
| ~ 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(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f2584,plain,
( sQ12_spl
| ~ sQ11_spl
| ~ sQ10_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f2579,f2581,f170,f173,f176]) ).
fof(f2656,plain,
( sQ18_spl
| ~ int_less(n,sK1_skl) ),
inference(resolution,[status(thm)],[f325,f49]) ).
fof(f2698,plain,
( sQ27_spl
| int_less(n,sK1_skl) ),
inference(resolution,[status(thm)],[f442,f25]) ).
fof(f2709,plain,
( ~ sQ14_spl
| sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f627,f1667]) ).
fof(f2710,plain,
( ~ sQ14_spl
| sQ27_spl ),
inference(contradiction_clause,[status(thm)],[f2709]) ).
fof(f3137,plain,
! [X0,X1] :
( int_zero = int_one
| a(X1,plus(X1,int_one)) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(plus(X0,int_one),n)
| ~ int_leq(int_one,plus(X0,int_one))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f1238,f1372]) ).
fof(f3141,definition,
! [X0,X1] :
( sQ128_spl
<=> ( a(X1,plus(X1,int_one)) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(plus(X0,int_one),n)
| ~ int_leq(int_one,plus(X0,int_one))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f3144,plain,
( sQ7_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f3137,f3141,f107]) ).
fof(f3173,definition,
( sQ130_spl
<=> int_leq(sK2_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f3175,plain,
( sQ130_spl
| ~ int_leq(sK2_skl,n) ),
inference(component_clause,[status(thm)],[f3173]) ).
fof(f3181,plain,
( sQ27_spl
| sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2698,f2656]) ).
fof(f3182,plain,
( sQ27_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f3181]) ).
fof(f3241,plain,
! [X0,X1] :
( int_zero = plus(int_zero,int_one)
| a(X1,plus(X1,plus(int_zero,int_one))) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(plus(X0,plus(int_zero,int_one)),n)
| ~ int_leq(int_one,plus(X0,plus(int_zero,int_one)))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f1373,f1238]) ).
fof(f3252,definition,
! [X0,X1] :
( sQ132_spl
<=> ( a(X1,plus(X1,plus(int_zero,int_one))) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(plus(X0,plus(int_zero,int_one)),n)
| ~ int_leq(int_one,plus(X0,plus(int_zero,int_one)))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f3255,plain,
( sQ91_spl
| sQ132_spl ),
inference(split_clause,[status(thm)],[f3241,f3252,f2199]) ).
fof(f3303,plain,
! [X0,X1] :
( int_zero = plus(int_one,int_zero)
| a(X1,plus(X1,plus(int_one,int_zero))) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(plus(X0,plus(int_one,int_zero)),n)
| ~ int_leq(int_one,plus(X0,plus(int_one,int_zero)))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f699,f1238]) ).
fof(f3314,definition,
! [X0,X1] :
( sQ133_spl
<=> ( a(X1,plus(X1,plus(int_one,int_zero))) = real_zero
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(plus(X0,plus(int_one,int_zero)),n)
| ~ int_leq(int_one,plus(X0,plus(int_one,int_zero)))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f3317,plain,
( sQ50_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f3303,f3314,f1378]) ).
fof(f3378,definition,
( sQ140_spl
<=> int_leq(int_zero,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f3380,plain,
( sQ140_spl
| ~ int_leq(int_zero,int_zero) ),
inference(component_clause,[status(thm)],[f3378]) ).
fof(f3609,plain,
( sK0_skl(int_one,int_zero) = sK0_skl(int_one,int_zero)
| ~ int_less(int_zero,int_one) ),
inference(paramodulation,[status(thm)],[f155,f162]) ).
fof(f3615,definition,
( sQ156_spl
<=> sK0_skl(int_one,int_zero) = sK0_skl(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f3618,plain,
( sQ156_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f3609,f258,f3615]) ).
fof(f3624,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f260,f26]) ).
fof(f3625,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f3624]) ).
fof(f3665,plain,
int_less(int_zero,sK1_skl),
inference(resolution,[status(thm)],[f48,f40]) ).
fof(f3859,plain,
plus(int_zero,sK0_skl(sK1_skl,int_zero)) = sK1_skl,
inference(resolution,[status(thm)],[f3665,f34]) ).
fof(f3864,plain,
sK0_skl(sK1_skl,int_zero) = sK1_skl,
inference(forward_demodulation,[status(thm)],[f113,f3859]) ).
fof(f3968,plain,
( sQ32_spl
| plus(int_zero,sK0_skl(sK2_skl,int_zero)) = sK2_skl ),
inference(resolution,[status(thm)],[f1634,f34]) ).
fof(f3973,plain,
( sQ32_spl
| sK0_skl(sK2_skl,int_zero) = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f113,f3968]) ).
fof(f4143,definition,
( sQ179_spl
<=> int_leq(n,n) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f4145,plain,
( sQ179_spl
| ~ int_leq(n,n) ),
inference(component_clause,[status(thm)],[f4143]) ).
fof(f4199,plain,
( sK0_skl(sK1_skl,int_zero) = sK0_skl(sK1_skl,int_zero)
| ~ int_less(int_zero,sK1_skl) ),
inference(paramodulation,[status(thm)],[f3864,f162]) ).
fof(f4204,definition,
( sQ184_spl
<=> sK0_skl(sK1_skl,int_zero) = sK0_skl(sK1_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f4207,plain,
( sQ184_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f4199,f465,f4204]) ).
fof(f4211,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f467,f975]) ).
fof(f4212,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f4211]) ).
fof(f4319,plain,
( sQ179_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4145,f59]) ).
fof(f4320,plain,
sQ179_spl,
inference(contradiction_clause,[status(thm)],[f4319]) ).
fof(f4695,definition,
( sQ228_spl
<=> int_leq(sK1_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f4697,plain,
( sQ228_spl
| ~ int_leq(sK1_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f4695]) ).
fof(f4727,plain,
( sQ228_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4697,f59]) ).
fof(f4728,plain,
sQ228_spl,
inference(contradiction_clause,[status(thm)],[f4727]) ).
fof(f4829,plain,
( sQ140_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3380,f59]) ).
fof(f4830,plain,
sQ140_spl,
inference(contradiction_clause,[status(thm)],[f4829]) ).
fof(f5021,plain,
( sQ32_spl
| int_leq(int_one,sK2_skl)
| ~ int_less(int_zero,sK2_skl) ),
inference(paramodulation,[status(thm)],[f3973,f1486]) ).
fof(f5026,plain,
( sQ32_spl
| sQ45_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f5021,f2010,f1124,f516]) ).
fof(f5031,plain,
( sQ80_spl
| sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2012,f1634]) ).
fof(f5032,plain,
( sQ80_spl
| sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f5031]) ).
fof(f5043,plain,
( a(sK1_skl,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))) = real_zero
| ~ int_leq(sK1_skl,sK1_skl)
| ~ int_less(int_zero,sK0_skl(sK2_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)],[f1053,f976]) ).
fof(f5052,definition,
( sQ242_spl
<=> int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f5054,plain,
( sQ242_spl
| ~ int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))) ),
inference(component_clause,[status(thm)],[f5052]) ).
fof(f5055,definition,
( sQ243_spl
<=> a(sK1_skl,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))) = real_zero ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f5056,plain,
( ~ sQ243_spl
| a(sK1_skl,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))) = real_zero ),
inference(component_clause,[status(thm)],[f5055]) ).
fof(f5058,plain,
( sQ243_spl
| ~ sQ228_spl
| ~ sQ10_spl
| ~ sQ130_spl
| ~ sQ242_spl
| ~ sQ27_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f5043,f173,f440,f5052,f3173,f170,f4695,f5055]) ).
fof(f5090,plain,
( sQ242_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f1053,f5054]) ).
fof(f5091,plain,
( sQ242_spl
| ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5090,f1125]) ).
fof(f5092,plain,
( sQ242_spl
| ~ sQ45_spl ),
inference(contradiction_clause,[status(thm)],[f5091]) ).
fof(f5093,plain,
( sQ130_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3175,f50]) ).
fof(f5094,plain,
sQ130_spl,
inference(contradiction_clause,[status(thm)],[f5093]) ).
fof(f5096,plain,
( ~ sQ243_spl
| a(sK1_skl,sK2_skl) = real_zero ),
inference(forward_demodulation,[status(thm)],[f1053,f5056]) ).
fof(f5097,plain,
( ~ sQ243_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5096,f51]) ).
fof(f5098,plain,
~ sQ243_spl,
inference(contradiction_clause,[status(thm)],[f5097]) ).
fof(f5100,plain,
( sQ17_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f2129,f775,f212]) ).
fof(f5102,plain,
$false,
inference(sat_refutation,[status(thm)],[f77,f110,f179,f181,f183,f202,f209,f215,f230,f810,f961,f1172,f1248,f1251,f1381,f1393,f1398,f1402,f1407,f1429,f1599,f1768,f2195,f2202,f2206,f2260,f2264,f2294,f2298,f2302,f2370,f2391,f2399,f2403,f2407,f2411,f2413,f2448,f2584,f2710,f3144,f3182,f3255,f3317,f3618,f3625,f4207,f4212,f4320,f4728,f4830,f5026,f5032,f5058,f5092,f5094,f5098,f5100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV486+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n006.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 08:53:46 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 3.81/1.04 % Refutation found
% 3.81/1.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.81/1.04 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.81/1.08 % Elapsed time: 0.696653 seconds
% 3.81/1.08 % CPU time: 5.172738 seconds
% 3.81/1.08 % Total memory used: 131.974 MB
% 3.81/1.08 % Net memory used: 126.001 MB
%------------------------------------------------------------------------------