%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ANA002-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 12:02:10 PM UTC 2026
% Result : Unsatisfiable 65.15s 8.64s
% Output : CNFRefutation 65.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 91
% Syntax : Number of formulae : 375 ( 18 unt; 74 def)
% Number of atoms : 1214 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 1470 ( 631 ~; 765 |; 0 &)
% ( 74 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 76 ( 75 usr; 75 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 328 ( 328 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : less_than_or_equal(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( less_than_or_equal(Y,X)
| less_than_or_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Z,Y] :
( ~ less_than_or_equal(Y,Z)
| ~ less_than_or_equal(X,Y)
| less_than_or_equal(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( less_than_or_equal(X,Y)
| ~ less_than_or_equal(X,q(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] :
( less_than_or_equal(Y,X)
| ~ less_than_or_equal(q(X,Y),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] :
( ~ less_than_or_equal(X,upper_bound)
| ~ less_than_or_equal(lower_bound,X)
| ~ less_than_or_equal(X,h(X))
| less_than_or_equal(f(X),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] :
( ~ less_than_or_equal(X,upper_bound)
| ~ less_than_or_equal(lower_bound,X)
| less_than_or_equal(Y,h(X))
| ~ less_than_or_equal(f(Y),n0)
| ~ less_than_or_equal(Y,X)
| less_than_or_equal(f(X),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] :
( ~ less_than_or_equal(X,upper_bound)
| ~ less_than_or_equal(lower_bound,X)
| ~ less_than_or_equal(k(X),X)
| less_than_or_equal(n0,f(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( ~ less_than_or_equal(X,upper_bound)
| ~ less_than_or_equal(lower_bound,X)
| less_than_or_equal(k(X),Y)
| ~ less_than_or_equal(n0,f(Y))
| ~ less_than_or_equal(X,Y)
| less_than_or_equal(n0,f(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] :
( ~ less_than_or_equal(f(X),n0)
| ~ less_than_or_equal(X,upper_bound)
| less_than_or_equal(X,l) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] :
( less_than_or_equal(l,X)
| less_than_or_equal(g(X),upper_bound) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] :
( less_than_or_equal(l,X)
| less_than_or_equal(f(g(X)),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X] :
( less_than_or_equal(l,X)
| ~ less_than_or_equal(g(X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
less_than_or_equal(lower_bound,upper_bound),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
less_than_or_equal(f(lower_bound),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
less_than_or_equal(n0,f(upper_bound)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
( ~ less_than_or_equal(n0,f(l))
| ~ less_than_or_equal(f(l),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,plain,
! [X0] : less_than_or_equal(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f19,plain,
! [X0,X1] :
( less_than_or_equal(X1,X0)
| less_than_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f20,plain,
! [Z,Y] :
( ~ less_than_or_equal(Y,Z)
| ! [X] :
( ~ less_than_or_equal(X,Y)
| less_than_or_equal(X,Z) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f21,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(X2,X1)
| ~ less_than_or_equal(X0,X2)
| less_than_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
! [X0,X1] :
( less_than_or_equal(X0,X1)
| ~ less_than_or_equal(X0,q(X1,X0)) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f23,plain,
! [X0,X1] :
( less_than_or_equal(X1,X0)
| ~ less_than_or_equal(q(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f24,plain,
! [X0] :
( ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(lower_bound,X0)
| ~ less_than_or_equal(X0,h(X0))
| less_than_or_equal(f(X0),n0) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f25,plain,
! [X] :
( ~ less_than_or_equal(X,upper_bound)
| ~ less_than_or_equal(lower_bound,X)
| ! [Y] :
( less_than_or_equal(Y,h(X))
| ~ less_than_or_equal(f(Y),n0)
| ~ less_than_or_equal(Y,X)
| less_than_or_equal(f(X),n0) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0,X1] :
( ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(lower_bound,X0)
| less_than_or_equal(X1,h(X0))
| ~ less_than_or_equal(f(X1),n0)
| ~ less_than_or_equal(X1,X0)
| less_than_or_equal(f(X0),n0) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f27,plain,
! [X0] :
( ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(lower_bound,X0)
| ~ less_than_or_equal(k(X0),X0)
| less_than_or_equal(n0,f(X0)) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f28,plain,
! [X] :
( ~ less_than_or_equal(X,upper_bound)
| ~ less_than_or_equal(lower_bound,X)
| ! [Y] :
( less_than_or_equal(k(X),Y)
| ~ less_than_or_equal(n0,f(Y))
| ~ less_than_or_equal(X,Y)
| less_than_or_equal(n0,f(X)) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f29,plain,
! [X0,X1] :
( ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(lower_bound,X0)
| less_than_or_equal(k(X0),X1)
| ~ less_than_or_equal(n0,f(X1))
| ~ less_than_or_equal(X0,X1)
| less_than_or_equal(n0,f(X0)) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [X0] :
( ~ less_than_or_equal(f(X0),n0)
| ~ less_than_or_equal(X0,upper_bound)
| less_than_or_equal(X0,l) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f31,plain,
! [X0] :
( less_than_or_equal(l,X0)
| less_than_or_equal(g(X0),upper_bound) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f32,plain,
! [X0] :
( less_than_or_equal(l,X0)
| less_than_or_equal(f(g(X0)),n0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f33,plain,
! [X0] :
( less_than_or_equal(l,X0)
| ~ less_than_or_equal(g(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f34,plain,
less_than_or_equal(lower_bound,upper_bound),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f35,plain,
less_than_or_equal(f(lower_bound),n0),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f36,plain,
less_than_or_equal(n0,f(upper_bound)),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f37,plain,
( ~ less_than_or_equal(n0,f(l))
| ~ less_than_or_equal(f(l),n0) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f38,definition,
( sQ0_spl
<=> less_than_or_equal(f(l),n0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f40,plain,
( sQ0_spl
| ~ less_than_or_equal(f(l),n0) ),
inference(component_clause,[status(thm)],[f38]) ).
fof(f41,definition,
( sQ1_spl
<=> less_than_or_equal(n0,f(l)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f43,plain,
( sQ1_spl
| ~ less_than_or_equal(n0,f(l)) ),
inference(component_clause,[status(thm)],[f41]) ).
fof(f44,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f37,f38,f41]) ).
fof(f46,plain,
! [X0] :
( sQ0_spl
| ~ less_than_or_equal(X0,n0)
| ~ less_than_or_equal(f(l),X0) ),
inference(resolution,[status(thm)],[f21,f40]) ).
fof(f47,plain,
! [X0,X1] :
( sQ0_spl
| ~ less_than_or_equal(X1,X0)
| ~ less_than_or_equal(f(l),X1)
| ~ less_than_or_equal(X0,n0) ),
inference(resolution,[status(thm)],[f46,f21]) ).
fof(f53,plain,
! [X0,X1] :
( sQ0_spl
| less_than_or_equal(n0,X1)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(f(l),X0) ),
inference(resolution,[status(thm)],[f47,f19]) ).
fof(f55,plain,
! [X0,X1] :
( sQ0_spl
| ~ less_than_or_equal(X1,n0)
| ~ less_than_or_equal(f(l),X1)
| ~ less_than_or_equal(X0,n0)
| ~ less_than_or_equal(f(l),X0) ),
inference(resolution,[status(thm)],[f53,f47]) ).
fof(f56,definition,
! [X0] :
( sQ2_spl
<=> ( ~ less_than_or_equal(X0,n0)
| ~ less_than_or_equal(f(l),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f57,plain,
! [X0] :
( ~ sQ2_spl
| ~ less_than_or_equal(X0,n0)
| ~ less_than_or_equal(f(l),X0) ),
inference(component_clause,[status(thm)],[f56]) ).
fof(f59,plain,
( sQ0_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f55,f56,f38]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(X2,q(X1,X0))
| ~ less_than_or_equal(X0,X2)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f22,f21]) ).
fof(f66,plain,
! [X0,X1] :
( less_than_or_equal(q(X1,X0),X0)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f22,f19]) ).
fof(f67,plain,
! [X0] :
( ~ less_than_or_equal(f(q(l,X0)),n0)
| ~ less_than_or_equal(q(l,X0),upper_bound)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f23,f30]) ).
fof(f68,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(X2,X1)
| ~ less_than_or_equal(q(X1,X0),X2)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f23,f21]) ).
fof(f69,plain,
! [X0,X1] :
( less_than_or_equal(X1,q(X1,X0))
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f23,f19]) ).
fof(f70,plain,
! [X0] :
( less_than_or_equal(l,X0)
| ~ less_than_or_equal(g(q(X0,l)),q(X0,l)) ),
inference(resolution,[status(thm)],[f33,f22]) ).
fof(f72,definition,
( sQ3_spl
<=> less_than_or_equal(g(f(l)),f(l)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f74,plain,
( sQ3_spl
| ~ less_than_or_equal(g(f(l)),f(l)) ),
inference(component_clause,[status(thm)],[f72]) ).
fof(f94,definition,
( sQ7_spl
<=> less_than_or_equal(l,h(l)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f96,plain,
( sQ7_spl
| ~ less_than_or_equal(l,h(l)) ),
inference(component_clause,[status(thm)],[f94]) ).
fof(f97,definition,
( sQ8_spl
<=> less_than_or_equal(lower_bound,l) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f99,plain,
( sQ8_spl
| ~ less_than_or_equal(lower_bound,l) ),
inference(component_clause,[status(thm)],[f97]) ).
fof(f100,definition,
( sQ9_spl
<=> less_than_or_equal(l,upper_bound) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f101,plain,
( ~ sQ9_spl
| less_than_or_equal(l,upper_bound) ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f102,plain,
( sQ9_spl
| ~ less_than_or_equal(l,upper_bound) ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f105,definition,
! [X0] :
( sQ10_spl
<=> ( less_than_or_equal(X0,h(l))
| ~ less_than_or_equal(f(X0),n0)
| ~ less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f106,plain,
! [X0] :
( ~ sQ10_spl
| less_than_or_equal(X0,h(l))
| ~ less_than_or_equal(f(X0),n0)
| ~ less_than_or_equal(X0,l) ),
inference(component_clause,[status(thm)],[f105]) ).
fof(f109,plain,
( sQ9_spl
| ~ less_than_or_equal(g(upper_bound),upper_bound) ),
inference(resolution,[status(thm)],[f102,f33]) ).
fof(f112,plain,
( sQ8_spl
| ~ less_than_or_equal(f(lower_bound),n0)
| ~ less_than_or_equal(lower_bound,upper_bound) ),
inference(resolution,[status(thm)],[f99,f30]) ).
fof(f115,definition,
( sQ11_spl
<=> less_than_or_equal(lower_bound,upper_bound) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f117,plain,
( sQ11_spl
| ~ less_than_or_equal(lower_bound,upper_bound) ),
inference(component_clause,[status(thm)],[f115]) ).
fof(f118,definition,
( sQ12_spl
<=> less_than_or_equal(f(lower_bound),n0) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f120,plain,
( sQ12_spl
| ~ less_than_or_equal(f(lower_bound),n0) ),
inference(component_clause,[status(thm)],[f118]) ).
fof(f121,plain,
( sQ8_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f112,f115,f118,f97]) ).
fof(f147,plain,
! [X0,X1] :
( ~ less_than_or_equal(g(q(X1,X0)),q(X1,X0))
| ~ less_than_or_equal(X0,l)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f65,f33]) ).
fof(f148,plain,
! [X0,X1,X2,X3] :
( ~ less_than_or_equal(X3,q(X1,X0))
| ~ less_than_or_equal(X2,X3)
| ~ less_than_or_equal(X0,X2)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f65,f21]) ).
fof(f149,plain,
! [X0,X1,X2] :
( less_than_or_equal(q(X1,X0),X2)
| ~ less_than_or_equal(X0,X2)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f65,f19]) ).
fof(f177,plain,
! [X0] :
( ~ sQ2_spl
| ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(X0,h(l))
| ~ less_than_or_equal(f(X0),n0)
| ~ less_than_or_equal(X0,l)
| ~ less_than_or_equal(n0,n0) ),
inference(resolution,[status(thm)],[f57,f26]) ).
fof(f184,definition,
( sQ17_spl
<=> less_than_or_equal(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f186,plain,
( sQ17_spl
| ~ less_than_or_equal(n0,n0) ),
inference(component_clause,[status(thm)],[f184]) ).
fof(f187,plain,
( ~ sQ2_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ10_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f177,f184,f105,f97,f100,f56]) ).
fof(f192,definition,
( sQ19_spl
<=> less_than_or_equal(f(l),upper_bound) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f186,f18]) ).
fof(f200,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f199]) ).
fof(f263,plain,
( less_than_or_equal(upper_bound,l)
| ~ less_than_or_equal(f(q(l,upper_bound)),n0)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f67,f66]) ).
fof(f264,plain,
! [X0,X1] :
( ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| ~ less_than_or_equal(f(q(l,X0)),n0)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f67,f21]) ).
fof(f265,plain,
! [X0] :
( less_than_or_equal(upper_bound,q(l,X0))
| ~ less_than_or_equal(f(q(l,X0)),n0)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f67,f19]) ).
fof(f266,definition,
( sQ28_spl
<=> less_than_or_equal(upper_bound,l) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f267,plain,
( ~ sQ28_spl
| less_than_or_equal(upper_bound,l) ),
inference(component_clause,[status(thm)],[f266]) ).
fof(f269,definition,
( sQ29_spl
<=> less_than_or_equal(f(q(l,upper_bound)),n0) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( sQ29_spl
| ~ less_than_or_equal(f(q(l,upper_bound)),n0) ),
inference(component_clause,[status(thm)],[f269]) ).
fof(f272,plain,
( ~ sQ29_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f263,f266,f269]) ).
fof(f276,plain,
! [X0,X1,X2,X3] :
( ~ less_than_or_equal(X3,X2)
| ~ less_than_or_equal(q(X1,X0),X3)
| ~ less_than_or_equal(X2,X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f68,f21]) ).
fof(f277,plain,
! [X0,X1,X2] :
( less_than_or_equal(X2,q(X1,X0))
| ~ less_than_or_equal(X2,X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f68,f19]) ).
fof(f291,definition,
( sQ30_spl
<=> less_than_or_equal(upper_bound,upper_bound) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ30_spl
| ~ less_than_or_equal(upper_bound,upper_bound) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f294,definition,
( sQ31_spl
<=> less_than_or_equal(f(upper_bound),n0) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f298,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f293,f18]) ).
fof(f299,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f298]) ).
fof(f317,plain,
! [X0,X1] :
( ~ less_than_or_equal(X1,q(X0,l))
| ~ less_than_or_equal(g(q(X0,l)),X1)
| less_than_or_equal(l,X0) ),
inference(resolution,[status(thm)],[f70,f21]) ).
fof(f340,definition,
( sQ32_spl
<=> less_than_or_equal(l,l) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( sQ32_spl
| ~ less_than_or_equal(l,l) ),
inference(component_clause,[status(thm)],[f340]) ).
fof(f347,definition,
( sQ34_spl
<=> less_than_or_equal(f(l),l) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( ~ sQ34_spl
| less_than_or_equal(f(l),l) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f351,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f342,f18]) ).
fof(f352,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f351]) ).
fof(f371,plain,
( sQ7_spl
| ~ less_than_or_equal(g(h(l)),h(l)) ),
inference(resolution,[status(thm)],[f96,f33]) ).
fof(f374,plain,
! [X0] :
( sQ3_spl
| ~ less_than_or_equal(X0,f(l))
| ~ less_than_or_equal(g(f(l)),X0) ),
inference(resolution,[status(thm)],[f74,f21]) ).
fof(f376,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f120,f35]) ).
fof(f377,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f376]) ).
fof(f421,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f117,f34]) ).
fof(f422,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f421]) ).
fof(f439,plain,
! [X0] :
( sQ29_spl
| ~ less_than_or_equal(q(l,upper_bound),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,upper_bound))
| less_than_or_equal(X0,h(q(l,upper_bound)))
| ~ less_than_or_equal(f(X0),n0)
| ~ less_than_or_equal(X0,q(l,upper_bound)) ),
inference(resolution,[status(thm)],[f271,f26]) ).
fof(f440,plain,
( sQ29_spl
| ~ less_than_or_equal(q(l,upper_bound),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,upper_bound))
| ~ less_than_or_equal(q(l,upper_bound),h(q(l,upper_bound))) ),
inference(resolution,[status(thm)],[f271,f24]) ).
fof(f442,plain,
( sQ29_spl
| less_than_or_equal(n0,f(q(l,upper_bound))) ),
inference(resolution,[status(thm)],[f271,f19]) ).
fof(f443,definition,
! [X0] :
( sQ37_spl
<=> ( less_than_or_equal(X0,h(q(l,upper_bound)))
| ~ less_than_or_equal(f(X0),n0)
| ~ less_than_or_equal(X0,q(l,upper_bound)) ) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f444,plain,
! [X0] :
( ~ sQ37_spl
| less_than_or_equal(X0,h(q(l,upper_bound)))
| ~ less_than_or_equal(f(X0),n0)
| ~ less_than_or_equal(X0,q(l,upper_bound)) ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,definition,
( sQ38_spl
<=> less_than_or_equal(lower_bound,q(l,upper_bound)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ38_spl
| ~ less_than_or_equal(lower_bound,q(l,upper_bound)) ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,definition,
( sQ39_spl
<=> less_than_or_equal(q(l,upper_bound),upper_bound) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( ~ sQ39_spl
| less_than_or_equal(q(l,upper_bound),upper_bound) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f451,plain,
( sQ39_spl
| ~ less_than_or_equal(q(l,upper_bound),upper_bound) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
( sQ29_spl
| ~ sQ39_spl
| ~ sQ38_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f439,f443,f446,f449,f269]) ).
fof(f453,definition,
( sQ40_spl
<=> less_than_or_equal(q(l,upper_bound),h(q(l,upper_bound))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( sQ40_spl
| ~ less_than_or_equal(q(l,upper_bound),h(q(l,upper_bound))) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,plain,
( sQ29_spl
| ~ sQ39_spl
| ~ sQ38_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f440,f453,f446,f449,f269]) ).
fof(f460,plain,
( sQ39_spl
| less_than_or_equal(upper_bound,q(l,upper_bound)) ),
inference(resolution,[status(thm)],[f451,f19]) ).
fof(f464,plain,
( sQ39_spl
| ~ less_than_or_equal(upper_bound,upper_bound)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f460,f65]) ).
fof(f466,plain,
( sQ39_spl
| ~ sQ30_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f464,f266,f291,f449]) ).
fof(f513,plain,
! [X0,X1] :
( sQ0_spl
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(lower_bound,X1)
| ~ less_than_or_equal(X1,h(X1))
| ~ less_than_or_equal(X0,f(X1))
| ~ less_than_or_equal(f(l),X0) ),
inference(resolution,[status(thm)],[f47,f24]) ).
fof(f518,definition,
! [X0] :
( sQ48_spl
<=> ( ~ less_than_or_equal(X0,l)
| ~ less_than_or_equal(f(l),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f519,plain,
! [X0] :
( ~ sQ48_spl
| ~ less_than_or_equal(X0,l)
| ~ less_than_or_equal(f(l),X0) ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f524,plain,
! [X0,X1,X2,X3] :
( less_than_or_equal(q(X1,X0),X3)
| ~ less_than_or_equal(X2,q(X3,q(X1,X0)))
| ~ less_than_or_equal(X0,X2)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f148,f66]) ).
fof(f527,plain,
! [X0,X1,X2,X3,X4] :
( ~ less_than_or_equal(X4,q(X1,X0))
| ~ less_than_or_equal(X3,X4)
| ~ less_than_or_equal(X2,X3)
| ~ less_than_or_equal(X0,X2)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f148,f21]) ).
fof(f528,plain,
! [X0,X1,X2,X3] :
( less_than_or_equal(q(X1,X0),X3)
| ~ less_than_or_equal(X2,X3)
| ~ less_than_or_equal(X0,X2)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f148,f19]) ).
fof(f547,plain,
( sQ9_spl
| less_than_or_equal(l,upper_bound) ),
inference(resolution,[status(thm)],[f109,f31]) ).
fof(f551,plain,
sQ9_spl,
inference(split_clause,[status(thm)],[f547,f100]) ).
fof(f554,plain,
! [X0] :
( sQ1_spl
| ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),X0)
| ~ less_than_or_equal(n0,f(X0))
| ~ less_than_or_equal(l,X0) ),
inference(resolution,[status(thm)],[f43,f29]) ).
fof(f555,plain,
( sQ1_spl
| ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| ~ less_than_or_equal(k(l),l) ),
inference(resolution,[status(thm)],[f43,f27]) ).
fof(f559,definition,
! [X0] :
( sQ50_spl
<=> ( less_than_or_equal(k(l),X0)
| ~ less_than_or_equal(n0,f(X0))
| ~ less_than_or_equal(l,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f560,plain,
! [X0] :
( ~ sQ50_spl
| less_than_or_equal(k(l),X0)
| ~ less_than_or_equal(n0,f(X0))
| ~ less_than_or_equal(l,X0) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,plain,
( sQ1_spl
| ~ sQ9_spl
| ~ sQ8_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f554,f559,f97,f100,f41]) ).
fof(f563,definition,
( sQ51_spl
<=> less_than_or_equal(k(l),l) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ51_spl
| ~ less_than_or_equal(k(l),l) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f566,plain,
( sQ1_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f555,f563,f97,f100,f41]) ).
fof(f591,plain,
! [X0,X1,X2] :
( ~ sQ50_spl
| ~ less_than_or_equal(X2,k(l))
| ~ less_than_or_equal(X1,X2)
| less_than_or_equal(X1,X0)
| ~ less_than_or_equal(n0,f(q(X0,X1)))
| ~ less_than_or_equal(l,q(X0,X1)) ),
inference(resolution,[status(thm)],[f560,f148]) ).
fof(f592,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ less_than_or_equal(X1,k(l))
| less_than_or_equal(X1,X0)
| ~ less_than_or_equal(n0,f(q(X0,X1)))
| ~ less_than_or_equal(l,q(X0,X1)) ),
inference(resolution,[status(thm)],[f560,f65]) ).
fof(f593,plain,
! [X0] :
( ~ sQ50_spl
| less_than_or_equal(k(l),X0)
| ~ less_than_or_equal(n0,f(q(X0,k(l))))
| ~ less_than_or_equal(l,q(X0,k(l))) ),
inference(resolution,[status(thm)],[f560,f22]) ).
fof(f594,definition,
( sQ53_spl
<=> less_than_or_equal(l,f(l)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f596,plain,
( sQ53_spl
| ~ less_than_or_equal(l,f(l)) ),
inference(component_clause,[status(thm)],[f594]) ).
fof(f609,definition,
( sQ56_spl
<=> less_than_or_equal(k(l),upper_bound) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( sQ56_spl
| ~ less_than_or_equal(k(l),upper_bound) ),
inference(component_clause,[status(thm)],[f609]) ).
fof(f620,plain,
! [X0,X1,X2,X3,X4] :
( ~ less_than_or_equal(X4,q(X1,X0))
| ~ less_than_or_equal(X3,X4)
| less_than_or_equal(X3,X2)
| ~ less_than_or_equal(X0,q(X2,X3))
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f149,f148]) ).
fof(f621,plain,
! [X0,X1,X2,X3] :
( ~ less_than_or_equal(X3,q(X1,X0))
| less_than_or_equal(X3,X2)
| ~ less_than_or_equal(X0,q(X2,X3))
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f149,f65]) ).
fof(f647,definition,
! [X0] :
( sQ58_spl
<=> ( ~ less_than_or_equal(X0,f(l))
| ~ less_than_or_equal(l,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f673,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X2,h(q(l,X0)))
| ~ less_than_or_equal(f(X2),n0)
| ~ less_than_or_equal(X2,q(l,X0))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f264,f26]) ).
fof(f674,plain,
! [X0,X1] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f264,f24]) ).
fof(f675,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(X2,n0)
| ~ less_than_or_equal(f(q(l,X0)),X2)
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f264,f21]) ).
fof(f677,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X2,h(q(l,X0)))
| ~ less_than_or_equal(f(X2),n0)
| ~ less_than_or_equal(X2,q(l,X0))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f21]) ).
fof(f678,plain,
! [X0,X1] :
( ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(forward_subsumption_resolution,[status(thm)],[f674,f21]) ).
fof(f696,plain,
! [X0,X1] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X1,h(q(l,X0)))
| ~ less_than_or_equal(f(X1),n0)
| ~ less_than_or_equal(X1,q(l,X0))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f265,f26]) ).
fof(f697,plain,
! [X0] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f265,f24]) ).
fof(f698,plain,
! [X0,X1] :
( ~ less_than_or_equal(X1,n0)
| ~ less_than_or_equal(f(q(l,X0)),X1)
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f265,f21]) ).
fof(f699,plain,
! [X0] :
( less_than_or_equal(n0,f(q(l,X0)))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f265,f19]) ).
fof(f700,plain,
! [X0,X1] :
( ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X1,h(q(l,X0)))
| ~ less_than_or_equal(f(X1),n0)
| ~ less_than_or_equal(X1,q(l,X0))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(forward_subsumption_resolution,[status(thm)],[f696,f19]) ).
fof(f701,plain,
! [X0] :
( ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(forward_subsumption_resolution,[status(thm)],[f697,f19]) ).
fof(f723,definition,
! [X0] :
( sQ59_spl
<=> ( ~ less_than_or_equal(X0,f(l))
| ~ less_than_or_equal(upper_bound,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f736,plain,
! [X0] :
( sQ53_spl
| ~ less_than_or_equal(X0,f(l))
| ~ less_than_or_equal(l,X0) ),
inference(resolution,[status(thm)],[f596,f21]) ).
fof(f737,plain,
( sQ53_spl
| less_than_or_equal(f(l),l) ),
inference(resolution,[status(thm)],[f596,f19]) ).
fof(f738,plain,
! [X0,X1,X2,X3] :
( ~ less_than_or_equal(X0,X3)
| less_than_or_equal(X0,X1)
| ~ less_than_or_equal(X3,X2)
| ~ less_than_or_equal(X2,X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f276,f149]) ).
fof(f742,plain,
! [X0,X1,X2,X3,X4] :
( ~ less_than_or_equal(X4,X3)
| ~ less_than_or_equal(q(X1,X0),X4)
| ~ less_than_or_equal(X3,X2)
| ~ less_than_or_equal(X2,X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f276,f21]) ).
fof(f743,plain,
! [X0,X1,X2,X3] :
( less_than_or_equal(X3,q(X1,X0))
| ~ less_than_or_equal(X3,X2)
| ~ less_than_or_equal(X2,X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f276,f19]) ).
fof(f745,plain,
! [X0,X1,X2,X3] :
( ~ less_than_or_equal(X0,X3)
| ~ less_than_or_equal(X3,X2)
| ~ less_than_or_equal(X2,X1)
| less_than_or_equal(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f738]) ).
fof(f749,plain,
! [X0,X1] :
( ~ less_than_or_equal(X0,l)
| less_than_or_equal(X0,X1)
| ~ less_than_or_equal(g(q(X1,X0)),X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f277,f147]) ).
fof(f751,plain,
! [X0,X1,X2,X3,X4] :
( ~ less_than_or_equal(q(X1,X0),X4)
| ~ less_than_or_equal(X4,X2)
| less_than_or_equal(X3,X2)
| ~ less_than_or_equal(q(X2,X3),X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f277,f276]) ).
fof(f752,plain,
! [X0,X1,X2,X3] :
( ~ less_than_or_equal(q(X1,X0),X2)
| less_than_or_equal(X3,X2)
| ~ less_than_or_equal(q(X2,X3),X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f277,f68]) ).
fof(f759,plain,
! [X0,X1] :
( ~ less_than_or_equal(X0,l)
| ~ less_than_or_equal(g(q(X1,X0)),X1)
| less_than_or_equal(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f749]) ).
fof(f822,plain,
( ~ sQ48_spl
| ~ less_than_or_equal(f(l),l) ),
inference(resolution,[status(thm)],[f519,f18]) ).
fof(f827,plain,
( ~ sQ48_spl
| sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f822,f737]) ).
fof(f828,plain,
( ~ sQ48_spl
| sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f827]) ).
fof(f839,definition,
! [X0] :
( sQ62_spl
<=> ( ~ less_than_or_equal(X0,q(f(l),l))
| ~ less_than_or_equal(g(q(f(l),l)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f895,plain,
! [X0] :
( sQ53_spl
| less_than_or_equal(X0,l)
| ~ less_than_or_equal(X0,f(l)) ),
inference(resolution,[status(thm)],[f736,f19]) ).
fof(f927,definition,
( sQ64_spl
<=> less_than_or_equal(upper_bound,f(l)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1016,plain,
( ~ sQ50_spl
| sQ56_spl
| ~ less_than_or_equal(n0,f(upper_bound))
| ~ less_than_or_equal(l,upper_bound) ),
inference(resolution,[status(thm)],[f611,f560]) ).
fof(f1019,definition,
( sQ66_spl
<=> less_than_or_equal(n0,f(upper_bound)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1021,plain,
( sQ66_spl
| ~ less_than_or_equal(n0,f(upper_bound)) ),
inference(component_clause,[status(thm)],[f1019]) ).
fof(f1022,plain,
( ~ sQ50_spl
| sQ56_spl
| ~ sQ66_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f1016,f100,f1019,f609,f559]) ).
fof(f1023,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1021,f36]) ).
fof(f1024,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f1023]) ).
fof(f1057,plain,
! [X0] :
( ~ sQ39_spl
| ~ less_than_or_equal(upper_bound,X0)
| ~ less_than_or_equal(X0,l)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f450,f276]) ).
fof(f1061,definition,
! [X0] :
( sQ70_spl
<=> ( ~ less_than_or_equal(upper_bound,X0)
| ~ less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1062,plain,
! [X0] :
( ~ sQ70_spl
| ~ less_than_or_equal(upper_bound,X0)
| ~ less_than_or_equal(X0,l) ),
inference(component_clause,[status(thm)],[f1061]) ).
fof(f1064,plain,
( ~ sQ39_spl
| sQ70_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1057,f266,f1061,f449]) ).
fof(f1127,plain,
! [X0] :
( ~ sQ50_spl
| sQ29_spl
| ~ less_than_or_equal(X0,k(l))
| ~ less_than_or_equal(upper_bound,X0)
| less_than_or_equal(upper_bound,l)
| ~ less_than_or_equal(l,q(l,upper_bound)) ),
inference(resolution,[status(thm)],[f442,f591]) ).
fof(f1128,plain,
( ~ sQ50_spl
| sQ29_spl
| ~ less_than_or_equal(upper_bound,k(l))
| less_than_or_equal(upper_bound,l)
| ~ less_than_or_equal(l,q(l,upper_bound)) ),
inference(resolution,[status(thm)],[f442,f592]) ).
fof(f1132,definition,
( sQ73_spl
<=> less_than_or_equal(l,q(l,upper_bound)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1133,plain,
( ~ sQ73_spl
| less_than_or_equal(l,q(l,upper_bound)) ),
inference(component_clause,[status(thm)],[f1132]) ).
fof(f1134,plain,
( sQ73_spl
| ~ less_than_or_equal(l,q(l,upper_bound)) ),
inference(component_clause,[status(thm)],[f1132]) ).
fof(f1135,definition,
! [X0] :
( sQ74_spl
<=> ( ~ less_than_or_equal(X0,k(l))
| ~ less_than_or_equal(upper_bound,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1138,plain,
( ~ sQ50_spl
| sQ29_spl
| sQ74_spl
| sQ28_spl
| ~ sQ73_spl ),
inference(split_clause,[status(thm)],[f1127,f1132,f266,f1135,f269,f559]) ).
fof(f1139,definition,
( sQ75_spl
<=> less_than_or_equal(upper_bound,k(l)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1142,plain,
( ~ sQ50_spl
| sQ29_spl
| ~ sQ75_spl
| sQ28_spl
| ~ sQ73_spl ),
inference(split_clause,[status(thm)],[f1128,f1132,f266,f1139,f269,f559]) ).
fof(f1147,plain,
( sQ73_spl
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f1134,f69]) ).
fof(f1151,plain,
( sQ73_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1147,f266,f1132]) ).
fof(f1166,plain,
( sQ38_spl
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f448,f277]) ).
fof(f1169,plain,
( sQ38_spl
| ~ sQ8_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1166,f266,f97,f446]) ).
fof(f1221,definition,
! [X0] :
( sQ80_spl
<=> ( ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(l,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1222,plain,
! [X0] :
( ~ sQ80_spl
| ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(l,X0) ),
inference(component_clause,[status(thm)],[f1221]) ).
fof(f1315,definition,
! [X0,X1] :
( sQ81_spl
<=> ( ~ less_than_or_equal(X1,l)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(upper_bound,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1360,plain,
! [X0] :
( sQ53_spl
| ~ less_than_or_equal(X0,q(f(l),l))
| ~ less_than_or_equal(g(q(f(l),l)),X0)
| ~ less_than_or_equal(l,l) ),
inference(resolution,[status(thm)],[f736,f317]) ).
fof(f1361,plain,
( sQ53_spl
| ~ less_than_or_equal(g(f(l)),f(l))
| ~ less_than_or_equal(l,l) ),
inference(resolution,[status(thm)],[f736,f33]) ).
fof(f1371,plain,
( sQ53_spl
| sQ62_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1360,f340,f839,f594]) ).
fof(f1372,plain,
( sQ53_spl
| ~ sQ3_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1361,f340,f72,f594]) ).
fof(f1401,plain,
! [X0,X1] :
( ~ sQ73_spl
| ~ less_than_or_equal(X1,l)
| less_than_or_equal(X1,X0)
| ~ less_than_or_equal(upper_bound,q(X0,X1))
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f620,f1133]) ).
fof(f1410,definition,
! [X0,X1] :
( sQ84_spl
<=> ( ~ less_than_or_equal(X1,l)
| less_than_or_equal(X1,X0)
| ~ less_than_or_equal(upper_bound,q(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1413,plain,
( ~ sQ73_spl
| sQ84_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1401,f266,f1410,f1132]) ).
fof(f1477,definition,
! [X0] :
( sQ92_spl
<=> ( ~ less_than_or_equal(l,X0)
| ~ less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1478,plain,
! [X0] :
( ~ sQ92_spl
| ~ less_than_or_equal(l,X0)
| ~ less_than_or_equal(X0,l) ),
inference(component_clause,[status(thm)],[f1477]) ).
fof(f1496,plain,
! [X0] :
( ~ sQ73_spl
| less_than_or_equal(l,X0)
| ~ less_than_or_equal(upper_bound,q(X0,l))
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f621,f1133]) ).
fof(f1505,definition,
! [X0] :
( sQ93_spl
<=> ( less_than_or_equal(l,X0)
| ~ less_than_or_equal(upper_bound,q(X0,l)) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1508,plain,
( ~ sQ73_spl
| sQ93_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1496,f266,f1505,f1132]) ).
fof(f1578,definition,
! [X0] :
( sQ95_spl
<=> ( ~ less_than_or_equal(X0,f(l))
| ~ less_than_or_equal(f(l),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1579,plain,
! [X0] :
( ~ sQ95_spl
| ~ less_than_or_equal(X0,f(l))
| ~ less_than_or_equal(f(l),X0) ),
inference(component_clause,[status(thm)],[f1578]) ).
fof(f1687,definition,
! [X0,X1] :
( sQ106_spl
<=> ( ~ less_than_or_equal(l,X0)
| ~ less_than_or_equal(X1,f(l))
| ~ less_than_or_equal(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1788,plain,
( ~ sQ92_spl
| ~ less_than_or_equal(l,l) ),
inference(resolution,[status(thm)],[f1478,f18]) ).
fof(f1797,plain,
( ~ sQ92_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1788,f340,f1477]) ).
fof(f1875,plain,
! [X0] :
( sQ53_spl
| less_than_or_equal(f(l),X0)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f895,f19]) ).
fof(f1967,definition,
! [X0] :
( sQ116_spl
<=> ( ~ less_than_or_equal(X0,l)
| less_than_or_equal(X0,upper_bound) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f2004,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(X0,l)
| less_than_or_equal(X2,h(q(l,X0)))
| ~ less_than_or_equal(f(X2),n0)
| ~ less_than_or_equal(X2,q(l,X0))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f677,f277]) ).
fof(f2007,definition,
! [X0,X1,X2] :
( sQ117_spl
<=> ( less_than_or_equal(X0,l)
| less_than_or_equal(X2,h(q(l,X0)))
| ~ less_than_or_equal(f(X2),n0)
| ~ less_than_or_equal(X2,q(l,X0))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f2010,plain,
( ~ sQ8_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f2004,f2007,f97]) ).
fof(f2104,plain,
! [X0,X1] :
( ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(X0,l)
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f678,f277]) ).
fof(f2107,definition,
! [X0,X1] :
( sQ118_spl
<=> ( less_than_or_equal(X0,l)
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f2110,plain,
( ~ sQ8_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f2104,f2107,f97]) ).
fof(f2112,plain,
! [X0,X1,X2] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X2,h(q(l,X0)))
| ~ less_than_or_equal(f(X2),n0)
| ~ less_than_or_equal(X2,q(l,X0))
| ~ less_than_or_equal(n0,n0)
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f675,f26]) ).
fof(f2113,plain,
! [X0,X1] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| ~ less_than_or_equal(n0,n0)
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f675,f24]) ).
fof(f2121,definition,
! [X0,X1,X2] :
( sQ119_spl
<=> ( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X2,h(q(l,X0)))
| ~ less_than_or_equal(f(X2),n0)
| ~ less_than_or_equal(X2,q(l,X0))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f2124,plain,
( ~ sQ17_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f2112,f2121,f184]) ).
fof(f2125,definition,
! [X0,X1] :
( sQ120_spl
<=> ( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(q(l,X0),X1)
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f2128,plain,
( ~ sQ17_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f2113,f2125,f184]) ).
fof(f2209,definition,
( sQ124_spl
<=> less_than_or_equal(l,q(l,k(l))) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f2211,plain,
( sQ124_spl
| ~ less_than_or_equal(l,q(l,k(l))) ),
inference(component_clause,[status(thm)],[f2209]) ).
fof(f2217,plain,
! [X0,X1] :
( ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(X0,l)
| less_than_or_equal(X1,h(q(l,X0)))
| ~ less_than_or_equal(f(X1),n0)
| ~ less_than_or_equal(X1,q(l,X0))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f700,f277]) ).
fof(f2220,definition,
! [X0,X1] :
( sQ125_spl
<=> ( less_than_or_equal(X0,l)
| less_than_or_equal(X1,h(q(l,X0)))
| ~ less_than_or_equal(f(X1),n0)
| ~ less_than_or_equal(X1,q(l,X0))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f2223,plain,
( ~ sQ8_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f2217,f2220,f97]) ).
fof(f2225,plain,
! [X0] :
( ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(X0,l)
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f701,f277]) ).
fof(f2228,definition,
! [X0] :
( sQ126_spl
<=> ( less_than_or_equal(X0,l)
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f2231,plain,
( ~ sQ8_spl
| sQ126_spl ),
inference(split_clause,[status(thm)],[f2225,f2228,f97]) ).
fof(f2275,plain,
! [X0,X1] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X1,h(q(l,X0)))
| ~ less_than_or_equal(f(X1),n0)
| ~ less_than_or_equal(X1,q(l,X0))
| ~ less_than_or_equal(n0,n0)
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f698,f26]) ).
fof(f2276,plain,
! [X0] :
( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| ~ less_than_or_equal(n0,n0)
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f698,f24]) ).
fof(f2284,definition,
! [X0,X1] :
( sQ127_spl
<=> ( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| less_than_or_equal(X1,h(q(l,X0)))
| ~ less_than_or_equal(f(X1),n0)
| ~ less_than_or_equal(X1,q(l,X0))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f2287,plain,
( ~ sQ17_spl
| sQ127_spl ),
inference(split_clause,[status(thm)],[f2275,f2284,f184]) ).
fof(f2288,definition,
! [X0] :
( sQ128_spl
<=> ( ~ less_than_or_equal(q(l,X0),upper_bound)
| ~ less_than_or_equal(lower_bound,q(l,X0))
| ~ less_than_or_equal(q(l,X0),h(q(l,X0)))
| less_than_or_equal(upper_bound,q(l,X0))
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f2291,plain,
( ~ sQ17_spl
| sQ128_spl ),
inference(split_clause,[status(thm)],[f2276,f2288,f184]) ).
fof(f2301,plain,
( ~ sQ50_spl
| less_than_or_equal(k(l),l)
| ~ less_than_or_equal(l,q(l,k(l)))
| less_than_or_equal(upper_bound,q(l,k(l)))
| less_than_or_equal(k(l),l) ),
inference(resolution,[status(thm)],[f699,f593]) ).
fof(f2309,definition,
( sQ131_spl
<=> less_than_or_equal(upper_bound,q(l,k(l))) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f2310,plain,
( ~ sQ131_spl
| less_than_or_equal(upper_bound,q(l,k(l))) ),
inference(component_clause,[status(thm)],[f2309]) ).
fof(f2312,plain,
( ~ sQ50_spl
| ~ sQ124_spl
| sQ131_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f2301,f563,f2309,f2209,f559]) ).
fof(f2375,definition,
! [X0,X1] :
( sQ136_spl
<=> ( ~ less_than_or_equal(upper_bound,X0)
| ~ less_than_or_equal(X1,f(l))
| ~ less_than_or_equal(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f2598,plain,
( sQ53_spl
| less_than_or_equal(f(l),l)
| less_than_or_equal(f(l),l) ),
inference(resolution,[status(thm)],[f1875,f895]) ).
fof(f2614,plain,
( sQ53_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f2598,f347,f594]) ).
fof(f2742,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ less_than_or_equal(X0,l)
| ~ less_than_or_equal(upper_bound,X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f745,f101]) ).
fof(f2814,plain,
( sQ124_spl
| less_than_or_equal(k(l),l) ),
inference(resolution,[status(thm)],[f2211,f69]) ).
fof(f2818,plain,
( sQ124_spl
| sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2814,f565]) ).
fof(f2819,plain,
( sQ124_spl
| sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f2818]) ).
fof(f2913,plain,
! [X0,X1] :
( ~ sQ39_spl
| ~ less_than_or_equal(upper_bound,X1)
| ~ less_than_or_equal(X1,X0)
| ~ less_than_or_equal(X0,l)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f742,f450]) ).
fof(f2931,plain,
( ~ sQ39_spl
| sQ81_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f2913,f266,f1315,f449]) ).
fof(f3080,plain,
! [X0] :
( less_than_or_equal(l,q(upper_bound,X0))
| ~ less_than_or_equal(X0,l)
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f759,f31]) ).
fof(f3180,plain,
! [X0,X1] :
( ~ sQ39_spl
| ~ less_than_or_equal(q(upper_bound,X0),X1)
| ~ less_than_or_equal(X1,l)
| less_than_or_equal(upper_bound,l)
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f751,f450]) ).
fof(f3199,definition,
! [X0,X1] :
( sQ163_spl
<=> ( ~ less_than_or_equal(q(upper_bound,X0),X1)
| ~ less_than_or_equal(X1,l)
| less_than_or_equal(X0,upper_bound) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f3202,plain,
( ~ sQ39_spl
| sQ28_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f3180,f3199,f266,f449]) ).
fof(f3211,plain,
! [X0] :
( ~ sQ39_spl
| ~ less_than_or_equal(q(upper_bound,X0),l)
| less_than_or_equal(upper_bound,l)
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f752,f450]) ).
fof(f3230,definition,
! [X0] :
( sQ164_spl
<=> ( ~ less_than_or_equal(q(upper_bound,X0),l)
| less_than_or_equal(X0,upper_bound) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f3233,plain,
( ~ sQ39_spl
| sQ28_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f3211,f3230,f266,f449]) ).
fof(f3299,plain,
( ~ sQ131_spl
| ~ less_than_or_equal(k(l),upper_bound)
| less_than_or_equal(k(l),l) ),
inference(resolution,[status(thm)],[f2310,f65]) ).
fof(f3317,plain,
( ~ sQ131_spl
| ~ sQ56_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f3299,f563,f609,f2309]) ).
fof(f3318,plain,
! [X0] :
( ~ less_than_or_equal(X0,l)
| less_than_or_equal(X0,upper_bound) ),
inference(forward_subsumption_resolution,[status(thm)],[f3080,f65]) ).
fof(f3322,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(l,X1)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f267,f745]) ).
fof(f3348,plain,
! [X0,X1] :
( ~ less_than_or_equal(X1,l)
| ~ less_than_or_equal(X0,X1)
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f3318,f21]) ).
fof(f3382,plain,
( ~ sQ70_spl
| ~ less_than_or_equal(f(upper_bound),n0)
| ~ less_than_or_equal(upper_bound,upper_bound)
| ~ less_than_or_equal(l,l) ),
inference(resolution,[status(thm)],[f1062,f30]) ).
fof(f3389,plain,
( ~ sQ70_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f3382,f340,f291,f294,f1061]) ).
fof(f3411,plain,
! [X0] :
( ~ sQ10_spl
| less_than_or_equal(l,X0)
| less_than_or_equal(g(X0),h(l))
| ~ less_than_or_equal(g(X0),l) ),
inference(resolution,[status(thm)],[f106,f32]) ).
fof(f3535,definition,
! [X0] :
( sQ170_spl
<=> ( ~ less_than_or_equal(n0,X0)
| ~ less_than_or_equal(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f3536,plain,
! [X0] :
( ~ sQ170_spl
| ~ less_than_or_equal(n0,X0)
| ~ less_than_or_equal(X0,n0) ),
inference(component_clause,[status(thm)],[f3535]) ).
fof(f3602,plain,
( ~ sQ170_spl
| ~ less_than_or_equal(n0,n0) ),
inference(resolution,[status(thm)],[f3536,f18]) ).
fof(f3607,plain,
( ~ sQ170_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f3602,f184,f3535]) ).
fof(f3920,plain,
! [X0] :
( ~ sQ10_spl
| ~ less_than_or_equal(f(g(X0)),n0)
| ~ less_than_or_equal(g(X0),upper_bound)
| less_than_or_equal(l,X0)
| less_than_or_equal(g(X0),h(l)) ),
inference(resolution,[status(thm)],[f3411,f30]) ).
fof(f3923,plain,
! [X0] :
( ~ sQ10_spl
| ~ less_than_or_equal(f(g(X0)),n0)
| less_than_or_equal(l,X0)
| less_than_or_equal(g(X0),h(l)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3920,f31]) ).
fof(f4212,plain,
! [X0,X1] :
( ~ sQ9_spl
| less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(X0,l)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f2742,f19]) ).
fof(f4386,plain,
( sQ3_spl
| less_than_or_equal(l,f(l))
| ~ less_than_or_equal(upper_bound,f(l)) ),
inference(resolution,[status(thm)],[f374,f31]) ).
fof(f4395,plain,
( sQ3_spl
| sQ53_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f4386,f927,f594,f72]) ).
fof(f4445,plain,
! [X0,X1] :
( less_than_or_equal(l,X1)
| ~ less_than_or_equal(X0,X1)
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f3348,f19]) ).
fof(f4468,plain,
! [X0] :
( sQ40_spl
| ~ less_than_or_equal(X0,h(q(l,upper_bound)))
| ~ less_than_or_equal(upper_bound,X0)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f455,f528]) ).
fof(f4469,plain,
! [X0] :
( sQ40_spl
| ~ less_than_or_equal(X0,q(h(q(l,upper_bound)),q(l,upper_bound)))
| ~ less_than_or_equal(upper_bound,X0)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f455,f524]) ).
fof(f4470,plain,
( sQ40_spl
| ~ less_than_or_equal(upper_bound,h(q(l,upper_bound)))
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f455,f149]) ).
fof(f4473,definition,
! [X0] :
( sQ203_spl
<=> ( ~ less_than_or_equal(X0,h(q(l,upper_bound)))
| ~ less_than_or_equal(upper_bound,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f4476,plain,
( sQ40_spl
| sQ203_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f4468,f266,f4473,f453]) ).
fof(f4477,definition,
! [X0] :
( sQ204_spl
<=> ( ~ less_than_or_equal(X0,q(h(q(l,upper_bound)),q(l,upper_bound)))
| ~ less_than_or_equal(upper_bound,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f4480,plain,
( sQ40_spl
| sQ204_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f4469,f266,f4477,f453]) ).
fof(f4481,definition,
( sQ205_spl
<=> less_than_or_equal(upper_bound,h(q(l,upper_bound))) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f4484,plain,
( sQ40_spl
| ~ sQ205_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f4470,f266,f4481,f453]) ).
fof(f4485,plain,
( ~ sQ37_spl
| less_than_or_equal(lower_bound,h(q(l,upper_bound)))
| ~ less_than_or_equal(lower_bound,q(l,upper_bound)) ),
inference(resolution,[status(thm)],[f444,f35]) ).
fof(f4491,definition,
( sQ206_spl
<=> less_than_or_equal(lower_bound,h(q(l,upper_bound))) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f4494,plain,
( ~ sQ37_spl
| sQ206_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f4485,f446,f4491,f443]) ).
fof(f4654,definition,
( sQ213_spl
<=> less_than_or_equal(upper_bound,q(f(l),l)) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f4655,plain,
( ~ sQ213_spl
| less_than_or_equal(upper_bound,q(f(l),l)) ),
inference(component_clause,[status(thm)],[f4654]) ).
fof(f4656,plain,
( sQ213_spl
| ~ less_than_or_equal(upper_bound,q(f(l),l)) ),
inference(component_clause,[status(thm)],[f4654]) ).
fof(f4661,definition,
( sQ215_spl
<=> less_than_or_equal(g(q(f(l),l)),upper_bound) ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f4663,plain,
( sQ215_spl
| ~ less_than_or_equal(g(q(f(l),l)),upper_bound) ),
inference(component_clause,[status(thm)],[f4661]) ).
fof(f4668,plain,
! [X0] :
( sQ213_spl
| ~ less_than_or_equal(upper_bound,X0)
| ~ less_than_or_equal(X0,f(l))
| less_than_or_equal(l,f(l)) ),
inference(resolution,[status(thm)],[f4656,f743]) ).
fof(f4671,plain,
( sQ213_spl
| less_than_or_equal(q(f(l),l),upper_bound) ),
inference(resolution,[status(thm)],[f4656,f19]) ).
fof(f4672,plain,
( sQ213_spl
| sQ59_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f4668,f594,f723,f4654]) ).
fof(f4675,plain,
! [X0] :
( sQ213_spl
| ~ less_than_or_equal(q(upper_bound,X0),f(l))
| less_than_or_equal(l,f(l))
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f4671,f752]) ).
fof(f4676,plain,
! [X0,X1] :
( sQ213_spl
| ~ less_than_or_equal(q(upper_bound,X0),X1)
| ~ less_than_or_equal(X1,f(l))
| less_than_or_equal(l,f(l))
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f4671,f751]) ).
fof(f4677,plain,
! [X0,X1] :
( sQ213_spl
| ~ less_than_or_equal(upper_bound,X1)
| ~ less_than_or_equal(X1,X0)
| ~ less_than_or_equal(X0,f(l))
| less_than_or_equal(l,f(l)) ),
inference(resolution,[status(thm)],[f4671,f742]) ).
fof(f4685,definition,
! [X0] :
( sQ218_spl
<=> ( ~ less_than_or_equal(q(upper_bound,X0),f(l))
| less_than_or_equal(X0,upper_bound) ) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f4688,plain,
( sQ213_spl
| sQ53_spl
| sQ218_spl ),
inference(split_clause,[status(thm)],[f4675,f4685,f594,f4654]) ).
fof(f4689,definition,
! [X0,X1] :
( sQ219_spl
<=> ( ~ less_than_or_equal(q(upper_bound,X0),X1)
| ~ less_than_or_equal(X1,f(l))
| less_than_or_equal(X0,upper_bound) ) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f4692,plain,
( sQ213_spl
| sQ53_spl
| sQ219_spl ),
inference(split_clause,[status(thm)],[f4676,f4689,f594,f4654]) ).
fof(f4693,plain,
( sQ213_spl
| sQ136_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f4677,f594,f2375,f4654]) ).
fof(f4707,plain,
( ~ sQ95_spl
| ~ less_than_or_equal(f(l),f(l)) ),
inference(resolution,[status(thm)],[f1579,f18]) ).
fof(f4711,plain,
( ~ sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4707,f18]) ).
fof(f4712,plain,
~ sQ95_spl,
inference(contradiction_clause,[status(thm)],[f4711]) ).
fof(f4805,definition,
! [X0,X1] :
( sQ220_spl
<=> ( ~ less_than_or_equal(X1,n0)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f4806,plain,
! [X0,X1] :
( ~ sQ220_spl
| ~ less_than_or_equal(X1,n0)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(n0,X0) ),
inference(component_clause,[status(thm)],[f4805]) ).
fof(f4839,plain,
( ~ sQ34_spl
| less_than_or_equal(f(l),upper_bound) ),
inference(resolution,[status(thm)],[f348,f3318]) ).
fof(f4842,plain,
( ~ sQ34_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f4839,f192,f347]) ).
fof(f5105,plain,
! [X0] :
( sQ0_spl
| ~ less_than_or_equal(f(lower_bound),n0)
| ~ less_than_or_equal(lower_bound,upper_bound)
| ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(l,h(l))
| ~ less_than_or_equal(X0,f(l))
| ~ less_than_or_equal(f(l),X0) ),
inference(resolution,[status(thm)],[f513,f30]) ).
fof(f5118,plain,
( sQ0_spl
| ~ sQ12_spl
| ~ sQ11_spl
| ~ sQ9_spl
| ~ sQ7_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f5105,f1578,f94,f100,f115,f118,f38]) ).
fof(f5321,plain,
! [X0,X1] :
( ~ sQ9_spl
| less_than_or_equal(l,X0)
| less_than_or_equal(X1,upper_bound)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f4212,f19]) ).
fof(f5323,definition,
! [X0] :
( sQ245_spl
<=> ( less_than_or_equal(X0,upper_bound)
| less_than_or_equal(l,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f5514,plain,
! [X0,X1] :
( ~ less_than_or_equal(X1,l)
| less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(X0,l)
| less_than_or_equal(X0,upper_bound) ),
inference(resolution,[status(thm)],[f4445,f3348]) ).
fof(f5539,plain,
sQ116_spl,
inference(split_clause,[status(thm)],[f5514,f1967]) ).
fof(f5585,plain,
( sQ215_spl
| less_than_or_equal(l,q(f(l),l)) ),
inference(resolution,[status(thm)],[f4663,f31]) ).
fof(f5595,plain,
! [X0,X1] :
( sQ215_spl
| ~ less_than_or_equal(X1,l)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(l,X0)
| less_than_or_equal(l,f(l)) ),
inference(resolution,[status(thm)],[f5585,f527]) ).
fof(f5608,definition,
! [X0,X1] :
( sQ253_spl
<=> ( ~ less_than_or_equal(X1,l)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(l,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f5609,plain,
! [X0,X1] :
( ~ sQ253_spl
| ~ less_than_or_equal(X1,l)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(l,X0) ),
inference(component_clause,[status(thm)],[f5608]) ).
fof(f5611,plain,
( sQ215_spl
| sQ253_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f5595,f594,f5608,f4661]) ).
fof(f5696,plain,
! [X0] :
( ~ sQ220_spl
| ~ less_than_or_equal(X0,n0)
| ~ less_than_or_equal(n0,X0) ),
inference(resolution,[status(thm)],[f4806,f18]) ).
fof(f5707,plain,
( ~ sQ220_spl
| sQ170_spl ),
inference(split_clause,[status(thm)],[f5696,f3535,f4805]) ).
fof(f5985,plain,
! [X0,X1] :
( ~ sQ213_spl
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(l,X0)
| less_than_or_equal(l,f(l)) ),
inference(resolution,[status(thm)],[f4655,f527]) ).
fof(f5989,definition,
! [X0] :
( sQ269_spl
<=> ( less_than_or_equal(upper_bound,X0)
| ~ less_than_or_equal(l,q(X0,upper_bound)) ) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f5990,plain,
! [X0] :
( ~ sQ269_spl
| less_than_or_equal(upper_bound,X0)
| ~ less_than_or_equal(l,q(X0,upper_bound)) ),
inference(component_clause,[status(thm)],[f5989]) ).
fof(f5997,definition,
! [X0,X1] :
( sQ271_spl
<=> ( ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(l,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f5998,plain,
! [X0,X1] :
( ~ sQ271_spl
| ~ less_than_or_equal(X1,upper_bound)
| ~ less_than_or_equal(X0,X1)
| ~ less_than_or_equal(l,X0) ),
inference(component_clause,[status(thm)],[f5997]) ).
fof(f6000,plain,
( ~ sQ213_spl
| sQ271_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f5985,f594,f5997,f4654]) ).
fof(f6019,plain,
( ~ sQ80_spl
| ~ less_than_or_equal(l,upper_bound) ),
inference(resolution,[status(thm)],[f1222,f18]) ).
fof(f6024,plain,
( ~ sQ80_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f6019,f100,f1221]) ).
fof(f6095,plain,
! [X0,X1] :
( ~ sQ9_spl
| less_than_or_equal(X1,upper_bound)
| less_than_or_equal(l,X1)
| less_than_or_equal(X0,upper_bound)
| less_than_or_equal(l,X0) ),
inference(resolution,[status(thm)],[f5321,f4212]) ).
fof(f6121,plain,
( ~ sQ9_spl
| sQ245_spl ),
inference(split_clause,[status(thm)],[f6095,f5323,f100]) ).
fof(f6432,plain,
! [X0] :
( ~ sQ253_spl
| ~ less_than_or_equal(X0,l)
| ~ less_than_or_equal(l,X0) ),
inference(resolution,[status(thm)],[f5609,f18]) ).
fof(f6436,plain,
( ~ sQ253_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f6432,f1477,f5608]) ).
fof(f6454,plain,
! [X0] :
( ~ sQ271_spl
| ~ less_than_or_equal(X0,upper_bound)
| ~ less_than_or_equal(l,X0) ),
inference(resolution,[status(thm)],[f5998,f18]) ).
fof(f6456,plain,
( ~ sQ271_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f6454,f1221,f5997]) ).
fof(f6465,plain,
( ~ sQ269_spl
| less_than_or_equal(upper_bound,l)
| less_than_or_equal(upper_bound,l) ),
inference(resolution,[status(thm)],[f5990,f69]) ).
fof(f6471,plain,
( ~ sQ269_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f6465,f266,f5989]) ).
fof(f6486,plain,
! [X0,X1] :
( ~ sQ28_spl
| less_than_or_equal(X1,l)
| ~ less_than_or_equal(X0,upper_bound)
| less_than_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f3322,f19]) ).
fof(f6876,definition,
! [X1] :
( sQ314_spl
<=> ( less_than_or_equal(X1,l)
| less_than_or_equal(upper_bound,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f6877,plain,
! [X0] :
( ~ sQ314_spl
| less_than_or_equal(X0,l)
| less_than_or_equal(upper_bound,X0) ),
inference(component_clause,[status(thm)],[f6876]) ).
fof(f6927,plain,
( sQ213_spl
| ~ sQ314_spl
| less_than_or_equal(q(f(l),l),l) ),
inference(resolution,[status(thm)],[f6877,f4656]) ).
fof(f7044,plain,
! [X0] :
( ~ sQ28_spl
| less_than_or_equal(X0,l)
| less_than_or_equal(upper_bound,X0) ),
inference(resolution,[status(thm)],[f6486,f18]) ).
fof(f7060,plain,
( ~ sQ28_spl
| sQ314_spl ),
inference(split_clause,[status(thm)],[f7044,f6876,f266]) ).
fof(f7205,plain,
! [X0] :
( sQ213_spl
| ~ sQ314_spl
| ~ less_than_or_equal(q(l,X0),f(l))
| less_than_or_equal(l,f(l))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f6927,f752]) ).
fof(f7206,plain,
! [X0,X1] :
( sQ213_spl
| ~ sQ314_spl
| ~ less_than_or_equal(q(l,X0),X1)
| ~ less_than_or_equal(X1,f(l))
| less_than_or_equal(l,f(l))
| less_than_or_equal(X0,l) ),
inference(resolution,[status(thm)],[f6927,f751]) ).
fof(f7207,plain,
! [X0,X1] :
( sQ213_spl
| ~ sQ314_spl
| ~ less_than_or_equal(l,X1)
| ~ less_than_or_equal(X1,X0)
| ~ less_than_or_equal(X0,f(l))
| less_than_or_equal(l,f(l)) ),
inference(resolution,[status(thm)],[f6927,f742]) ).
fof(f7208,plain,
! [X0] :
( sQ213_spl
| ~ sQ314_spl
| ~ less_than_or_equal(l,X0)
| ~ less_than_or_equal(X0,f(l))
| less_than_or_equal(l,f(l)) ),
inference(resolution,[status(thm)],[f6927,f276]) ).
fof(f7219,definition,
! [X0] :
( sQ329_spl
<=> ( ~ less_than_or_equal(q(l,X0),f(l))
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition]) ).
fof(f7222,plain,
( sQ213_spl
| ~ sQ314_spl
| sQ53_spl
| sQ329_spl ),
inference(split_clause,[status(thm)],[f7205,f7219,f594,f6876,f4654]) ).
fof(f7223,definition,
! [X0,X1] :
( sQ330_spl
<=> ( ~ less_than_or_equal(q(l,X0),X1)
| ~ less_than_or_equal(X1,f(l))
| less_than_or_equal(X0,l) ) ),
introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition]) ).
fof(f7226,plain,
( sQ213_spl
| ~ sQ314_spl
| sQ53_spl
| sQ330_spl ),
inference(split_clause,[status(thm)],[f7206,f7223,f594,f6876,f4654]) ).
fof(f7227,plain,
( sQ213_spl
| ~ sQ314_spl
| sQ106_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f7207,f594,f1687,f6876,f4654]) ).
fof(f7228,plain,
( sQ213_spl
| ~ sQ314_spl
| sQ58_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f7208,f594,f647,f6876,f4654]) ).
fof(f7263,plain,
! [X0] :
( ~ sQ10_spl
| less_than_or_equal(l,X0)
| less_than_or_equal(g(X0),h(l)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3923,f32]) ).
fof(f7264,plain,
( sQ7_spl
| ~ sQ10_spl
| less_than_or_equal(l,h(l)) ),
inference(resolution,[status(thm)],[f7263,f371]) ).
fof(f7278,plain,
( ~ sQ10_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f7264,f94,f105]) ).
fof(f7289,plain,
$false,
inference(sat_refutation,[status(thm)],[f44,f59,f121,f187,f200,f272,f299,f352,f377,f422,f452,f456,f466,f551,f562,f566,f828,f1022,f1024,f1064,f1138,f1142,f1151,f1169,f1371,f1372,f1413,f1508,f1797,f2010,f2110,f2124,f2128,f2223,f2231,f2287,f2291,f2312,f2614,f2819,f2931,f3202,f3233,f3317,f3389,f3607,f4395,f4476,f4480,f4484,f4494,f4672,f4688,f4692,f4693,f4712,f4842,f5118,f5539,f5611,f5707,f6000,f6024,f6121,f6436,f6456,f6471,f7060,f7222,f7226,f7227,f7228,f7278]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA002-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n011.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 13:21:40 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 65.15/8.64 % Refutation found
% 65.15/8.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 65.15/8.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 65.15/8.69 % Elapsed time: 8.295101 seconds
% 65.15/8.69 % CPU time: 65.580558 seconds
% 65.15/8.69 % Total memory used: 139.697 MB
% 65.15/8.69 % Net memory used: 107.572 MB
%------------------------------------------------------------------------------