%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV487+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 19.31s 3.02s
% Output : CNFRefutation 19.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 24
% Syntax : Number of formulae : 125 ( 20 unt; 16 def)
% Number of atoms : 361 ( 55 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 395 ( 159 ~; 171 |; 36 &)
% ( 19 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 17 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 108 ( 103 !; 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(f9,axiom,
! [I,J] :
( int_less(I,J)
<=> ? [K] :
( int_less(int_zero,K)
& plus(I,K) = J ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [I] :
( int_less(int_zero,I)
<=> int_leq(int_one,I) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
! [I,J] :
( ( int_leq(J,n)
& int_leq(int_one,J)
& int_leq(I,n)
& int_leq(int_one,I) )
=> ( ! [C] :
( ( J = plus(I,C)
& int_less(int_zero,C) )
=> ! [K] :
( ( int_leq(K,I)
& int_leq(int_one,K) )
=> a(K,plus(K,C)) = real_zero ) )
& ! [K] :
( ( int_leq(K,J)
& int_leq(int_one,K) )
=> a(K,K) = real_one )
& ! [C] :
( ( I = plus(J,C)
& int_less(int_zero,C) )
=> ! [K] :
( ( int_leq(K,J)
& int_leq(int_one,K) )
=> a(plus(K,C),K) = real_zero ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,conjecture,
! [I,J] :
( ( int_leq(I,n)
& int_less(J,I)
& int_leq(int_one,J) )
=> a(I,J) = real_zero ),
file('/export/starexec/sandbox2/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(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(f37,plain,
! [I] :
( ( ~ int_leq(int_one,I)
| int_less(int_zero,I) )
& ( int_leq(int_one,I)
| ~ int_less(int_zero,I) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f38,plain,
( ! [I] :
( ~ int_leq(int_one,I)
| int_less(int_zero,I) )
& ! [I] :
( int_leq(int_one,I)
| ~ int_less(int_zero,I) ) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f39,plain,
! [X0] :
( int_leq(int_one,X0)
| ~ int_less(int_zero,X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0] :
( ~ int_leq(int_one,X0)
| int_less(int_zero,X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f42,plain,
! [I,J] :
( ( ! [C] :
( ! [K] :
( a(K,plus(K,C)) = real_zero
| ~ int_leq(K,I)
| ~ int_leq(int_one,K) )
| J != plus(I,C)
| ~ int_less(int_zero,C) )
& ! [K] :
( a(K,K) = real_one
| ~ int_leq(K,J)
| ~ int_leq(int_one,K) )
& ! [C] :
( ! [K] :
( a(plus(K,C),K) = real_zero
| ~ int_leq(K,J)
| ~ int_leq(int_one,K) )
| I != plus(J,C)
| ~ int_less(int_zero,C) ) )
| ~ int_leq(J,n)
| ~ int_leq(int_one,J)
| ~ int_leq(I,n)
| ~ int_leq(int_one,I) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( a(plus(X3,X2),X3) = real_zero
| ~ int_leq(X3,X1)
| ~ int_leq(int_one,X3)
| X0 != plus(X1,X2)
| ~ int_less(int_zero,X2)
| ~ int_leq(X1,n)
| ~ int_leq(int_one,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f46,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(f47,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)],[f46]) ).
fof(f48,plain,
int_leq(int_one,sK2_skl),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
int_less(sK2_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f50,plain,
int_leq(sK1_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(f62,plain,
! [X0,X1,X2] :
( a(plus(X2,X1),X2) = real_zero
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_less(int_zero,X1)
| ~ int_leq(X0,n)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,X1),n)
| ~ int_leq(int_one,plus(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f43]) ).
fof(f73,plain,
int_leq(sK2_skl,sK1_skl),
inference(resolution,[status(thm)],[f18,f49]) ).
fof(f76,plain,
! [X0] :
( int_less(sK2_skl,X0)
| ~ int_less(sK1_skl,X0) ),
inference(resolution,[status(thm)],[f22,f49]) ).
fof(f77,plain,
! [X0,X1] :
( X1 = X0
| int_less(X1,X0)
| int_less(X0,X1) ),
inference(resolution,[status(thm)],[f25,f17]) ).
fof(f86,plain,
( sK1_skl = n
| int_less(sK1_skl,n) ),
inference(resolution,[status(thm)],[f50,f17]) ).
fof(f87,definition,
( sQ4_spl
<=> int_less(sK1_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f88,plain,
( ~ sQ4_spl
| int_less(sK1_skl,n) ),
inference(component_clause,[status(thm)],[f87]) ).
fof(f90,definition,
( sQ5_spl
<=> sK1_skl = n ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f91,plain,
( ~ sQ5_spl
| sK1_skl = n ),
inference(component_clause,[status(thm)],[f90]) ).
fof(f93,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f86,f87,f90]) ).
fof(f100,definition,
( sQ7_spl
<=> sK2_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f101,plain,
( ~ sQ7_spl
| sK2_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f162,plain,
plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)) = sK1_skl,
inference(resolution,[status(thm)],[f34,f49]) ).
fof(f197,plain,
! [X0] :
( int_less(sK2_skl,X0)
| sK1_skl = X0
| int_less(X0,sK1_skl) ),
inference(resolution,[status(thm)],[f77,f76]) ).
fof(f245,definition,
( sQ21_spl
<=> int_less(sK2_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f246,plain,
( ~ sQ21_spl
| int_less(sK2_skl,n) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f247,plain,
( sQ21_spl
| ~ int_less(sK2_skl,n) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f323,plain,
( ~ sQ21_spl
| int_leq(sK2_skl,n) ),
inference(resolution,[status(thm)],[f246,f18]) ).
fof(f350,plain,
int_less(int_zero,sK2_skl),
inference(resolution,[status(thm)],[f40,f48]) ).
fof(f418,plain,
! [X0] :
( a(plus(X0,sK0_skl(sK1_skl,sK2_skl)),X0) = real_zero
| ~ int_leq(X0,sK2_skl)
| ~ int_leq(int_one,X0)
| ~ int_less(int_zero,sK0_skl(sK1_skl,sK2_skl))
| ~ int_leq(sK2_skl,n)
| ~ int_leq(int_one,sK2_skl)
| ~ int_leq(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),n)
| ~ int_leq(int_one,sK1_skl) ),
inference(paramodulation,[status(thm)],[f162,f62]) ).
fof(f421,definition,
( sQ29_spl
<=> int_leq(int_one,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f423,plain,
( sQ29_spl
| ~ int_leq(int_one,sK1_skl) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,definition,
( sQ30_spl
<=> int_leq(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),n) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f426,plain,
( sQ30_spl
| ~ int_leq(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),n) ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f427,definition,
( sQ31_spl
<=> int_leq(int_one,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( sQ31_spl
| ~ int_leq(int_one,sK2_skl) ),
inference(component_clause,[status(thm)],[f427]) ).
fof(f430,definition,
( sQ32_spl
<=> int_leq(sK2_skl,n) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( sQ32_spl
| ~ int_leq(sK2_skl,n) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f433,definition,
( sQ33_spl
<=> int_less(int_zero,sK0_skl(sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( sQ33_spl
| ~ int_less(int_zero,sK0_skl(sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f433]) ).
fof(f436,definition,
! [X0] :
( sQ34_spl
<=> ( a(plus(X0,sK0_skl(sK1_skl,sK2_skl)),X0) = real_zero
| ~ int_leq(X0,sK2_skl)
| ~ int_leq(int_one,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f437,plain,
! [X0] :
( ~ sQ34_spl
| a(plus(X0,sK0_skl(sK1_skl,sK2_skl)),X0) = real_zero
| ~ int_leq(X0,sK2_skl)
| ~ int_leq(int_one,X0) ),
inference(component_clause,[status(thm)],[f436]) ).
fof(f439,plain,
( sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f418,f421,f424,f427,f430,f433,f436]) ).
fof(f440,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f429,f48]) ).
fof(f441,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f440]) ).
fof(f442,plain,
( sQ30_spl
| ~ int_leq(sK1_skl,n) ),
inference(forward_demodulation,[status(thm)],[f162,f426]) ).
fof(f443,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f442,f50]) ).
fof(f444,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f443]) ).
fof(f479,plain,
! [X0] :
( int_less(int_zero,X0)
| ~ int_less(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f350,f22]) ).
fof(f647,definition,
( sQ47_spl
<=> int_less(int_zero,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f648,plain,
( ~ sQ47_spl
| int_less(int_zero,sK1_skl) ),
inference(component_clause,[status(thm)],[f647]) ).
fof(f687,plain,
( sQ32_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f432,f323]) ).
fof(f688,plain,
( sQ32_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f687]) ).
fof(f707,plain,
( ~ sQ47_spl
| int_leq(int_one,sK1_skl) ),
inference(resolution,[status(thm)],[f648,f39]) ).
fof(f713,plain,
( ~ sQ47_spl
| sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f707,f423]) ).
fof(f714,plain,
( ~ sQ47_spl
| sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f713]) ).
fof(f718,definition,
( sQ51_spl
<=> int_leq(sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f720,plain,
( sQ51_spl
| ~ int_leq(sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f729,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f720,f59]) ).
fof(f730,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f729]) ).
fof(f927,plain,
( ~ sQ7_spl
| int_less(sK1_skl,sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f101,f49]) ).
fof(f930,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f927,f60]) ).
fof(f931,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f930]) ).
fof(f1126,definition,
( sQ74_spl
<=> int_leq(sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1128,plain,
( sQ74_spl
| ~ int_leq(sK2_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f1126]) ).
fof(f1138,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| 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),sK1_skl)
| ~ int_leq(int_one,plus(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f91,f62]) ).
fof(f1139,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| a(plus(X2,X1),X2) = real_zero
| ~ int_leq(X2,X0)
| ~ int_leq(int_one,X2)
| ~ int_less(int_zero,X1)
| ~ int_leq(X0,sK1_skl)
| ~ int_leq(int_one,X0)
| ~ int_leq(plus(X0,X1),sK1_skl)
| ~ int_leq(int_one,plus(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f91,f1138]) ).
fof(f1302,plain,
( sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1128,f73]) ).
fof(f1303,plain,
sQ74_spl,
inference(contradiction_clause,[status(thm)],[f1302]) ).
fof(f1507,plain,
( ~ sQ4_spl
| int_less(sK2_skl,n) ),
inference(resolution,[status(thm)],[f88,f76]) ).
fof(f1642,plain,
int_less(int_zero,sK0_skl(sK1_skl,sK2_skl)),
inference(resolution,[status(thm)],[f35,f49]) ).
fof(f2360,plain,
( sQ21_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f247,f1507]) ).
fof(f2361,plain,
( sQ21_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f2360]) ).
fof(f3105,definition,
( sQ131_spl
<=> int_leq(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f3107,plain,
( sQ131_spl
| ~ int_leq(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK1_skl) ),
inference(component_clause,[status(thm)],[f3105]) ).
fof(f3230,plain,
( sQ131_spl
| ~ int_leq(sK1_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f162,f3107]) ).
fof(f3231,plain,
( sQ131_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3230,f59]) ).
fof(f3232,plain,
sQ131_spl,
inference(contradiction_clause,[status(thm)],[f3231]) ).
fof(f3364,plain,
! [X0] :
( ~ sQ5_spl
| a(plus(X0,sK0_skl(sK1_skl,sK2_skl)),X0) = real_zero
| ~ int_leq(X0,sK2_skl)
| ~ int_leq(int_one,X0)
| ~ int_less(int_zero,sK0_skl(sK1_skl,sK2_skl))
| ~ int_leq(sK2_skl,sK1_skl)
| ~ int_leq(int_one,sK2_skl)
| ~ int_leq(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK1_skl)
| ~ int_leq(int_one,sK1_skl) ),
inference(paramodulation,[status(thm)],[f162,f1139]) ).
fof(f3371,plain,
( ~ sQ5_spl
| sQ34_spl
| ~ sQ33_spl
| ~ sQ74_spl
| ~ sQ31_spl
| ~ sQ131_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f3364,f421,f3105,f427,f1126,f433,f436,f90]) ).
fof(f3841,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f435,f1642]) ).
fof(f3842,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f3841]) ).
fof(f5188,plain,
( int_less(sK2_skl,sK2_skl)
| sK1_skl = sK2_skl
| int_less(int_zero,sK1_skl) ),
inference(resolution,[status(thm)],[f479,f197]) ).
fof(f5203,definition,
( sQ168_spl
<=> int_less(sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f5204,plain,
( ~ sQ168_spl
| int_less(sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f5203]) ).
fof(f5206,plain,
( sQ168_spl
| sQ7_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f5188,f647,f100,f5203]) ).
fof(f5213,plain,
( ~ sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5204,f60]) ).
fof(f5214,plain,
~ sQ168_spl,
inference(contradiction_clause,[status(thm)],[f5213]) ).
fof(f8918,plain,
( ~ sQ34_spl
| a(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK2_skl) = real_zero
| ~ int_leq(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f437,f48]) ).
fof(f8944,definition,
( sQ322_spl
<=> a(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK2_skl) = real_zero ),
introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition]) ).
fof(f8945,plain,
( ~ sQ322_spl
| a(plus(sK2_skl,sK0_skl(sK1_skl,sK2_skl)),sK2_skl) = real_zero ),
inference(component_clause,[status(thm)],[f8944]) ).
fof(f8947,plain,
( ~ sQ34_spl
| sQ322_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f8918,f718,f8944,f436]) ).
fof(f8982,plain,
( ~ sQ322_spl
| a(sK1_skl,sK2_skl) = real_zero ),
inference(forward_demodulation,[status(thm)],[f162,f8945]) ).
fof(f8983,plain,
( ~ sQ322_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8982,f51]) ).
fof(f8984,plain,
~ sQ322_spl,
inference(contradiction_clause,[status(thm)],[f8983]) ).
fof(f8985,plain,
$false,
inference(sat_refutation,[status(thm)],[f93,f439,f441,f444,f688,f714,f730,f931,f1303,f2361,f3232,f3371,f3842,f5206,f5214,f8947,f8984]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV487+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n015.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 08:57:51 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 19.31/3.02 % Refutation found
% 19.31/3.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.31/3.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.34/3.07 % Elapsed time: 2.591476 seconds
% 8.34/3.07 % CPU time: 20.045711 seconds
% 8.34/3.07 % Total memory used: 175.105 MB
% 8.34/3.07 % Net memory used: 159.651 MB
%------------------------------------------------------------------------------