%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV487+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 6.67s 1.48s
% Output : CNFRefutation 6.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 103
% Syntax : Number of formulae : 492 ( 57 unt; 91 def)
% Number of atoms : 1202 ( 192 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1190 ( 480 ~; 572 |; 34 &)
% ( 94 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 95 ( 93 usr; 92 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 241 ( 236 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [I,J] :
( int_leq(I,J)
<=> ( I = J
| int_less(I,J) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,K] :
( ( int_less(J,K)
& int_less(I,J) )
=> int_less(I,K) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [I,J] :
( int_less(I,J)
=> I != J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [I,J] :
( int_leq(J,I)
| int_less(I,J) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
int_less(int_zero,int_one),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [I,J] : plus(I,J) = plus(J,I),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [I] : plus(I,int_zero) = I,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [I] :
( int_less(int_zero,I)
<=> int_leq(int_one,I) ),
file('/export/starexec/sandbox/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_leq(int_zero,C) )
=> ! [K] :
( ( int_leq(K,I)
& int_leq(int_one,K) )
=> a(K,plus(K,C)) = lu(K,plus(K,C)) ) )
& ! [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/sandbox/benchmark/theBenchmark.p') ).
fof(f13,conjecture,
! [I,J] :
( ( int_leq(I,n)
& int_less(J,I)
& int_leq(int_one,J) )
=> a(I,J) = real_zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
~ ! [I,J] :
( ( int_leq(I,n)
& int_less(J,I)
& int_leq(int_one,J) )
=> 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)) = lu(K,plus(K,C))
| ~ int_leq(K,I)
| ~ int_leq(int_one,K) )
| J != plus(I,C)
| ~ int_leq(int_zero,C) )
& ! [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(f44,plain,
! [X0,X1,X2,X3] :
( a(X3,plus(X3,X2)) = lu(X3,plus(X3,X2))
| ~ int_leq(X3,X0)
| ~ int_leq(int_one,X3)
| X1 != plus(X0,X2)
| ~ int_leq(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,
? [I,J] :
( a(I,J) != real_zero
& int_leq(I,n)
& int_less(J,I)
& int_leq(int_one,J) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f46,plain,
( a(sK1_skl,sK2_skl) != real_zero
& int_leq(sK1_skl,n)
& int_less(sK2_skl,sK1_skl)
& int_leq(int_one,sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(I,sK1_skl),skolemize(J,sK2_skl)],[f45]) ).
fof(f47,plain,
int_leq(int_one,sK2_skl),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
int_less(sK2_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f49,plain,
int_leq(sK1_skl,n),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f50,plain,
a(sK1_skl,sK2_skl) != real_zero,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f51,plain,
! [X0] : int_leq(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f19]) ).
fof(f52,plain,
! [X0] : ~ int_less(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f24]) ).
fof(f53,plain,
! [X0,X1] :
( ~ int_less(int_zero,X1)
| int_less(X0,plus(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f36]) ).
fof(f54,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(f55,plain,
! [X0,X1,X2] :
( a(X2,plus(X2,X1)) = lu(X2,plus(X2,X1))
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_leq(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)],[f44]) ).
fof(f57,plain,
! [X0,X1] :
( ~ int_less(X1,X0)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f22,f52]) ).
fof(f58,plain,
~ int_less(sK1_skl,sK2_skl),
inference(resolution,[status(thm)],[f57,f48]) ).
fof(f59,plain,
! [X0,X1,X2] :
( ~ int_less(X2,X0)
| ~ int_less(X1,X2)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f57,f22]) ).
fof(f60,plain,
! [X0,X1] :
( X1 = X0
| ~ int_leq(X1,X0)
| ~ int_less(X0,X1) ),
inference(resolution,[status(thm)],[f57,f17]) ).
fof(f61,plain,
! [X0] :
( ~ int_less(X0,sK2_skl)
| ~ int_less(sK1_skl,X0) ),
inference(resolution,[status(thm)],[f58,f22]) ).
fof(f62,plain,
( sK1_skl = sK2_skl
| ~ int_leq(sK1_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f58,f17]) ).
fof(f63,definition,
( sQ0_spl
<=> int_leq(sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f65,plain,
( sQ0_spl
| ~ int_leq(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f63]) ).
fof(f66,definition,
( sQ1_spl
<=> sK1_skl = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f67,plain,
( ~ sQ1_spl
| sK1_skl = sK2_skl ),
inference(component_clause,[status(thm)],[f66]) ).
fof(f68,plain,
( sQ1_spl
| sK1_skl != sK2_skl ),
inference(component_clause,[status(thm)],[f66]) ).
fof(f69,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f62,f63,f66]) ).
fof(f81,plain,
! [X0] :
( ~ int_less(int_one,X0)
| ~ int_less(X0,int_zero) ),
inference(resolution,[status(thm)],[f26,f59]) ).
fof(f82,plain,
~ int_less(int_one,int_zero),
inference(resolution,[status(thm)],[f26,f57]) ).
fof(f87,definition,
( sQ3_spl
<=> int_less(int_zero,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f95,plain,
( int_one = int_zero
| ~ int_leq(int_one,int_zero) ),
inference(resolution,[status(thm)],[f82,f17]) ).
fof(f96,definition,
( sQ4_spl
<=> int_leq(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f98,plain,
( sQ4_spl
| ~ int_leq(int_one,int_zero) ),
inference(component_clause,[status(thm)],[f96]) ).
fof(f99,definition,
( sQ5_spl
<=> int_one = int_zero ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f100,plain,
( ~ sQ5_spl
| int_one = int_zero ),
inference(component_clause,[status(thm)],[f99]) ).
fof(f101,plain,
( sQ5_spl
| int_one != int_zero ),
inference(component_clause,[status(thm)],[f99]) ).
fof(f102,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f95,f96,f99]) ).
fof(f105,plain,
! [X0] : X0 = plus(int_zero,X0),
inference(paramodulation,[status(thm)],[f28,f27]) ).
fof(f135,plain,
! [X0,X1] :
( int_leq(plus(int_zero,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f30,f26]) ).
fof(f139,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(f140,plain,
! [X0,X1] :
( int_leq(X0,plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f105,f135]) ).
fof(f142,plain,
plus(int_zero,sK0_skl(int_one,int_zero)) = int_one,
inference(resolution,[status(thm)],[f34,f26]) ).
fof(f143,plain,
! [X0] :
( ~ int_leq(int_one,X0)
| plus(int_zero,sK0_skl(X0,int_zero)) = X0 ),
inference(resolution,[status(thm)],[f34,f40]) ).
fof(f144,plain,
plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)) = sK1_skl,
inference(resolution,[status(thm)],[f34,f48]) ).
fof(f146,plain,
! [X0,X1] :
( X0 = X1
| ~ int_leq(X0,X1)
| plus(X0,sK0_skl(X1,X0)) = X1 ),
inference(resolution,[status(thm)],[f34,f17]) ).
fof(f147,plain,
sK0_skl(int_one,int_zero) = int_one,
inference(forward_demodulation,[status(thm)],[f105,f142]) ).
fof(f148,plain,
! [X0] :
( ~ int_leq(int_one,X0)
| sK0_skl(X0,int_zero) = X0 ),
inference(forward_demodulation,[status(thm)],[f105,f143]) ).
fof(f149,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(f154,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,f149]) ).
fof(f158,plain,
! [X0] :
( a(sK1_skl,sK2_skl) = real_zero
| ~ int_leq(sK2_skl,X0)
| ~ int_leq(int_one,sK2_skl)
| ~ int_less(int_zero,sK0_skl(sK1_skl,sK2_skl))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,sK0_skl(sK1_skl,sK2_skl)),n)
| ~ int_leq(int_one,plus(X0,sK0_skl(sK1_skl,sK2_skl))) ),
inference(paramodulation,[status(thm)],[f144,f54]) ).
fof(f159,definition,
! [X0] :
( sQ7_spl
<=> ( ~ int_leq(sK2_skl,X0)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,sK0_skl(sK1_skl,sK2_skl)),n)
| ~ int_leq(int_one,plus(X0,sK0_skl(sK1_skl,sK2_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f162,definition,
( sQ8_spl
<=> int_less(int_zero,sK0_skl(sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( sQ8_spl
| ~ int_less(int_zero,sK0_skl(sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f162]) ).
fof(f165,definition,
( sQ9_spl
<=> int_leq(int_one,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f167,plain,
( sQ9_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(component_clause,[status(thm)],[f165]) ).
fof(f168,definition,
( sQ10_spl
<=> a(sK1_skl,sK2_skl) = real_zero ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f169,plain,
( ~ sQ10_spl
| a(sK1_skl,sK2_skl) = real_zero ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,plain,
( sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f158,f159,f162,f165,f168]) ).
fof(f172,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f169,f50]) ).
fof(f173,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f172]) ).
fof(f174,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f167,f47]) ).
fof(f175,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f174]) ).
fof(f182,plain,
( sK1_skl = n
| ~ int_less(n,sK1_skl) ),
inference(resolution,[status(thm)],[f60,f49]) ).
fof(f183,plain,
( int_one = sK2_skl
| ~ int_less(sK2_skl,int_one) ),
inference(resolution,[status(thm)],[f60,f47]) ).
fof(f188,definition,
( sQ11_spl
<=> int_less(n,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f190,plain,
( sQ11_spl
| ~ int_less(n,sK1_skl) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f191,definition,
( sQ12_spl
<=> sK1_skl = n ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( ~ sQ12_spl
| sK1_skl = n ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,plain,
( sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f182,f188,f191]) ).
fof(f195,definition,
( sQ13_spl
<=> int_less(sK2_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( ~ sQ13_spl
| int_less(sK2_skl,int_one) ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f198,definition,
( sQ14_spl
<=> int_one = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( ~ sQ14_spl
| int_one = sK2_skl ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f183,f195,f198]) ).
fof(f218,plain,
( sQ11_spl
| n = sK1_skl
| ~ int_leq(n,sK1_skl) ),
inference(resolution,[status(thm)],[f190,f17]) ).
fof(f219,definition,
( sQ16_spl
<=> int_leq(n,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f221,plain,
( sQ16_spl
| ~ int_leq(n,sK1_skl) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,plain,
( sQ11_spl
| sQ12_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f218,f219,f191,f188]) ).
fof(f230,definition,
( sQ17_spl
<=> int_leq(n,int_one) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( ~ sQ17_spl
| int_leq(n,int_one) ),
inference(component_clause,[status(thm)],[f230]) ).
fof(f232,plain,
( sQ17_spl
| ~ int_leq(n,int_one) ),
inference(component_clause,[status(thm)],[f230]) ).
fof(f233,definition,
( sQ18_spl
<=> n = int_one ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ18_spl
| n = int_one ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f250,definition,
( sQ19_spl
<=> int_less(int_zero,int_one) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f252,plain,
( sQ19_spl
| ~ int_less(int_zero,int_one) ),
inference(component_clause,[status(thm)],[f250]) ).
fof(f259,definition,
( sQ20_spl
<=> int_leq(n,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( ~ sQ20_spl
| int_leq(n,int_zero) ),
inference(component_clause,[status(thm)],[f259]) ).
fof(f261,plain,
( sQ20_spl
| ~ int_leq(n,int_zero) ),
inference(component_clause,[status(thm)],[f259]) ).
fof(f262,definition,
( sQ21_spl
<=> n = int_zero ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( ~ sQ21_spl
| n = int_zero ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f274,plain,
( ~ sQ21_spl
| ~ int_less(int_one,n) ),
inference(backward_demodulation,[status(thm)],[f263,f82]) ).
fof(f280,plain,
( sQ16_spl
| int_less(sK1_skl,n) ),
inference(resolution,[status(thm)],[f221,f25]) ).
fof(f282,plain,
( sQ20_spl
| ~ sQ21_spl
| ~ int_leq(n,n) ),
inference(forward_demodulation,[status(thm)],[f263,f261]) ).
fof(f283,plain,
( sQ20_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f282,f51]) ).
fof(f284,plain,
( sQ20_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f283]) ).
fof(f318,plain,
( ~ sQ1_spl
| int_less(sK2_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f67,f48]) ).
fof(f319,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f318,f52]) ).
fof(f320,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f319]) ).
fof(f327,plain,
( sQ17_spl
| int_less(int_one,n) ),
inference(resolution,[status(thm)],[f232,f25]) ).
fof(f371,definition,
( sQ24_spl
<=> int_less(int_zero,n) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( sQ24_spl
| ~ int_less(int_zero,n) ),
inference(component_clause,[status(thm)],[f371]) ).
fof(f377,plain,
plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)) = sK1_skl,
inference(resolution,[status(thm)],[f48,f34]) ).
fof(f382,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(f387,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,f382]) ).
fof(f389,plain,
int_less(int_zero,sK2_skl),
inference(resolution,[status(thm)],[f40,f47]) ).
fof(f390,plain,
! [X0] :
( int_less(X0,int_one)
| int_less(int_zero,X0) ),
inference(resolution,[status(thm)],[f40,f25]) ).
fof(f391,plain,
! [X0] :
( ~ int_less(int_one,X0)
| int_less(int_zero,X0) ),
inference(resolution,[status(thm)],[f40,f18]) ).
fof(f407,plain,
( sQ24_spl
| int_zero = n
| ~ int_leq(int_zero,n) ),
inference(resolution,[status(thm)],[f373,f17]) ).
fof(f408,definition,
( sQ25_spl
<=> int_leq(int_zero,n) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f409,plain,
( ~ sQ25_spl
| int_leq(int_zero,n) ),
inference(component_clause,[status(thm)],[f408]) ).
fof(f410,plain,
( sQ25_spl
| ~ int_leq(int_zero,n) ),
inference(component_clause,[status(thm)],[f408]) ).
fof(f411,plain,
( sQ24_spl
| sQ21_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f407,f408,f262,f371]) ).
fof(f412,plain,
( sQ20_spl
| int_less(int_zero,n) ),
inference(resolution,[status(thm)],[f261,f25]) ).
fof(f413,plain,
( sQ20_spl
| ~ int_less(n,int_zero) ),
inference(resolution,[status(thm)],[f261,f18]) ).
fof(f414,plain,
plus(int_zero,sK0_skl(sK2_skl,int_zero)) = sK2_skl,
inference(resolution,[status(thm)],[f389,f34]) ).
fof(f416,plain,
! [X0] :
( ~ int_less(X0,int_zero)
| ~ int_less(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f389,f59]) ).
fof(f418,plain,
~ int_less(sK2_skl,int_zero),
inference(resolution,[status(thm)],[f389,f57]) ).
fof(f419,plain,
sK0_skl(sK2_skl,int_zero) = sK2_skl,
inference(forward_demodulation,[status(thm)],[f105,f414]) ).
fof(f421,plain,
( sQ25_spl
| int_less(n,int_zero) ),
inference(resolution,[status(thm)],[f410,f25]) ).
fof(f423,plain,
! [X0,X1] :
( a(plus(sK2_skl,X1),sK2_skl) = real_zero
| ~ int_leq(sK2_skl,X0)
| ~ 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(resolution,[status(thm)],[f54,f47]) ).
fof(f446,plain,
( sK2_skl = int_zero
| ~ int_leq(sK2_skl,int_zero) ),
inference(resolution,[status(thm)],[f418,f17]) ).
fof(f447,definition,
( sQ26_spl
<=> int_leq(sK2_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f450,definition,
( sQ27_spl
<=> sK2_skl = int_zero ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( ~ sQ27_spl
| sK2_skl = int_zero ),
inference(component_clause,[status(thm)],[f450]) ).
fof(f453,plain,
( sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f446,f447,f450]) ).
fof(f455,plain,
( ~ sQ27_spl
| int_less(int_zero,int_zero) ),
inference(backward_demodulation,[status(thm)],[f451,f389]) ).
fof(f465,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f455,f52]) ).
fof(f466,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f465]) ).
fof(f467,plain,
( sQ25_spl
| sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f421,f413]) ).
fof(f468,plain,
( sQ25_spl
| sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f467]) ).
fof(f469,plain,
( ~ sQ21_spl
| sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f274,f327]) ).
fof(f470,plain,
( ~ sQ21_spl
| sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f469]) ).
fof(f479,plain,
! [X0,X1,X2] :
( ~ int_less(X2,X1)
| int_less(X0,plus(X0,sK0_skl(X1,X2))) ),
inference(resolution,[status(thm)],[f53,f35]) ).
fof(f481,plain,
! [X0,X1,X2] :
( ~ int_less(X2,X1)
| ~ int_less(int_zero,X2)
| int_less(X0,plus(X0,X1)) ),
inference(resolution,[status(thm)],[f53,f22]) ).
fof(f482,plain,
! [X0,X1] :
( int_zero = X1
| ~ int_leq(int_zero,X1)
| int_less(X0,plus(X0,X1)) ),
inference(resolution,[status(thm)],[f53,f17]) ).
fof(f488,plain,
plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)) = sK1_skl,
inference(resolution,[status(thm)],[f48,f34]) ).
fof(f492,plain,
~ int_less(sK1_skl,sK2_skl),
inference(resolution,[status(thm)],[f48,f57]) ).
fof(f493,plain,
! [X0] : int_less(X0,plus(X0,sK2_skl)),
inference(resolution,[status(thm)],[f389,f53]) ).
fof(f556,plain,
( ~ sQ12_spl
| ~ int_less(n,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f492]) ).
fof(f558,plain,
( ~ sQ12_spl
| n = sK2_skl
| ~ int_leq(n,sK2_skl) ),
inference(resolution,[status(thm)],[f556,f17]) ).
fof(f559,definition,
( sQ31_spl
<=> int_leq(n,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f561,plain,
( sQ31_spl
| ~ int_leq(n,sK2_skl) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,definition,
( sQ32_spl
<=> n = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f563,plain,
( ~ sQ32_spl
| n = sK2_skl ),
inference(component_clause,[status(thm)],[f562]) ).
fof(f565,plain,
( ~ sQ12_spl
| sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f558,f559,f562,f191]) ).
fof(f583,plain,
( sQ4_spl
| ~ sQ18_spl
| ~ int_leq(n,int_zero) ),
inference(backward_demodulation,[status(thm)],[f234,f98]) ).
fof(f604,plain,
( sQ20_spl
| plus(int_zero,sK0_skl(n,int_zero)) = n ),
inference(resolution,[status(thm)],[f412,f34]) ).
fof(f609,plain,
( sQ20_spl
| sK0_skl(n,int_zero) = n ),
inference(forward_demodulation,[status(thm)],[f105,f604]) ).
fof(f615,plain,
! [X0,X1] :
( ~ sQ25_spl
| int_zero = n
| int_leq(plus(int_zero,X0),plus(n,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f409,f139]) ).
fof(f617,plain,
( ~ sQ25_spl
| int_zero = n
| ~ int_less(n,int_zero) ),
inference(resolution,[status(thm)],[f409,f60]) ).
fof(f618,definition,
! [X0,X1] :
( sQ33_spl
<=> ( int_leq(plus(int_zero,X0),plus(n,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f621,plain,
( ~ sQ25_spl
| sQ21_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f615,f618,f262,f408]) ).
fof(f623,definition,
( sQ34_spl
<=> int_less(n,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( ~ sQ25_spl
| sQ21_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f617,f623,f262,f408]) ).
fof(f650,plain,
! [X0] :
( ~ int_less(X0,sK2_skl)
| ~ int_less(sK1_skl,X0) ),
inference(resolution,[status(thm)],[f492,f22]) ).
fof(f677,plain,
! [X0,X1] :
( a(int_one,plus(int_one,X1)) = lu(int_one,plus(int_one,X1))
| ~ int_leq(int_one,X0)
| ~ int_leq(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)],[f55,f51]) ).
fof(f683,plain,
! [X0,X1] :
( a(int_one,plus(int_one,X1)) = lu(int_one,plus(int_one,X1))
| ~ int_leq(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(duplicate_literals_removal,[status(thm)],[f677]) ).
fof(f691,plain,
( sQ31_spl
| int_less(sK2_skl,n) ),
inference(resolution,[status(thm)],[f561,f25]) ).
fof(f692,plain,
( sQ31_spl
| ~ int_less(n,sK2_skl) ),
inference(resolution,[status(thm)],[f561,f18]) ).
fof(f744,plain,
( sQ20_spl
| int_leq(int_one,n) ),
inference(resolution,[status(thm)],[f39,f412]) ).
fof(f747,plain,
! [X0] :
( int_zero = X0
| ~ int_leq(int_zero,X0)
| int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f39,f17]) ).
fof(f752,plain,
int_leq(int_one,plus(int_one,sK2_skl)),
inference(resolution,[status(thm)],[f140,f47]) ).
fof(f757,plain,
! [X0] : int_leq(X0,plus(int_one,X0)),
inference(resolution,[status(thm)],[f140,f51]) ).
fof(f763,plain,
! [X0,X1] :
( sQ20_spl
| int_one = n
| int_leq(plus(int_one,X0),plus(n,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f744,f139]) ).
fof(f765,plain,
( sQ20_spl
| int_one = n
| ~ int_less(n,int_one) ),
inference(resolution,[status(thm)],[f744,f60]) ).
fof(f766,definition,
! [X0,X1] :
( sQ35_spl
<=> ( int_leq(plus(int_one,X0),plus(n,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( sQ20_spl
| sQ18_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f763,f766,f233,f259]) ).
fof(f770,definition,
( sQ36_spl
<=> int_less(n,int_one) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f772,plain,
( sQ36_spl
| ~ int_less(n,int_one) ),
inference(component_clause,[status(thm)],[f770]) ).
fof(f773,plain,
( sQ20_spl
| sQ18_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f765,f770,f233,f259]) ).
fof(f775,plain,
( sQ36_spl
| n = int_one
| ~ int_leq(n,int_one) ),
inference(resolution,[status(thm)],[f772,f17]) ).
fof(f776,plain,
( sQ36_spl
| sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f775,f230,f233,f770]) ).
fof(f791,plain,
( sQ4_spl
| ~ sQ18_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f583,f259,f233,f96]) ).
fof(f798,plain,
( ~ sQ21_spl
| ~ int_less(sK2_skl,n) ),
inference(backward_demodulation,[status(thm)],[f263,f418]) ).
fof(f806,plain,
( ~ sQ21_spl
| sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f798,f691]) ).
fof(f807,plain,
( ~ sQ21_spl
| sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f806]) ).
fof(f835,definition,
( sQ39_spl
<=> int_leq(int_one,n) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f837,plain,
( sQ39_spl
| ~ int_leq(int_one,n) ),
inference(component_clause,[status(thm)],[f835]) ).
fof(f849,plain,
( ~ sQ21_spl
| ~ int_less(sK2_skl,n) ),
inference(forward_demodulation,[status(thm)],[f263,f418]) ).
fof(f851,plain,
( ~ sQ21_spl
| sK2_skl = n
| ~ int_leq(sK2_skl,n) ),
inference(resolution,[status(thm)],[f849,f17]) ).
fof(f852,definition,
( sQ40_spl
<=> int_leq(sK2_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f853,plain,
( ~ sQ40_spl
| int_leq(sK2_skl,n) ),
inference(component_clause,[status(thm)],[f852]) ).
fof(f854,plain,
( sQ40_spl
| ~ int_leq(sK2_skl,n) ),
inference(component_clause,[status(thm)],[f852]) ).
fof(f855,plain,
( ~ sQ21_spl
| sQ32_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f851,f852,f562,f262]) ).
fof(f905,plain,
( ~ sQ17_spl
| n = int_one
| plus(n,sK0_skl(int_one,n)) = int_one ),
inference(resolution,[status(thm)],[f231,f146]) ).
fof(f908,plain,
! [X0,X1] :
( ~ sQ17_spl
| n = int_one
| int_leq(plus(n,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f231,f139]) ).
fof(f910,plain,
( ~ sQ17_spl
| n = int_one
| ~ int_less(int_one,n) ),
inference(resolution,[status(thm)],[f231,f60]) ).
fof(f911,definition,
( sQ41_spl
<=> plus(n,sK0_skl(int_one,n)) = int_one ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f914,plain,
( ~ sQ17_spl
| sQ18_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f905,f911,f233,f230]) ).
fof(f916,definition,
! [X0,X1] :
( sQ42_spl
<=> ( int_leq(plus(n,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f919,plain,
( ~ sQ17_spl
| sQ18_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f908,f916,f233,f230]) ).
fof(f921,definition,
( sQ43_spl
<=> int_less(int_one,n) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( sQ43_spl
| ~ int_less(int_one,n) ),
inference(component_clause,[status(thm)],[f921]) ).
fof(f924,plain,
( ~ sQ17_spl
| sQ18_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f910,f921,f233,f230]) ).
fof(f971,plain,
! [X0,X1] :
( X1 = X0
| ~ int_leq(X1,X0)
| int_less(int_zero,sK0_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f35,f17]) ).
fof(f991,plain,
( ~ sQ25_spl
| int_zero = n
| plus(int_zero,sK0_skl(n,int_zero)) = n ),
inference(resolution,[status(thm)],[f409,f146]) ).
fof(f996,definition,
( sQ47_spl
<=> plus(int_zero,sK0_skl(n,int_zero)) = n ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f999,plain,
( ~ sQ25_spl
| sQ21_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f991,f996,f262,f408]) ).
fof(f1036,plain,
plus(int_zero,sK0_skl(int_one,int_zero)) = int_one,
inference(resolution,[status(thm)],[f26,f34]) ).
fof(f1041,plain,
sK0_skl(int_one,int_zero) = int_one,
inference(forward_demodulation,[status(thm)],[f105,f1036]) ).
fof(f1057,plain,
( sQ20_spl
| int_one = n
| plus(int_one,sK0_skl(n,int_one)) = n ),
inference(resolution,[status(thm)],[f744,f146]) ).
fof(f1062,definition,
( sQ48_spl
<=> plus(int_one,sK0_skl(n,int_one)) = n ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1065,plain,
( sQ20_spl
| sQ18_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1057,f1062,f233,f259]) ).
fof(f1086,plain,
plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)) = sK1_skl,
inference(resolution,[status(thm)],[f48,f34]) ).
fof(f1118,plain,
( ~ sQ20_spl
| int_leq(n,plus(int_one,int_zero)) ),
inference(resolution,[status(thm)],[f260,f140]) ).
fof(f1126,plain,
( ~ sQ20_spl
| int_leq(n,int_one) ),
inference(forward_demodulation,[status(thm)],[f28,f1118]) ).
fof(f1127,plain,
( ~ sQ20_spl
| sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1126,f232]) ).
fof(f1128,plain,
( ~ sQ20_spl
| sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f1127]) ).
fof(f1228,plain,
int_less(int_zero,plus(int_one,int_one)),
inference(resolution,[status(thm)],[f757,f40]) ).
fof(f1235,plain,
int_leq(int_zero,int_one),
inference(paramodulation,[status(thm)],[f28,f757]) ).
fof(f1236,plain,
! [X0] : int_leq(X0,plus(X0,int_one)),
inference(paramodulation,[status(thm)],[f27,f757]) ).
fof(f1244,plain,
( int_zero = int_one
| plus(int_zero,sK0_skl(int_one,int_zero)) = int_one ),
inference(resolution,[status(thm)],[f1235,f146]) ).
fof(f1245,plain,
int_leq(int_zero,plus(int_one,int_one)),
inference(resolution,[status(thm)],[f1235,f140]) ).
fof(f1246,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)],[f1235,f139]) ).
fof(f1250,definition,
( sQ50_spl
<=> plus(int_zero,sK0_skl(int_one,int_zero)) = int_one ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1253,plain,
( sQ5_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1244,f1250,f99]) ).
fof(f1254,definition,
! [X0,X1] :
( sQ51_spl
<=> ( int_leq(plus(int_zero,X0),plus(int_one,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1257,plain,
( sQ5_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1246,f1254,f99]) ).
fof(f1259,definition,
( sQ52_spl
<=> int_less(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1269,plain,
( sQ20_spl
| sK0_skl(n,int_zero) = n ),
inference(resolution,[status(thm)],[f148,f744]) ).
fof(f1275,plain,
( sK0_skl(sK2_skl,int_zero) = sK0_skl(sK2_skl,int_zero)
| ~ int_less(int_zero,sK2_skl) ),
inference(paramodulation,[status(thm)],[f419,f154]) ).
fof(f1276,plain,
( sK0_skl(int_one,int_zero) = sK0_skl(int_one,int_zero)
| ~ int_less(int_zero,int_one) ),
inference(paramodulation,[status(thm)],[f147,f154]) ).
fof(f1277,definition,
( sQ53_spl
<=> int_less(int_zero,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1279,plain,
( sQ53_spl
| ~ int_less(int_zero,sK2_skl) ),
inference(component_clause,[status(thm)],[f1277]) ).
fof(f1280,definition,
( sQ54_spl
<=> sK0_skl(sK2_skl,int_zero) = sK0_skl(sK2_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f1283,plain,
( sQ54_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f1275,f1277,f1280]) ).
fof(f1284,definition,
( sQ55_spl
<=> sK0_skl(int_one,int_zero) = sK0_skl(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1287,plain,
( sQ55_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1276,f250,f1284]) ).
fof(f1288,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f252,f26]) ).
fof(f1289,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1288]) ).
fof(f1290,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1279,f389]) ).
fof(f1291,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f1290]) ).
fof(f1293,definition,
( sQ56_spl
<=> sK0_skl(n,int_zero) = sK0_skl(n,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1348,plain,
( ~ sQ5_spl
| int_less(int_one,int_one) ),
inference(backward_demodulation,[status(thm)],[f100,f26]) ).
fof(f1362,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1348,f52]) ).
fof(f1363,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f1362]) ).
fof(f1364,plain,
( sQ40_spl
| int_less(n,sK2_skl) ),
inference(resolution,[status(thm)],[f854,f25]) ).
fof(f1366,plain,
( sQ40_spl
| sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1364,f692]) ).
fof(f1367,plain,
( sQ40_spl
| sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f1366]) ).
fof(f1475,plain,
! [X0,X1,X2] :
( ~ int_less(plus(X0,X1),n)
| a(X2,plus(X2,X1)) = lu(X2,plus(X2,X1))
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_leq(int_zero,X1)
| ~ int_leq(int_one,plus(X0,X1))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(resolution,[status(thm)],[f55,f18]) ).
fof(f1477,plain,
! [X0,X1] :
( a(X1,plus(X1,int_zero)) = lu(X1,plus(X1,int_zero))
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(int_zero,int_zero)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,plus(X0,int_zero))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(paramodulation,[status(thm)],[f28,f55]) ).
fof(f1484,definition,
! [X0,X1] :
( sQ65_spl
<=> ( a(X1,plus(X1,int_zero)) = lu(X1,plus(X1,int_zero))
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,plus(X0,int_zero))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1487,definition,
( sQ66_spl
<=> int_leq(int_zero,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1489,plain,
( sQ66_spl
| ~ int_leq(int_zero,int_zero) ),
inference(component_clause,[status(thm)],[f1487]) ).
fof(f1490,plain,
( ~ sQ66_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f1477,f1484,f1487]) ).
fof(f1495,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1489,f51]) ).
fof(f1496,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f1495]) ).
fof(f1502,plain,
( ~ sQ40_spl
| sK2_skl = n
| ~ int_less(n,sK2_skl) ),
inference(resolution,[status(thm)],[f853,f60]) ).
fof(f1511,definition,
( sQ69_spl
<=> int_less(n,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1513,plain,
( sQ69_spl
| ~ int_less(n,sK2_skl) ),
inference(component_clause,[status(thm)],[f1511]) ).
fof(f1514,plain,
( ~ sQ40_spl
| sQ32_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f1502,f1511,f562,f852]) ).
fof(f1582,plain,
! [X0] :
( ~ int_less(int_zero,int_zero)
| int_less(X0,X0) ),
inference(paramodulation,[status(thm)],[f28,f53]) ).
fof(f1585,definition,
! [X0] :
( sQ70_spl
<=> int_less(X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1586,plain,
! [X0] :
( ~ sQ70_spl
| int_less(X0,X0) ),
inference(component_clause,[status(thm)],[f1585]) ).
fof(f1588,plain,
( ~ sQ3_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1582,f1585,f87]) ).
fof(f1589,plain,
( ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1586,f52]) ).
fof(f1590,plain,
~ sQ70_spl,
inference(contradiction_clause,[status(thm)],[f1589]) ).
fof(f1617,plain,
( ~ int_less(int_zero,sK0_skl(sK1_skl,sK2_skl))
| int_less(sK2_skl,sK1_skl) ),
inference(paramodulation,[status(thm)],[f488,f53]) ).
fof(f1620,definition,
( sQ71_spl
<=> int_less(sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1623,plain,
( ~ sQ8_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1617,f1620,f162]) ).
fof(f1624,definition,
( sQ72_spl
<=> int_leq(int_one,plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl))) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1626,plain,
( sQ72_spl
| ~ int_leq(int_one,plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl))) ),
inference(component_clause,[status(thm)],[f1624]) ).
fof(f1627,definition,
( sQ73_spl
<=> int_leq(sK1_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1629,plain,
( sQ73_spl
| ~ int_leq(sK1_skl,n) ),
inference(component_clause,[status(thm)],[f1627]) ).
fof(f1638,plain,
( sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1629,f49]) ).
fof(f1639,plain,
sQ73_spl,
inference(contradiction_clause,[status(thm)],[f1638]) ).
fof(f1640,plain,
( sQ72_spl
| ~ int_leq(int_one,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f488,f1626]) ).
fof(f1641,plain,
( sQ72_spl
| ~ int_less(int_zero,sK1_skl) ),
inference(resolution,[status(thm)],[f1640,f39]) ).
fof(f1647,plain,
( sQ72_spl
| int_zero = sK1_skl
| ~ int_leq(int_zero,sK1_skl) ),
inference(resolution,[status(thm)],[f1641,f17]) ).
fof(f1648,definition,
( sQ76_spl
<=> int_leq(int_zero,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1650,plain,
( sQ76_spl
| ~ int_leq(int_zero,sK1_skl) ),
inference(component_clause,[status(thm)],[f1648]) ).
fof(f1651,definition,
( sQ77_spl
<=> int_zero = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1652,plain,
( ~ sQ77_spl
| int_zero = sK1_skl ),
inference(component_clause,[status(thm)],[f1651]) ).
fof(f1654,plain,
( sQ72_spl
| sQ77_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f1647,f1648,f1651,f1624]) ).
fof(f1656,plain,
( ~ sQ77_spl
| int_less(sK2_skl,int_zero) ),
inference(backward_demodulation,[status(thm)],[f1652,f48]) ).
fof(f1666,plain,
( ~ sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1656,f418]) ).
fof(f1667,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f1666]) ).
fof(f1669,plain,
( sQ76_spl
| ~ int_less(int_zero,sK1_skl) ),
inference(resolution,[status(thm)],[f1650,f18]) ).
fof(f1708,plain,
( sQ76_spl
| ~ int_less(int_one,sK1_skl) ),
inference(resolution,[status(thm)],[f1669,f391]) ).
fof(f1713,plain,
( sQ20_spl
| sK0_skl(n,int_zero) = sK0_skl(n,int_zero)
| ~ int_less(int_zero,n) ),
inference(paramodulation,[status(thm)],[f609,f387]) ).
fof(f1715,plain,
( sQ20_spl
| sQ56_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1713,f371,f1293,f259]) ).
fof(f1721,plain,
( sQ76_spl
| int_one = sK1_skl
| ~ int_leq(int_one,sK1_skl) ),
inference(resolution,[status(thm)],[f1708,f17]) ).
fof(f1722,definition,
( sQ78_spl
<=> int_leq(int_one,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1724,plain,
( sQ78_spl
| ~ int_leq(int_one,sK1_skl) ),
inference(component_clause,[status(thm)],[f1722]) ).
fof(f1725,definition,
( sQ79_spl
<=> int_one = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1726,plain,
( ~ sQ79_spl
| int_one = sK1_skl ),
inference(component_clause,[status(thm)],[f1725]) ).
fof(f1728,plain,
( sQ76_spl
| sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f1721,f1722,f1725,f1648]) ).
fof(f1739,plain,
( sQ0_spl
| ~ sQ79_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f1726,f65]) ).
fof(f1757,plain,
( sQ43_spl
| int_one = n
| ~ int_leq(int_one,n) ),
inference(resolution,[status(thm)],[f923,f17]) ).
fof(f1758,plain,
( sQ43_spl
| sQ18_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1757,f835,f233,f921]) ).
fof(f1759,plain,
( sQ25_spl
| int_less(n,int_zero) ),
inference(resolution,[status(thm)],[f410,f25]) ).
fof(f1791,plain,
( sQ78_spl
| ~ int_less(int_zero,sK1_skl) ),
inference(resolution,[status(thm)],[f1724,f39]) ).
fof(f1809,definition,
( sQ82_spl
<=> int_less(sK1_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1811,plain,
( sQ82_spl
| ~ int_less(sK1_skl,int_zero) ),
inference(component_clause,[status(thm)],[f1809]) ).
fof(f1831,plain,
( sQ39_spl
| ~ int_less(int_zero,n) ),
inference(resolution,[status(thm)],[f837,f39]) ).
fof(f1834,plain,
( sQ39_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1831,f371,f835]) ).
fof(f1991,plain,
( sQ82_spl
| sK1_skl = int_zero
| ~ int_leq(sK1_skl,int_zero) ),
inference(resolution,[status(thm)],[f1811,f17]) ).
fof(f1992,definition,
( sQ93_spl
<=> int_leq(sK1_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1994,plain,
( sQ93_spl
| ~ int_leq(sK1_skl,int_zero) ),
inference(component_clause,[status(thm)],[f1992]) ).
fof(f1995,plain,
( sQ82_spl
| sQ77_spl
| ~ sQ93_spl ),
inference(split_clause,[status(thm)],[f1991,f1992,f1651,f1809]) ).
fof(f2029,plain,
( sQ93_spl
| int_less(int_zero,sK1_skl) ),
inference(resolution,[status(thm)],[f1994,f25]) ).
fof(f2059,plain,
! [X0] :
( ~ int_less(int_zero,int_one)
| int_less(X0,plus(X0,int_one)) ),
inference(paramodulation,[status(thm)],[f1041,f479]) ).
fof(f2060,definition,
! [X0] :
( sQ99_spl
<=> int_less(X0,plus(X0,int_one)) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2063,plain,
( ~ sQ19_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f2059,f2060,f250]) ).
fof(f2089,definition,
( sQ101_spl
<=> int_leq(n,n) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f2091,plain,
( sQ101_spl
| ~ int_leq(n,n) ),
inference(component_clause,[status(thm)],[f2089]) ).
fof(f2095,plain,
( sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2091,f51]) ).
fof(f2096,plain,
sQ101_spl,
inference(contradiction_clause,[status(thm)],[f2095]) ).
fof(f2106,plain,
( sQ93_spl
| sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2029,f1791]) ).
fof(f2107,plain,
( sQ93_spl
| sQ78_spl ),
inference(contradiction_clause,[status(thm)],[f2106]) ).
fof(f2115,plain,
! [X0,X1] :
( ~ int_less(X1,int_zero)
| ~ int_less(int_zero,X1)
| int_less(X0,X0) ),
inference(paramodulation,[status(thm)],[f28,f481]) ).
fof(f2118,definition,
! [X1] :
( sQ102_spl
<=> ( ~ int_less(X1,int_zero)
| ~ int_less(int_zero,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f2121,plain,
( sQ102_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f2115,f1585,f2118]) ).
fof(f2124,plain,
! [X0] :
( int_zero = plus(int_one,int_zero)
| int_less(X0,plus(X0,plus(int_one,int_zero))) ),
inference(resolution,[status(thm)],[f482,f757]) ).
fof(f2128,definition,
! [X0] :
( sQ103_spl
<=> int_less(X0,plus(X0,n)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f2133,definition,
! [X0] :
( sQ104_spl
<=> int_less(X0,plus(X0,plus(int_one,int_zero))) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f2136,definition,
( sQ105_spl
<=> int_zero = plus(int_one,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f2137,plain,
( ~ sQ105_spl
| int_zero = plus(int_one,int_zero) ),
inference(component_clause,[status(thm)],[f2136]) ).
fof(f2139,plain,
( sQ105_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f2124,f2133,f2136]) ).
fof(f2140,definition,
! [X0] :
( sQ106_spl
<=> int_less(X0,plus(X0,int_zero)) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f2141,plain,
! [X0] :
( ~ sQ106_spl
| int_less(X0,plus(X0,int_zero)) ),
inference(component_clause,[status(thm)],[f2140]) ).
fof(f2143,definition,
( sQ107_spl
<=> int_zero = int_zero ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f2147,plain,
! [X0] :
( ~ sQ106_spl
| int_less(X0,X0) ),
inference(forward_demodulation,[status(thm)],[f28,f2141]) ).
fof(f2148,plain,
( ~ sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2147,f52]) ).
fof(f2149,plain,
~ sQ106_spl,
inference(contradiction_clause,[status(thm)],[f2148]) ).
fof(f2151,plain,
( ~ sQ105_spl
| int_zero = int_one ),
inference(forward_demodulation,[status(thm)],[f28,f2137]) ).
fof(f2152,plain,
( ~ sQ105_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2151,f101]) ).
fof(f2153,plain,
( ~ sQ105_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f2152]) ).
fof(f2278,definition,
! [X0] :
( sQ118_spl
<=> int_less(X0,plus(X0,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f2394,plain,
! [X0] :
( int_zero = plus(int_zero,int_one)
| int_less(X0,plus(X0,plus(int_zero,int_one))) ),
inference(resolution,[status(thm)],[f1236,f482]) ).
fof(f2417,definition,
! [X0] :
( sQ122_spl
<=> int_less(X0,plus(X0,plus(int_zero,int_one))) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f2420,definition,
( sQ123_spl
<=> int_zero = plus(int_zero,int_one) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f2421,plain,
( ~ sQ123_spl
| int_zero = plus(int_zero,int_one) ),
inference(component_clause,[status(thm)],[f2420]) ).
fof(f2423,plain,
( sQ123_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f2394,f2417,f2420]) ).
fof(f2464,plain,
! [X0] :
( ~ int_less(int_zero,n)
| a(int_one,plus(int_one,X0)) = lu(int_one,plus(int_one,X0))
| ~ int_leq(int_zero,X0)
| ~ int_leq(plus(int_one,X0),n)
| ~ int_leq(int_one,plus(int_one,X0))
| ~ int_leq(int_one,int_one) ),
inference(resolution,[status(thm)],[f683,f39]) ).
fof(f2467,plain,
! [X0] :
( a(int_one,plus(int_one,X0)) = lu(int_one,plus(int_one,X0))
| ~ int_leq(int_zero,X0)
| ~ int_leq(plus(n,X0),n)
| ~ int_leq(int_one,plus(n,X0))
| ~ int_leq(int_one,n) ),
inference(resolution,[status(thm)],[f683,f51]) ).
fof(f2476,definition,
( sQ132_spl
<=> int_leq(int_one,int_one) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f2478,plain,
( sQ132_spl
| ~ int_leq(int_one,int_one) ),
inference(component_clause,[status(thm)],[f2476]) ).
fof(f2479,definition,
! [X0] :
( sQ133_spl
<=> ( a(int_one,plus(int_one,X0)) = lu(int_one,plus(int_one,X0))
| ~ int_leq(int_zero,X0)
| ~ int_leq(plus(int_one,X0),n)
| ~ int_leq(int_one,plus(int_one,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f2482,plain,
( ~ sQ24_spl
| sQ133_spl
| ~ sQ132_spl ),
inference(split_clause,[status(thm)],[f2464,f2476,f2479,f371]) ).
fof(f2483,definition,
! [X0] :
( sQ134_spl
<=> ( a(int_one,plus(int_one,X0)) = lu(int_one,plus(int_one,X0))
| ~ int_leq(int_zero,X0)
| ~ int_leq(plus(n,X0),n)
| ~ int_leq(int_one,plus(n,X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f2486,plain,
( sQ134_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f2467,f835,f2483]) ).
fof(f2522,plain,
( int_less(sK2_skl,int_one)
| ~ int_less(sK1_skl,int_zero) ),
inference(resolution,[status(thm)],[f61,f390]) ).
fof(f2530,plain,
( sQ13_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f2522,f1809,f195]) ).
fof(f2532,plain,
( ~ int_less(int_one,int_zero)
| ~ int_less(int_one,int_zero) ),
inference(resolution,[status(thm)],[f81,f391]) ).
fof(f2536,plain,
~ sQ52_spl,
inference(split_clause,[status(thm)],[f2532,f1259]) ).
fof(f2561,plain,
( sQ132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2478,f51]) ).
fof(f2562,plain,
sQ132_spl,
inference(contradiction_clause,[status(thm)],[f2561]) ).
fof(f2565,plain,
( int_zero = plus(int_one,int_zero)
| int_leq(int_one,plus(int_one,int_zero)) ),
inference(resolution,[status(thm)],[f747,f757]) ).
fof(f2566,plain,
( int_zero = plus(int_zero,int_one)
| int_leq(int_one,plus(int_zero,int_one)) ),
inference(resolution,[status(thm)],[f747,f1236]) ).
fof(f2569,plain,
( int_zero = int_zero
| int_leq(int_one,int_zero) ),
inference(resolution,[status(thm)],[f747,f51]) ).
fof(f2572,definition,
( sQ137_spl
<=> int_leq(int_one,plus(int_one,int_zero)) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f2575,plain,
( sQ105_spl
| sQ137_spl ),
inference(split_clause,[status(thm)],[f2565,f2572,f2136]) ).
fof(f2576,definition,
( sQ138_spl
<=> int_leq(int_one,plus(int_zero,int_one)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f2579,plain,
( sQ123_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f2566,f2576,f2420]) ).
fof(f2580,plain,
( sQ107_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f2569,f96,f2143]) ).
fof(f2581,plain,
( ~ sQ123_spl
| int_zero = int_one ),
inference(forward_demodulation,[status(thm)],[f105,f2421]) ).
fof(f2582,plain,
( ~ sQ123_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2581,f101]) ).
fof(f2583,plain,
( ~ sQ123_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f2582]) ).
fof(f2587,plain,
( sQ25_spl
| ~ int_less(sK2_skl,n) ),
inference(resolution,[status(thm)],[f416,f1759]) ).
fof(f2592,plain,
( sQ25_spl
| sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2587,f691]) ).
fof(f2593,plain,
( sQ25_spl
| sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f2592]) ).
fof(f2594,definition,
( sQ139_spl
<=> int_less(sK2_skl,int_zero) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f2710,plain,
( ~ sQ13_spl
| ~ sQ14_spl
| int_less(int_one,int_one) ),
inference(forward_demodulation,[status(thm)],[f199,f196]) ).
fof(f2711,plain,
( ~ sQ13_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2710,f52]) ).
fof(f2712,plain,
( ~ sQ13_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f2711]) ).
fof(f2782,plain,
! [X0] :
( sQ20_spl
| ~ int_less(int_zero,n)
| int_less(X0,plus(X0,n)) ),
inference(paramodulation,[status(thm)],[f1269,f479]) ).
fof(f2786,plain,
( sQ20_spl
| ~ sQ24_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f2782,f2128,f371,f259]) ).
fof(f2914,plain,
( sQ0_spl
| ~ sQ79_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1739,f165,f1725,f63]) ).
fof(f2972,definition,
( sQ151_spl
<=> int_zero = sK0_skl(sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2973,plain,
( ~ sQ151_spl
| int_zero = sK0_skl(sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f2972]) ).
fof(f3013,plain,
( sQ69_spl
| n = sK2_skl
| ~ int_leq(n,sK2_skl) ),
inference(resolution,[status(thm)],[f1513,f17]) ).
fof(f3014,plain,
( sQ69_spl
| sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f3013,f559,f562,f1511]) ).
fof(f3093,definition,
( sQ153_spl
<=> int_leq(int_zero,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f3094,plain,
( ~ sQ153_spl
| int_leq(int_zero,sK2_skl) ),
inference(component_clause,[status(thm)],[f3093]) ).
fof(f3095,plain,
( sQ153_spl
| ~ int_leq(int_zero,sK2_skl) ),
inference(component_clause,[status(thm)],[f3093]) ).
fof(f3111,plain,
( ~ sQ151_spl
| plus(sK2_skl,int_zero) = sK1_skl ),
inference(backward_demodulation,[status(thm)],[f2973,f1086]) ).
fof(f3118,plain,
( ~ sQ151_spl
| sK2_skl = sK1_skl ),
inference(forward_demodulation,[status(thm)],[f28,f3111]) ).
fof(f3119,plain,
( ~ sQ151_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3118,f68]) ).
fof(f3120,plain,
( ~ sQ151_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f3119]) ).
fof(f3121,plain,
( sQ40_spl
| ~ int_less(sK1_skl,n) ),
inference(resolution,[status(thm)],[f650,f1364]) ).
fof(f3128,plain,
( sQ40_spl
| sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3121,f280]) ).
fof(f3129,plain,
( sQ40_spl
| sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f3128]) ).
fof(f3142,plain,
( sQ0_spl
| ~ sQ32_spl
| ~ int_leq(sK1_skl,n) ),
inference(backward_demodulation,[status(thm)],[f563,f65]) ).
fof(f3155,plain,
( sQ0_spl
| ~ sQ32_spl
| ~ sQ73_spl ),
inference(split_clause,[status(thm)],[f3142,f1627,f562,f63]) ).
fof(f3333,plain,
( int_one = plus(int_one,sK2_skl)
| plus(int_one,sK0_skl(plus(int_one,sK2_skl),int_one)) = plus(int_one,sK2_skl) ),
inference(resolution,[status(thm)],[f752,f146]) ).
fof(f3335,plain,
! [X0,X1] :
( int_one = plus(int_one,sK2_skl)
| int_leq(plus(int_one,X0),plus(plus(int_one,sK2_skl),X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f752,f139]) ).
fof(f3337,plain,
( int_one = plus(int_one,sK2_skl)
| ~ int_less(plus(int_one,sK2_skl),int_one) ),
inference(resolution,[status(thm)],[f752,f60]) ).
fof(f3338,definition,
( sQ160_spl
<=> plus(int_one,sK0_skl(plus(int_one,sK2_skl),int_one)) = plus(int_one,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f3341,definition,
( sQ161_spl
<=> int_one = plus(int_one,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f3342,plain,
( ~ sQ161_spl
| int_one = plus(int_one,sK2_skl) ),
inference(component_clause,[status(thm)],[f3341]) ).
fof(f3344,plain,
( sQ161_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f3333,f3338,f3341]) ).
fof(f3345,definition,
! [X0,X1] :
( sQ162_spl
<=> ( int_leq(plus(int_one,X0),plus(plus(int_one,sK2_skl),X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f3348,plain,
( sQ161_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f3335,f3345,f3341]) ).
fof(f3349,definition,
( sQ163_spl
<=> int_less(plus(int_one,sK2_skl),int_one) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f3352,plain,
( sQ161_spl
| ~ sQ163_spl ),
inference(split_clause,[status(thm)],[f3337,f3349,f3341]) ).
fof(f3357,plain,
( ~ sQ161_spl
| int_less(int_one,int_one) ),
inference(paramodulation,[status(thm)],[f3342,f493]) ).
fof(f3376,plain,
( ~ sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3357,f52]) ).
fof(f3377,plain,
~ sQ161_spl,
inference(contradiction_clause,[status(thm)],[f3376]) ).
fof(f3445,plain,
( a(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK2_skl) = real_zero
| ~ int_leq(sK2_skl,sK2_skl)
| ~ int_less(int_zero,sK0_skl(sK1_skl,sK2_skl))
| ~ int_leq(sK2_skl,n)
| ~ int_leq(int_one,sK2_skl)
| ~ int_leq(sK1_skl,n)
| ~ int_leq(int_one,plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl))) ),
inference(paramodulation,[status(thm)],[f377,f423]) ).
fof(f3460,definition,
( sQ168_spl
<=> int_leq(sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f3462,plain,
( sQ168_spl
| ~ int_leq(sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f3460]) ).
fof(f3463,definition,
( sQ169_spl
<=> a(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK2_skl) = real_zero ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f3464,plain,
( ~ sQ169_spl
| a(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK2_skl) = real_zero ),
inference(component_clause,[status(thm)],[f3463]) ).
fof(f3466,plain,
( sQ169_spl
| ~ sQ168_spl
| ~ sQ8_spl
| ~ sQ40_spl
| ~ sQ9_spl
| ~ sQ73_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f3445,f1624,f1627,f165,f852,f162,f3460,f3463]) ).
fof(f3480,plain,
( ~ sQ169_spl
| a(sK1_skl,sK2_skl) = real_zero ),
inference(forward_demodulation,[status(thm)],[f377,f3464]) ).
fof(f3481,plain,
( ~ sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3480,f50]) ).
fof(f3482,plain,
~ sQ169_spl,
inference(contradiction_clause,[status(thm)],[f3481]) ).
fof(f3483,plain,
( sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3462,f51]) ).
fof(f3484,plain,
sQ168_spl,
inference(contradiction_clause,[status(thm)],[f3483]) ).
fof(f3583,definition,
( sQ174_spl
<=> int_zero = sK0_skl(sK1_skl,int_one) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f3584,plain,
( ~ sQ174_spl
| int_zero = sK0_skl(sK1_skl,int_one) ),
inference(component_clause,[status(thm)],[f3583]) ).
fof(f3729,plain,
! [X0,X1] :
( ~ int_less(X0,n)
| a(X1,plus(X1,int_zero)) = lu(X1,plus(X1,int_zero))
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(int_zero,int_zero)
| ~ int_leq(int_one,plus(X0,int_zero))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(paramodulation,[status(thm)],[f28,f1475]) ).
fof(f3736,definition,
! [X0,X1] :
( sQ187_spl
<=> ( ~ int_less(X0,n)
| a(X1,plus(X1,int_zero)) = lu(X1,plus(X1,int_zero))
| ~ int_leq(X1,X0)
| ~ int_leq(int_one,X1)
| ~ int_leq(int_one,plus(X0,int_zero))
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f3739,plain,
( ~ sQ66_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f3729,f3736,f1487]) ).
fof(f3745,plain,
( ~ sQ174_spl
| int_one = sK1_skl
| ~ int_leq(int_one,sK1_skl)
| int_less(int_zero,int_zero) ),
inference(paramodulation,[status(thm)],[f3584,f971]) ).
fof(f3751,plain,
( ~ sQ174_spl
| sQ79_spl
| ~ sQ78_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f3745,f87,f1722,f1725,f3583]) ).
fof(f3875,plain,
( sQ153_spl
| int_less(sK2_skl,int_zero) ),
inference(resolution,[status(thm)],[f3095,f25]) ).
fof(f3877,plain,
( sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3875,f418]) ).
fof(f3878,plain,
sQ153_spl,
inference(contradiction_clause,[status(thm)],[f3877]) ).
fof(f3883,plain,
! [X0] :
( ~ sQ153_spl
| int_zero = sK2_skl
| int_less(X0,plus(X0,sK2_skl)) ),
inference(resolution,[status(thm)],[f3094,f482]) ).
fof(f3885,plain,
( ~ sQ153_spl
| int_zero = sK2_skl
| plus(int_zero,sK0_skl(sK2_skl,int_zero)) = sK2_skl ),
inference(resolution,[status(thm)],[f3094,f146]) ).
fof(f3887,plain,
! [X0,X1] :
( ~ sQ153_spl
| int_zero = sK2_skl
| int_leq(plus(int_zero,X0),plus(sK2_skl,X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f3094,f139]) ).
fof(f3889,plain,
( ~ sQ153_spl
| int_zero = sK2_skl
| ~ int_less(sK2_skl,int_zero) ),
inference(resolution,[status(thm)],[f3094,f60]) ).
fof(f3891,plain,
( ~ sQ153_spl
| sQ27_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f3883,f2278,f450,f3093]) ).
fof(f3892,definition,
( sQ195_spl
<=> plus(int_zero,sK0_skl(sK2_skl,int_zero)) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f3895,plain,
( ~ sQ153_spl
| sQ27_spl
| sQ195_spl ),
inference(split_clause,[status(thm)],[f3885,f3892,f450,f3093]) ).
fof(f3896,definition,
! [X0,X1] :
( sQ196_spl
<=> ( int_leq(plus(int_zero,X0),plus(sK2_skl,X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f3899,plain,
( ~ sQ153_spl
| sQ27_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f3887,f3896,f450,f3093]) ).
fof(f3901,plain,
( ~ sQ153_spl
| sQ27_spl
| ~ sQ139_spl ),
inference(split_clause,[status(thm)],[f3889,f2594,f450,f3093]) ).
fof(f3924,plain,
( int_zero = plus(int_one,int_one)
| int_leq(int_one,plus(int_one,int_one)) ),
inference(resolution,[status(thm)],[f1245,f747]) ).
fof(f3927,plain,
! [X0] :
( int_zero = plus(int_one,int_one)
| int_less(X0,plus(X0,plus(int_one,int_one))) ),
inference(resolution,[status(thm)],[f1245,f482]) ).
fof(f3929,plain,
( int_zero = plus(int_one,int_one)
| plus(int_zero,sK0_skl(plus(int_one,int_one),int_zero)) = plus(int_one,int_one) ),
inference(resolution,[status(thm)],[f1245,f146]) ).
fof(f3931,plain,
! [X0,X1] :
( int_zero = plus(int_one,int_one)
| int_leq(plus(int_zero,X0),plus(plus(int_one,int_one),X1))
| ~ int_leq(X0,X1) ),
inference(resolution,[status(thm)],[f1245,f139]) ).
fof(f3933,plain,
( int_zero = plus(int_one,int_one)
| ~ int_less(plus(int_one,int_one),int_zero) ),
inference(resolution,[status(thm)],[f1245,f60]) ).
fof(f3934,definition,
( sQ197_spl
<=> int_leq(int_one,plus(int_one,int_one)) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f3937,definition,
( sQ198_spl
<=> int_zero = plus(int_one,int_one) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f3938,plain,
( ~ sQ198_spl
| int_zero = plus(int_one,int_one) ),
inference(component_clause,[status(thm)],[f3937]) ).
fof(f3940,plain,
( sQ198_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f3924,f3934,f3937]) ).
fof(f3941,definition,
! [X0] :
( sQ199_spl
<=> int_less(X0,plus(X0,plus(int_one,int_one))) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f3944,plain,
( sQ198_spl
| sQ199_spl ),
inference(split_clause,[status(thm)],[f3927,f3941,f3937]) ).
fof(f3945,definition,
( sQ200_spl
<=> plus(int_zero,sK0_skl(plus(int_one,int_one),int_zero)) = plus(int_one,int_one) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f3948,plain,
( sQ198_spl
| sQ200_spl ),
inference(split_clause,[status(thm)],[f3929,f3945,f3937]) ).
fof(f3949,definition,
! [X0,X1] :
( sQ201_spl
<=> ( int_leq(plus(int_zero,X0),plus(plus(int_one,int_one),X1))
| ~ int_leq(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f3952,plain,
( sQ198_spl
| sQ201_spl ),
inference(split_clause,[status(thm)],[f3931,f3949,f3937]) ).
fof(f3954,definition,
( sQ202_spl
<=> int_less(plus(int_one,int_one),int_zero) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f3957,plain,
( sQ198_spl
| ~ sQ202_spl ),
inference(split_clause,[status(thm)],[f3933,f3954,f3937]) ).
fof(f3961,plain,
( ~ sQ198_spl
| int_less(int_zero,int_zero) ),
inference(backward_demodulation,[status(thm)],[f3938,f1228]) ).
fof(f3984,plain,
( ~ sQ198_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3961,f52]) ).
fof(f3985,plain,
~ sQ198_spl,
inference(contradiction_clause,[status(thm)],[f3984]) ).
fof(f4095,plain,
( sQ8_spl
| ~ int_less(sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f164,f35]) ).
fof(f4104,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4095,f48]) ).
fof(f4105,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f4104]) ).
fof(f4106,plain,
$false,
inference(sat_refutation,[status(thm)],[f69,f102,f171,f173,f175,f194,f201,f222,f284,f320,f411,f453,f466,f468,f470,f565,f621,f626,f769,f773,f776,f791,f807,f855,f914,f919,f924,f999,f1065,f1128,f1253,f1257,f1283,f1287,f1289,f1291,f1363,f1367,f1490,f1496,f1514,f1588,f1590,f1623,f1639,f1654,f1667,f1715,f1728,f1758,f1834,f1995,f2063,f2096,f2107,f2121,f2139,f2149,f2153,f2423,f2482,f2486,f2530,f2536,f2562,f2575,f2579,f2580,f2583,f2593,f2712,f2786,f2914,f3014,f3120,f3129,f3155,f3344,f3348,f3352,f3377,f3466,f3482,f3484,f3739,f3751,f3878,f3891,f3895,f3899,f3901,f3940,f3944,f3948,f3952,f3957,f3985,f4105]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV487+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.54 % Computer : n014.cluster.edu
% 0.09/0.54 % Model : x86_64 x86_64
% 0.09/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.54 % Memory : 8046.5625MB
% 0.09/0.54 % OS : Linux 6.8.0-71-generic
% 0.09/0.54 % CPULimit : 300
% 0.09/0.54 % WCLimit : 300
% 0.09/0.54 % DateTime : Mon Sep 21 08:54:35 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.09/0.55 % Drodi V4.1.1
% 6.67/1.48 % Refutation found
% 6.67/1.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.67/1.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.34/1.51 % Elapsed time: 0.951439 seconds
% 0.34/1.51 % CPU time: 7.258491 seconds
% 0.34/1.51 % Total memory used: 144.256 MB
% 0.34/1.51 % Net memory used: 135.048 MB
%------------------------------------------------------------------------------