%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM858+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 01:41:52 PM UTC 2026
% Result : Theorem 59.89s 8.01s
% Output : CNFRefutation 54.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 124
% Syntax : Number of formulae : 710 ( 17 unt; 111 def)
% Number of atoms : 1981 ( 232 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 2200 ( 929 ~;1108 |; 37 &)
% ( 121 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 119 ( 117 usr; 112 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 414 ( 404 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : lesseq(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( lesseq(Y,Z)
& lesseq(X,Y) )
=> lesseq(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( ( lesseq(Y,X)
& lesseq(X,Y) )
=> X = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( lesseq(Y,X)
| lesseq(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] :
( lesseq(X,Y)
<=> lesseq(sum(Z,X),sum(Z,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] :
( ~ lesseq(Y,X)
| max(X,Y) = X ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( ~ lesseq(X,Y)
| max(X,Y) = Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,Z] :
( ub(X,Y,Z)
<=> ( lesseq(Y,Z)
& lesseq(X,Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y,N] :
( model_max(X,Y,N)
<=> N = max(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y,N] :
( model_ub(X,Y,N)
<=> ub(X,Y,N) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y,N] :
( minsol_model_max(X,Y,N)
<=> ( ! [Z] :
( model_max(X,Y,Z)
=> lesseq(N,Z) )
& model_max(X,Y,N) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y,N] :
( minsol_model_ub(X,Y,N)
<=> ( ! [Z] :
( model_ub(X,Y,Z)
=> lesseq(N,Z) )
& model_ub(X,Y,N) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,conjecture,
! [X,Y,Z] :
( minsol_model_ub(X,Y,Z)
<=> minsol_model_max(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
~ ! [X,Y,Z] :
( minsol_model_ub(X,Y,Z)
<=> minsol_model_max(X,Y,Z) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
! [X0] : lesseq(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
! [X,Y,Z] :
( lesseq(X,Z)
| ~ lesseq(Y,Z)
| ~ lesseq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
! [X,Z] :
( lesseq(X,Z)
| ! [Y] :
( ~ lesseq(Y,Z)
| ~ lesseq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f19,plain,
! [X0,X1,X2] :
( lesseq(X0,X2)
| ~ lesseq(X1,X2)
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f20,plain,
! [X,Y] :
( X = Y
| ~ lesseq(Y,X)
| ~ lesseq(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f21,plain,
! [X0,X1] :
( X0 = X1
| ~ lesseq(X1,X0)
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
! [X0,X1] :
( lesseq(X1,X0)
| lesseq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f23,plain,
! [X,Y,Z] :
( ( ~ lesseq(sum(Z,X),sum(Z,Y))
| lesseq(X,Y) )
& ( lesseq(sum(Z,X),sum(Z,Y))
| ~ lesseq(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f24,plain,
( ! [X,Y] :
( ! [Z] : ~ lesseq(sum(Z,X),sum(Z,Y))
| lesseq(X,Y) )
& ! [X,Y] :
( ! [Z] : lesseq(sum(Z,X),sum(Z,Y))
| ~ lesseq(X,Y) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f25,plain,
! [X0,X1,X2] :
( lesseq(sum(X2,X0),sum(X2,X1))
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f26,plain,
! [X0,X1,X2] :
( ~ lesseq(sum(X2,X0),sum(X2,X1))
| lesseq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f31,plain,
! [X0,X1] :
( ~ lesseq(X1,X0)
| max(X0,X1) = X0 ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f32,plain,
! [X0,X1] :
( ~ lesseq(X0,X1)
| max(X0,X1) = X1 ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f33,plain,
! [X,Y,Z] :
( ( ~ lesseq(Y,Z)
| ~ lesseq(X,Z)
| ub(X,Y,Z) )
& ( ( lesseq(Y,Z)
& lesseq(X,Z) )
| ~ ub(X,Y,Z) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f34,plain,
( ! [X,Y,Z] :
( ~ lesseq(Y,Z)
| ~ lesseq(X,Z)
| ub(X,Y,Z) )
& ! [X,Y,Z] :
( ( lesseq(Y,Z)
& lesseq(X,Z) )
| ~ ub(X,Y,Z) ) ),
inference(miniscoping,[status(thm)],[f33]) ).
fof(f35,plain,
! [X0,X1,X2] :
( lesseq(X0,X2)
| ~ ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
! [X0,X1,X2] :
( lesseq(X1,X2)
| ~ ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f37,plain,
! [X0,X1,X2] :
( ~ lesseq(X1,X2)
| ~ lesseq(X0,X2)
| ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f38,plain,
! [X,Y,N] :
( ( N != max(X,Y)
| model_max(X,Y,N) )
& ( N = max(X,Y)
| ~ model_max(X,Y,N) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f39,plain,
( ! [X,Y,N] :
( N != max(X,Y)
| model_max(X,Y,N) )
& ! [X,Y,N] :
( N = max(X,Y)
| ~ model_max(X,Y,N) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0,X1,X2] :
( X2 = max(X0,X1)
| ~ model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [X0,X1,X2] :
( X2 != max(X0,X1)
| model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f42,plain,
! [X,Y,N] :
( ( ~ ub(X,Y,N)
| model_ub(X,Y,N) )
& ( ub(X,Y,N)
| ~ model_ub(X,Y,N) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f43,plain,
( ! [X,Y,N] :
( ~ ub(X,Y,N)
| model_ub(X,Y,N) )
& ! [X,Y,N] :
( ub(X,Y,N)
| ~ model_ub(X,Y,N) ) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f45,plain,
! [X0,X1,X2] :
( ~ ub(X0,X1,X2)
| model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f46,plain,
! [X,Y,N] :
( minsol_model_max(X,Y,N)
<=> ( ! [Z] :
( lesseq(N,Z)
| ~ model_max(X,Y,Z) )
& model_max(X,Y,N) ) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f47,plain,
! [X,Y,N] :
( ( ? [Z] :
( ~ lesseq(N,Z)
& model_max(X,Y,Z) )
| ~ model_max(X,Y,N)
| minsol_model_max(X,Y,N) )
& ( ( ! [Z] :
( lesseq(N,Z)
| ~ model_max(X,Y,Z) )
& model_max(X,Y,N) )
| ~ minsol_model_max(X,Y,N) ) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
( ! [X,Y,N] :
( ? [Z] :
( ~ lesseq(N,Z)
& model_max(X,Y,Z) )
| ~ model_max(X,Y,N)
| minsol_model_max(X,Y,N) )
& ! [X,Y,N] :
( ( ! [Z] :
( lesseq(N,Z)
| ~ model_max(X,Y,Z) )
& model_max(X,Y,N) )
| ~ minsol_model_max(X,Y,N) ) ),
inference(miniscoping,[status(thm)],[f47]) ).
fof(f49,plain,
( ! [X,Y,N] :
( ( ~ lesseq(N,sK0_skl(N,Y,X))
& model_max(X,Y,sK0_skl(N,Y,X)) )
| ~ model_max(X,Y,N)
| minsol_model_max(X,Y,N) )
& ! [X,Y,N] :
( ( ! [Z] :
( lesseq(N,Z)
| ~ model_max(X,Y,Z) )
& model_max(X,Y,N) )
| ~ minsol_model_max(X,Y,N) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Z,sK0_skl(N,Y,X))],[f48]) ).
fof(f50,plain,
! [X0,X1,X2] :
( model_max(X0,X1,X2)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2,X3] :
( lesseq(X2,X3)
| ~ model_max(X0,X1,X3)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f52,plain,
! [X0,X1,X2] :
( model_max(X0,X1,sK0_skl(X2,X1,X0))
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ~ lesseq(X2,sK0_skl(X2,X1,X0))
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f54,plain,
! [X,Y,N] :
( minsol_model_ub(X,Y,N)
<=> ( ! [Z] :
( lesseq(N,Z)
| ~ model_ub(X,Y,Z) )
& model_ub(X,Y,N) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f55,plain,
! [X,Y,N] :
( ( ? [Z] :
( ~ lesseq(N,Z)
& model_ub(X,Y,Z) )
| ~ model_ub(X,Y,N)
| minsol_model_ub(X,Y,N) )
& ( ( ! [Z] :
( lesseq(N,Z)
| ~ model_ub(X,Y,Z) )
& model_ub(X,Y,N) )
| ~ minsol_model_ub(X,Y,N) ) ),
inference(NNF_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
( ! [X,Y,N] :
( ? [Z] :
( ~ lesseq(N,Z)
& model_ub(X,Y,Z) )
| ~ model_ub(X,Y,N)
| minsol_model_ub(X,Y,N) )
& ! [X,Y,N] :
( ( ! [Z] :
( lesseq(N,Z)
| ~ model_ub(X,Y,Z) )
& model_ub(X,Y,N) )
| ~ minsol_model_ub(X,Y,N) ) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f57,plain,
( ! [X,Y,N] :
( ( ~ lesseq(N,sK1_skl(N,Y,X))
& model_ub(X,Y,sK1_skl(N,Y,X)) )
| ~ model_ub(X,Y,N)
| minsol_model_ub(X,Y,N) )
& ! [X,Y,N] :
( ( ! [Z] :
( lesseq(N,Z)
| ~ model_ub(X,Y,Z) )
& model_ub(X,Y,N) )
| ~ minsol_model_ub(X,Y,N) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Z,sK1_skl(N,Y,X))],[f56]) ).
fof(f58,plain,
! [X0,X1,X2] :
( model_ub(X0,X1,X2)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( lesseq(X2,X3)
| ~ model_ub(X0,X1,X3)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f60,plain,
! [X0,X1,X2] :
( model_ub(X0,X1,sK1_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f61,plain,
! [X0,X1,X2] :
( ~ lesseq(X2,sK1_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f62,plain,
? [X,Y,Z] :
( minsol_model_ub(X,Y,Z)
<~> minsol_model_max(X,Y,Z) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f63,plain,
? [X,Y,Z] :
( ( ~ minsol_model_max(X,Y,Z)
| ~ minsol_model_ub(X,Y,Z) )
& ( minsol_model_max(X,Y,Z)
| minsol_model_ub(X,Y,Z) ) ),
inference(NNF_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
( ( ~ minsol_model_max(sK2_skl,sK3_skl,sK4_skl)
| ~ minsol_model_ub(sK2_skl,sK3_skl,sK4_skl) )
& ( minsol_model_max(sK2_skl,sK3_skl,sK4_skl)
| minsol_model_ub(sK2_skl,sK3_skl,sK4_skl) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl),skolemize(Z,sK4_skl)],[f63]) ).
fof(f65,plain,
( minsol_model_max(sK2_skl,sK3_skl,sK4_skl)
| minsol_model_ub(sK2_skl,sK3_skl,sK4_skl) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
( ~ minsol_model_max(sK2_skl,sK3_skl,sK4_skl)
| ~ minsol_model_ub(sK2_skl,sK3_skl,sK4_skl) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,definition,
( sQ0_spl
<=> minsol_model_ub(sK2_skl,sK3_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f68,plain,
( ~ sQ0_spl
| minsol_model_ub(sK2_skl,sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f67]) ).
fof(f69,plain,
( sQ0_spl
| ~ minsol_model_ub(sK2_skl,sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f67]) ).
fof(f70,definition,
( sQ1_spl
<=> minsol_model_max(sK2_skl,sK3_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f71,plain,
( ~ sQ1_spl
| minsol_model_max(sK2_skl,sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f70]) ).
fof(f72,plain,
( sQ1_spl
| ~ minsol_model_max(sK2_skl,sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f70]) ).
fof(f73,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f65,f67,f70]) ).
fof(f74,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f66,f67,f70]) ).
fof(f75,plain,
! [X0,X1] : model_max(X0,X1,max(X0,X1)),
inference(destructive_equality_resolution,[status(thm)],[f41]) ).
fof(f76,plain,
! [X0] : max(X0,X0) = X0,
inference(resolution,[status(thm)],[f31,f22]) ).
fof(f77,plain,
! [X0,X1] :
( lesseq(X0,X1)
| max(X0,X1) = X0 ),
inference(resolution,[status(thm)],[f31,f22]) ).
fof(f90,plain,
! [X0] : model_max(X0,X0,X0),
inference(paramodulation,[status(thm)],[f76,f75]) ).
fof(f92,plain,
! [X0,X1] :
( lesseq(X1,X0)
| max(X0,X1) = X1 ),
inference(resolution,[status(thm)],[f32,f22]) ).
fof(f96,plain,
! [X0,X1,X2,X3] :
( ~ model_ub(X2,X3,X1)
| ~ minsol_model_ub(X2,X3,X0)
| max(X0,X1) = X1 ),
inference(resolution,[status(thm)],[f32,f59]) ).
fof(f97,plain,
! [X0,X1,X2,X3] :
( ~ model_max(X2,X3,X1)
| ~ minsol_model_max(X2,X3,X0)
| max(X0,X1) = X1 ),
inference(resolution,[status(thm)],[f32,f51]) ).
fof(f98,plain,
! [X0,X1] :
( max(X0,X1) = X1
| max(X0,X1) = X0 ),
inference(resolution,[status(thm)],[f77,f32]) ).
fof(f99,plain,
! [X0,X1] :
( max(X1,X0) = X1
| max(X0,X1) = X0 ),
inference(resolution,[status(thm)],[f77,f31]) ).
fof(f100,plain,
! [X0,X1] :
( max(X1,X0) = X0
| max(X0,X1) = X1 ),
inference(resolution,[status(thm)],[f92,f32]) ).
fof(f109,plain,
! [X0,X1,X2,X3] :
( ~ model_ub(X2,X3,X0)
| ~ minsol_model_ub(X2,X3,X1)
| X0 = X1
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f21,f59]) ).
fof(f110,plain,
! [X0,X1,X2,X3] :
( ~ model_max(X2,X3,X0)
| ~ minsol_model_max(X2,X3,X1)
| X0 = X1
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f21,f51]) ).
fof(f114,plain,
! [X0,X1,X2] :
( ~ minsol_model_max(X1,X2,X0)
| X0 = max(X1,X2) ),
inference(resolution,[status(thm)],[f40,f50]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ~ minsol_model_ub(X0,X1,X2)
| ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f44,f58]) ).
fof(f116,plain,
! [X0,X1,X2] :
( X2 = X0
| ~ lesseq(X2,X0)
| ~ lesseq(X1,X2)
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f19,f21]) ).
fof(f117,plain,
! [X0,X1,X2] :
( max(X0,X2) = X2
| ~ lesseq(X1,X2)
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f19,f32]) ).
fof(f118,plain,
! [X0,X1,X2] :
( max(X2,X0) = X2
| ~ lesseq(X1,X2)
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f19,f31]) ).
fof(f123,plain,
! [X0,X1,X2,X3] :
( ~ lesseq(X3,sum(X2,X1))
| ~ lesseq(sum(X2,X0),X3)
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f26,f19]) ).
fof(f127,plain,
! [X0,X1,X2] :
( lesseq(sum(X2,X1),sum(X2,X0))
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f26,f22]) ).
fof(f133,plain,
( ~ sQ1_spl
| sK4_skl = max(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f114,f71]) ).
fof(f136,plain,
( ~ sQ1_spl
| model_max(sK2_skl,sK3_skl,sK4_skl) ),
inference(paramodulation,[status(thm)],[f133,f75]) ).
fof(f148,plain,
! [X0] :
( ~ sQ1_spl
| ~ model_max(sK2_skl,sK3_skl,X0)
| X0 = sK4_skl
| ~ lesseq(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f110,f71]) ).
fof(f149,plain,
( ~ sQ1_spl
| sK4_skl = sK4_skl
| ~ lesseq(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f148,f136]) ).
fof(f152,definition,
( sQ2_spl
<=> lesseq(sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( sQ2_spl
| ~ lesseq(sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f152]) ).
fof(f155,definition,
( sQ3_spl
<=> sK4_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f158,plain,
( ~ sQ1_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f149,f152,f155,f70]) ).
fof(f166,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f154,f16]) ).
fof(f167,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f166]) ).
fof(f168,plain,
! [X0] :
( ~ sQ0_spl
| ~ model_ub(sK2_skl,sK3_skl,X0)
| X0 = sK4_skl
| ~ lesseq(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f68,f109]) ).
fof(f170,plain,
( ~ sQ0_spl
| ub(sK2_skl,sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f68,f115]) ).
fof(f172,plain,
( ~ sQ0_spl
| model_ub(sK2_skl,sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f170,f45]) ).
fof(f173,plain,
( ~ sQ0_spl
| lesseq(sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f170,f36]) ).
fof(f174,plain,
( ~ sQ0_spl
| lesseq(sK2_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f170,f35]) ).
fof(f175,plain,
( ~ sQ0_spl
| sK4_skl = sK3_skl
| ~ lesseq(sK4_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f173,f21]) ).
fof(f176,plain,
( ~ sQ0_spl
| max(sK3_skl,sK4_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f173,f32]) ).
fof(f177,plain,
( ~ sQ0_spl
| max(sK4_skl,sK3_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f173,f31]) ).
fof(f178,definition,
( sQ6_spl
<=> lesseq(sK4_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( ~ sQ6_spl
| lesseq(sK4_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f180,plain,
( sQ6_spl
| ~ lesseq(sK4_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f181,definition,
( sQ7_spl
<=> sK4_skl = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( ~ sQ7_spl
| sK4_skl = sK3_skl ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f183,plain,
( sQ7_spl
| sK4_skl != sK3_skl ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f184,plain,
( ~ sQ0_spl
| sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f175,f178,f181,f67]) ).
fof(f185,plain,
( ~ sQ0_spl
| sK4_skl = sK2_skl
| ~ lesseq(sK4_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f174,f21]) ).
fof(f188,definition,
( sQ8_spl
<=> lesseq(sK4_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f189,plain,
( ~ sQ8_spl
| lesseq(sK4_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f190,plain,
( sQ8_spl
| ~ lesseq(sK4_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f191,definition,
( sQ9_spl
<=> sK4_skl = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( ~ sQ9_spl
| sK4_skl = sK2_skl ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f193,plain,
( sQ9_spl
| sK4_skl != sK2_skl ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,plain,
( ~ sQ0_spl
| sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f185,f188,f191,f67]) ).
fof(f195,plain,
! [X0] :
( sQ6_spl
| ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f180,f19]) ).
fof(f202,plain,
! [X0] :
( sQ8_spl
| ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f190,f19]) ).
fof(f207,plain,
! [X0,X1] :
( sQ8_spl
| ~ model_ub(X0,X1,sK2_skl)
| ~ minsol_model_ub(X0,X1,sK4_skl) ),
inference(resolution,[status(thm)],[f190,f59]) ).
fof(f211,plain,
( ~ sQ0_spl
| model_max(sK4_skl,sK3_skl,sK4_skl) ),
inference(paramodulation,[status(thm)],[f177,f75]) ).
fof(f232,plain,
! [X0,X1,X2] :
( model_ub(X0,X2,X1)
| ~ lesseq(X2,X1)
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f37,f45]) ).
fof(f239,plain,
! [X0] :
( sQ6_spl
| lesseq(X0,sK4_skl)
| ~ lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f195,f22]) ).
fof(f245,plain,
! [X0,X1] :
( sQ8_spl
| ~ lesseq(X1,X0)
| ~ lesseq(sK4_skl,X1)
| ~ lesseq(X0,sK2_skl) ),
inference(resolution,[status(thm)],[f202,f19]) ).
fof(f249,plain,
! [X0] :
( sQ8_spl
| lesseq(X0,sK4_skl)
| ~ lesseq(X0,sK2_skl) ),
inference(resolution,[status(thm)],[f202,f22]) ).
fof(f269,plain,
( ~ sQ0_spl
| sK4_skl = sK4_skl
| ~ lesseq(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f168,f172]) ).
fof(f271,plain,
( ~ sQ0_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f269,f152,f155,f67]) ).
fof(f317,plain,
( ~ sQ0_spl
| max(sK3_skl,sK4_skl) = sK4_skl
| sK4_skl = sK3_skl ),
inference(paramodulation,[status(thm)],[f176,f98]) ).
fof(f324,plain,
! [X0,X1] :
( max(X0,X1) = X1
| model_max(X0,X1,X0) ),
inference(paramodulation,[status(thm)],[f98,f75]) ).
fof(f326,definition,
( sQ10_spl
<=> max(sK2_skl,sK4_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f327,plain,
( ~ sQ10_spl
| max(sK2_skl,sK4_skl) = sK4_skl ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f330,definition,
( sQ11_spl
<=> max(sK4_skl,sK2_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( ~ sQ11_spl
| max(sK4_skl,sK2_skl) = sK2_skl ),
inference(component_clause,[status(thm)],[f330]) ).
fof(f332,plain,
( sQ11_spl
| max(sK4_skl,sK2_skl) != sK2_skl ),
inference(component_clause,[status(thm)],[f330]) ).
fof(f338,definition,
( sQ13_spl
<=> max(sK3_skl,sK4_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( ~ sQ13_spl
| max(sK3_skl,sK4_skl) = sK4_skl ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,plain,
( ~ sQ0_spl
| sQ13_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f317,f181,f338,f67]) ).
fof(f357,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| lesseq(sK2_skl,sK3_skl) ),
inference(backward_demodulation,[status(thm)],[f182,f174]) ).
fof(f361,plain,
( sQ1_spl
| ~ sQ7_spl
| ~ minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(backward_demodulation,[status(thm)],[f182,f72]) ).
fof(f404,plain,
! [X0,X1,X2] :
( sK0_skl(X2,X1,X0) = max(X0,X1)
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ),
inference(resolution,[status(thm)],[f52,f40]) ).
fof(f405,plain,
! [X0,X1,X2] :
( ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2)
| ~ lesseq(sK0_skl(X2,X1,X0),sK0_skl(sK0_skl(X2,X1,X0),X1,X0))
| minsol_model_max(X0,X1,sK0_skl(X2,X1,X0)) ),
inference(resolution,[status(thm)],[f53,f52]) ).
fof(f406,plain,
! [X0,X1] :
( ~ lesseq(max(X0,X1),sK0_skl(max(X0,X1),X1,X0))
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f53,f75]) ).
fof(f407,plain,
! [X0] :
( ~ lesseq(X0,sK0_skl(X0,X0,X0))
| minsol_model_max(X0,X0,X0) ),
inference(resolution,[status(thm)],[f53,f90]) ).
fof(f409,plain,
! [X0,X1,X2] :
( ub(X0,X1,sK1_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f60,f44]) ).
fof(f427,definition,
( sQ14_spl
<=> lesseq(sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( sQ14_spl
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f427]) ).
fof(f430,definition,
( sQ15_spl
<=> sK2_skl = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ8_spl
| max(sK2_skl,sK4_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f190,f92]) ).
fof(f453,plain,
( ~ sQ0_spl
| max(sK2_skl,sK4_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f174,f32]) ).
fof(f465,definition,
( sQ16_spl
<=> max(sK4_skl,sK2_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( ~ sQ16_spl
| max(sK4_skl,sK2_skl) = sK4_skl ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f476,plain,
( ~ sQ13_spl
| max(sK4_skl,sK3_skl) = sK4_skl
| sK3_skl = sK4_skl ),
inference(paramodulation,[status(thm)],[f99,f339]) ).
fof(f481,definition,
( sQ17_spl
<=> max(sK4_skl,sK3_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( ~ sQ13_spl
| sQ17_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f476,f181,f481,f338]) ).
fof(f496,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| sK3_skl = sK2_skl
| ~ lesseq(sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f357,f21]) ).
fof(f499,definition,
( sQ18_spl
<=> lesseq(sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f500,plain,
( ~ sQ18_spl
| lesseq(sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f501,plain,
( sQ18_spl
| ~ lesseq(sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,definition,
( sQ19_spl
<=> sK3_skl = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f503,plain,
( ~ sQ19_spl
| sK3_skl = sK2_skl ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f504,plain,
( sQ19_spl
| sK3_skl != sK2_skl ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f505,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f496,f499,f502,f181,f67]) ).
fof(f550,plain,
( sQ6_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f180]) ).
fof(f551,plain,
( sQ6_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f550,f16]) ).
fof(f552,plain,
( sQ6_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f551]) ).
fof(f564,plain,
( sQ8_spl
| max(sK4_skl,sK2_skl) = sK4_skl
| sK2_skl = sK4_skl ),
inference(paramodulation,[status(thm)],[f99,f439]) ).
fof(f565,plain,
( sQ8_spl
| max(sK2_skl,sK4_skl) = sK4_skl
| sK2_skl = sK4_skl ),
inference(paramodulation,[status(thm)],[f98,f439]) ).
fof(f569,plain,
( sQ8_spl
| sQ16_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f564,f191,f465,f188]) ).
fof(f570,plain,
( sQ8_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f565,f191,f326,f188]) ).
fof(f573,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f429,f16]) ).
fof(f574,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f573]) ).
fof(f575,plain,
( sQ7_spl
| ~ sQ19_spl
| sK4_skl != sK2_skl ),
inference(backward_demodulation,[status(thm)],[f503,f183]) ).
fof(f576,plain,
( sQ7_spl
| ~ sQ19_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f575,f191,f502,f181]) ).
fof(f578,plain,
( sQ18_spl
| max(sK2_skl,sK3_skl) = sK3_skl ),
inference(resolution,[status(thm)],[f501,f92]) ).
fof(f581,plain,
( sQ18_spl
| lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f501,f22]) ).
fof(f586,plain,
( sQ0_spl
| ~ sQ9_spl
| ~ minsol_model_ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f69]) ).
fof(f587,plain,
( ~ sQ1_spl
| ~ sQ9_spl
| minsol_model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f71]) ).
fof(f592,plain,
( ~ sQ6_spl
| ~ sQ9_spl
| lesseq(sK2_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f179]) ).
fof(f593,plain,
( ~ sQ6_spl
| ~ sQ9_spl
| sK3_skl = sK2_skl
| ~ lesseq(sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f592,f21]) ).
fof(f596,plain,
( ~ sQ6_spl
| ~ sQ9_spl
| sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f593,f499,f502,f191,f178]) ).
fof(f602,definition,
( sQ20_spl
<=> max(sK2_skl,sK4_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f603,plain,
( ~ sQ20_spl
| max(sK2_skl,sK4_skl) = sK2_skl ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f604,plain,
( sQ20_spl
| max(sK2_skl,sK4_skl) != sK2_skl ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f612,definition,
( sQ21_spl
<=> lesseq(sK2_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f618,plain,
( ~ sQ1_spl
| sK4_skl = max(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f71,f114]) ).
fof(f639,plain,
( ~ sQ1_spl
| max(sK3_skl,sK2_skl) = sK3_skl
| sK4_skl = sK2_skl ),
inference(paramodulation,[status(thm)],[f99,f133]) ).
fof(f644,definition,
( sQ23_spl
<=> max(sK3_skl,sK2_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f645,plain,
( ~ sQ23_spl
| max(sK3_skl,sK2_skl) = sK3_skl ),
inference(component_clause,[status(thm)],[f644]) ).
fof(f647,plain,
( ~ sQ1_spl
| sQ23_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f639,f191,f644,f70]) ).
fof(f648,definition,
( sQ24_spl
<=> max(sK2_skl,sK3_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( ~ sQ24_spl
| max(sK2_skl,sK3_skl) = sK3_skl ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f650,plain,
( sQ24_spl
| max(sK2_skl,sK3_skl) != sK3_skl ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f654,plain,
( sQ18_spl
| ~ sQ1_spl
| sK4_skl = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f133,f578]) ).
fof(f655,plain,
( sQ18_spl
| ~ sQ1_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f654,f183]) ).
fof(f656,plain,
( sQ18_spl
| ~ sQ1_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f655]) ).
fof(f663,plain,
( ~ sQ18_spl
| sK2_skl = sK3_skl
| ~ lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f500,f21]) ).
fof(f666,definition,
( sQ25_spl
<=> lesseq(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f667,plain,
( ~ sQ25_spl
| lesseq(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f666]) ).
fof(f668,plain,
( sQ25_spl
| ~ lesseq(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f666]) ).
fof(f669,plain,
( ~ sQ18_spl
| sQ19_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f663,f666,f502,f499]) ).
fof(f689,plain,
( ~ sQ1_spl
| ~ sQ19_spl
| model_max(sK2_skl,sK2_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f503,f136]) ).
fof(f691,plain,
( ~ sQ1_spl
| ~ sQ19_spl
| sK4_skl = max(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f689,f40]) ).
fof(f699,plain,
( ~ sQ1_spl
| ~ sQ19_spl
| sK4_skl = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f76,f691]) ).
fof(f700,plain,
( ~ sQ1_spl
| ~ sQ19_spl
| sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f699,f193]) ).
fof(f701,plain,
( ~ sQ1_spl
| ~ sQ19_spl
| sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f700]) ).
fof(f704,plain,
( sQ25_spl
| max(sK3_skl,sK2_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f668,f92]) ).
fof(f705,plain,
( sQ25_spl
| max(sK2_skl,sK3_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f668,f77]) ).
fof(f707,plain,
( sQ25_spl
| lesseq(sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f668,f22]) ).
fof(f712,plain,
( ~ sQ18_spl
| max(sK2_skl,sK3_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f500,f31]) ).
fof(f775,plain,
( ~ sQ7_spl
| ~ sQ9_spl
| sK2_skl = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f192,f182]) ).
fof(f782,plain,
( sQ18_spl
| ~ sQ7_spl
| ~ sQ9_spl
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f775,f501]) ).
fof(f783,plain,
( sQ18_spl
| ~ sQ7_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f16]) ).
fof(f784,plain,
( sQ18_spl
| ~ sQ7_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f783]) ).
fof(f787,plain,
( ~ sQ0_spl
| ub(sK2_skl,sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f68,f115]) ).
fof(f793,plain,
( sQ25_spl
| lesseq(sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f668,f22]) ).
fof(f802,plain,
( ~ sQ0_spl
| max(sK4_skl,sK2_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f174,f31]) ).
fof(f806,plain,
( ~ sQ0_spl
| max(sK4_skl,sK3_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f173,f31]) ).
fof(f830,plain,
! [X0,X1,X2,X3] :
( ~ lesseq(X3,X2)
| ~ lesseq(X1,X3)
| X2 = X0
| ~ lesseq(X2,X0)
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f116,f19]) ).
fof(f846,plain,
! [X0] :
( ~ sQ0_spl
| sK3_skl = sK4_skl
| ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f116,f173]) ).
fof(f847,plain,
! [X0] :
( sQ25_spl
| sK3_skl = sK2_skl
| ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f116,f707]) ).
fof(f860,definition,
! [X0] :
( sQ28_spl
<=> ( ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f861,plain,
! [X0] :
( ~ sQ28_spl
| ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f860]) ).
fof(f864,definition,
! [X0] :
( sQ29_spl
<=> ( ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f865,plain,
! [X0] :
( ~ sQ29_spl
| ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f864]) ).
fof(f867,plain,
( ~ sQ0_spl
| sQ7_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f846,f864,f181,f67]) ).
fof(f868,definition,
! [X0] :
( sQ30_spl
<=> ( ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK2_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f869,plain,
! [X0] :
( ~ sQ30_spl
| ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK2_skl,X0) ),
inference(component_clause,[status(thm)],[f868]) ).
fof(f871,plain,
( sQ25_spl
| sQ19_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f847,f868,f502,f666]) ).
fof(f883,definition,
! [X0] :
( sQ31_spl
<=> ( ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f884,plain,
! [X0] :
( ~ sQ31_spl
| ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK3_skl,X0) ),
inference(component_clause,[status(thm)],[f883]) ).
fof(f907,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| minsol_model_ub(sK2_skl,sK2_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f503,f68]) ).
fof(f937,plain,
! [X0] :
( sQ18_spl
| sK2_skl = sK3_skl
| ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f581,f116]) ).
fof(f942,plain,
( sQ18_spl
| sQ19_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f937,f883,f502,f499]) ).
fof(f967,plain,
( ~ sQ11_spl
| max(sK2_skl,sK4_skl) = sK2_skl
| sK4_skl = sK2_skl ),
inference(paramodulation,[status(thm)],[f99,f331]) ).
fof(f972,plain,
( ~ sQ11_spl
| sQ20_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f967,f191,f602,f330]) ).
fof(f1022,plain,
! [X0] :
( ~ sQ0_spl
| ~ model_ub(sK2_skl,sK3_skl,X0)
| max(sK4_skl,X0) = X0 ),
inference(resolution,[status(thm)],[f68,f96]) ).
fof(f1035,plain,
( sQ9_spl
| ~ sQ7_spl
| sK3_skl != sK2_skl ),
inference(backward_demodulation,[status(thm)],[f182,f193]) ).
fof(f1059,definition,
( sQ32_spl
<=> sK3_skl = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1062,definition,
( sQ33_spl
<=> max(sK2_skl,sK3_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1063,plain,
( ~ sQ33_spl
| max(sK2_skl,sK3_skl) = sK2_skl ),
inference(component_clause,[status(thm)],[f1062]) ).
fof(f1066,definition,
( sQ34_spl
<=> max(sK3_skl,sK2_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1067,plain,
( ~ sQ34_spl
| max(sK3_skl,sK2_skl) = sK2_skl ),
inference(component_clause,[status(thm)],[f1066]) ).
fof(f1072,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| max(sK2_skl,sK3_skl) = sK4_skl ),
inference(forward_demodulation,[status(thm)],[f182,f453]) ).
fof(f1073,plain,
( ~ sQ0_spl
| ~ sQ7_spl
| max(sK2_skl,sK3_skl) = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f182,f1072]) ).
fof(f1090,definition,
( sQ35_spl
<=> minsol_model_ub(sK2_skl,sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1091,plain,
( ~ sQ35_spl
| minsol_model_ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f1090]) ).
fof(f1093,definition,
( sQ36_spl
<=> lesseq(sK3_skl,sK1_skl(sK3_skl,sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1113,definition,
( sQ37_spl
<=> minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1114,plain,
( ~ sQ37_spl
| minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f1113]) ).
fof(f1116,definition,
( sQ38_spl
<=> lesseq(sK3_skl,sK0_skl(sK3_skl,sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1118,plain,
( sQ38_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK3_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f1116]) ).
fof(f1120,plain,
( ~ sQ37_spl
| sQ1_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f361]) ).
fof(f1121,plain,
( ~ sQ37_spl
| sQ1_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f1120]) ).
fof(f1143,plain,
! [X0] :
( ~ sQ0_spl
| ~ model_ub(sK2_skl,sK3_skl,X0)
| X0 = sK4_skl
| ~ lesseq(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f68,f109]) ).
fof(f1170,definition,
( sQ39_spl
<=> minsol_model_max(sK4_skl,sK2_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1171,plain,
( ~ sQ39_spl
| minsol_model_max(sK4_skl,sK2_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1170]) ).
fof(f1173,definition,
( sQ40_spl
<=> lesseq(sK4_skl,sK0_skl(sK4_skl,sK2_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1174,plain,
( ~ sQ40_spl
| lesseq(sK4_skl,sK0_skl(sK4_skl,sK2_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f1173]) ).
fof(f1175,plain,
( sQ40_spl
| ~ lesseq(sK4_skl,sK0_skl(sK4_skl,sK2_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f1173]) ).
fof(f1214,plain,
! [X0,X1,X2] :
( lesseq(X2,X1)
| max(X0,X2) = X2
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f117,f22]) ).
fof(f1229,plain,
! [X0,X1,X2] :
( lesseq(X2,X1)
| max(X2,X0) = X2
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f118,f22]) ).
fof(f1271,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| sK4_skl = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f327,f603]) ).
fof(f1272,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1271,f193]) ).
fof(f1273,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f1272]) ).
fof(f1280,definition,
( sQ44_spl
<=> lesseq(sK4_skl,sK0_skl(sK4_skl,sK4_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1282,plain,
( sQ44_spl
| ~ lesseq(sK4_skl,sK0_skl(sK4_skl,sK4_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f1280]) ).
fof(f1314,plain,
! [X0,X1,X2,X3] :
( ~ lesseq(X0,X3)
| ~ lesseq(sum(X2,X3),sum(X2,X1))
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f123,f25]) ).
fof(f1327,definition,
( sQ45_spl
<=> minsol_model_max(sK4_skl,sK3_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1328,plain,
( ~ sQ45_spl
| minsol_model_max(sK4_skl,sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1327]) ).
fof(f1372,plain,
( sQ25_spl
| max(sK3_skl,sK2_skl) = sK2_skl
| sK3_skl = sK2_skl ),
inference(paramodulation,[status(thm)],[f98,f704]) ).
fof(f1375,plain,
( sQ25_spl
| model_max(sK3_skl,sK2_skl,sK2_skl) ),
inference(paramodulation,[status(thm)],[f704,f75]) ).
fof(f1377,plain,
( sQ25_spl
| sQ34_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f1372,f502,f1066,f666]) ).
fof(f1384,plain,
( sQ25_spl
| model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(paramodulation,[status(thm)],[f705,f75]) ).
fof(f1449,plain,
( sQ25_spl
| ~ lesseq(sK2_skl,sK0_skl(sK2_skl,sK2_skl,sK3_skl))
| minsol_model_max(sK3_skl,sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1375,f53]) ).
fof(f1451,definition,
( sQ48_spl
<=> minsol_model_max(sK3_skl,sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1454,definition,
( sQ49_spl
<=> lesseq(sK2_skl,sK0_skl(sK2_skl,sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1457,plain,
( sQ25_spl
| ~ sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1449,f1451,f1454,f666]) ).
fof(f1460,definition,
( sQ50_spl
<=> minsol_model_max(sK2_skl,sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1461,plain,
( ~ sQ50_spl
| minsol_model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f1460]) ).
fof(f1473,plain,
( ~ sQ50_spl
| sK2_skl = max(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f1461,f114]) ).
fof(f1490,plain,
! [X0] :
( sQ8_spl
| lesseq(sK2_skl,X0)
| lesseq(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f249,f22]) ).
fof(f1497,plain,
! [X0] :
( ~ sQ30_spl
| max(sK3_skl,X0) = X0
| ~ lesseq(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f869,f92]) ).
fof(f1503,plain,
( ~ sQ30_spl
| ~ lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f869,f16]) ).
fof(f1506,plain,
( sQ25_spl
| ~ sQ31_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f884,f793]) ).
fof(f1517,plain,
( sQ25_spl
| ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1506,f16]) ).
fof(f1518,plain,
( sQ25_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f1517]) ).
fof(f1519,plain,
( sQ9_spl
| ~ sQ7_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1035,f502,f181,f191]) ).
fof(f1676,plain,
! [X0,X1] :
( max(X1,X0) = X0
| model_max(X0,X1,X1) ),
inference(paramodulation,[status(thm)],[f100,f75]) ).
fof(f1712,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| sQ8_spl
| ~ model_ub(sK2_skl,sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f207,f907]) ).
fof(f1713,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| sQ8_spl
| ~ lesseq(sK2_skl,sK2_skl)
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1712,f232]) ).
fof(f1715,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| sQ8_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1713,f427,f188,f502,f67]) ).
fof(f1726,plain,
( sQ0_spl
| ~ sQ19_spl
| ~ minsol_model_ub(sK2_skl,sK2_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f503,f69]) ).
fof(f1775,plain,
( sQ0_spl
| ~ sQ19_spl
| ~ sQ9_spl
| ~ minsol_model_ub(sK2_skl,sK2_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f1726]) ).
fof(f2079,definition,
( sQ54_spl
<=> minsol_model_ub(sK2_skl,sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2080,plain,
( ~ sQ54_spl
| minsol_model_ub(sK2_skl,sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f2079]) ).
fof(f2082,definition,
( sQ55_spl
<=> lesseq(sK2_skl,sK1_skl(sK2_skl,sK2_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f2161,definition,
( sQ60_spl
<=> model_max(sK2_skl,sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2163,plain,
( sQ60_spl
| ~ model_max(sK2_skl,sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f2161]) ).
fof(f2189,plain,
! [X0] :
( lesseq(sK0_skl(X0,X0,X0),X0)
| minsol_model_max(X0,X0,X0) ),
inference(resolution,[status(thm)],[f407,f22]) ).
fof(f2217,plain,
! [X0,X1,X2] :
( lesseq(X2,X1)
| lesseq(X0,X2)
| max(X0,X1) = X0 ),
inference(resolution,[status(thm)],[f1229,f22]) ).
fof(f2231,plain,
! [X0,X1] :
( sK0_skl(max(X0,X1),X1,X0) = max(X0,X1)
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f404,f75]) ).
fof(f2245,plain,
! [X0,X1,X2] :
( ~ lesseq(X2,sK0_skl(max(X0,X1),X1,X0))
| ~ lesseq(max(X0,X1),X2)
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f406,f19]) ).
fof(f2246,plain,
! [X0,X1] :
( max(sK0_skl(max(X0,X1),X1,X0),max(X0,X1)) = max(X0,X1)
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f406,f92]) ).
fof(f2247,plain,
! [X0,X1] :
( max(max(X0,X1),sK0_skl(max(X0,X1),X1,X0)) = max(X0,X1)
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f406,f77]) ).
fof(f2248,plain,
! [X0,X1] :
( lesseq(sK0_skl(max(X0,X1),X1,X0),max(X0,X1))
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f406,f22]) ).
fof(f2250,plain,
! [X0,X1,X2,X3] :
( ~ model_ub(X2,X3,sK0_skl(max(X0,X1),X1,X0))
| ~ minsol_model_ub(X2,X3,max(X0,X1))
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f406,f59]) ).
fof(f2251,plain,
! [X0,X1,X2,X3] :
( ~ model_max(X2,X3,sK0_skl(max(X0,X1),X1,X0))
| ~ minsol_model_max(X2,X3,max(X0,X1))
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f406,f51]) ).
fof(f2403,plain,
! [X0,X1,X2] :
( lesseq(X1,sK1_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f409,f36]) ).
fof(f2404,plain,
! [X0,X1,X2] :
( lesseq(X0,sK1_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f409,f35]) ).
fof(f2463,definition,
( sQ64_spl
<=> lesseq(max(sK2_skl,sK2_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f2465,plain,
( sQ64_spl
| ~ lesseq(max(sK2_skl,sK2_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f2463]) ).
fof(f3448,plain,
( sQ64_spl
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f76,f2465]) ).
fof(f3449,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3448,f16]) ).
fof(f3450,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f3449]) ).
fof(f3451,plain,
( ~ sQ30_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1503,f666,f868]) ).
fof(f3558,plain,
! [X0] :
( ~ sQ54_spl
| ~ model_ub(sK2_skl,sK2_skl,X0)
| max(sK2_skl,X0) = X0 ),
inference(resolution,[status(thm)],[f2080,f96]) ).
fof(f3581,definition,
( sQ80_spl
<=> minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f3584,definition,
( sQ81_spl
<=> lesseq(max(sK3_skl,sK2_skl),sK0_skl(sK2_skl,sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f3588,definition,
( sQ82_spl
<=> lesseq(sK2_skl,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f3609,plain,
( ~ sQ50_spl
| max(sK3_skl,sK2_skl) = sK2_skl
| sK2_skl = sK3_skl ),
inference(paramodulation,[status(thm)],[f100,f1473]) ).
fof(f3618,plain,
( ~ sQ50_spl
| sQ34_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f3609,f502,f1066,f1460]) ).
fof(f3621,definition,
( sQ83_spl
<=> minsol_model_max(sK2_skl,sK3_skl,max(sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f3622,plain,
( ~ sQ83_spl
| minsol_model_max(sK2_skl,sK3_skl,max(sK2_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f3621]) ).
fof(f3662,definition,
( sQ88_spl
<=> sK0_skl(sK3_skl,sK3_skl,sK2_skl) = max(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f3663,plain,
( ~ sQ88_spl
| sK0_skl(sK3_skl,sK3_skl,sK2_skl) = max(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f3662]) ).
fof(f3698,definition,
( sQ91_spl
<=> minsol_model_max(sK3_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f3699,plain,
( ~ sQ91_spl
| minsol_model_max(sK3_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f3698]) ).
fof(f3700,plain,
( sQ91_spl
| ~ minsol_model_max(sK3_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f3698]) ).
fof(f3701,definition,
( sQ92_spl
<=> sK0_skl(sK3_skl,sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f3702,plain,
( ~ sQ92_spl
| sK0_skl(sK3_skl,sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f3701]) ).
fof(f3705,definition,
( sQ93_spl
<=> lesseq(sK3_skl,sK0_skl(sK3_skl,sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f3707,plain,
( sQ93_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK2_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f3705]) ).
fof(f3721,definition,
( sQ94_spl
<=> lesseq(max(sK3_skl,sK2_skl),sK0_skl(sK3_skl,sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f3725,definition,
( sQ95_spl
<=> lesseq(sK3_skl,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f4031,plain,
( sQ20_spl
| ~ sQ7_spl
| max(sK2_skl,sK3_skl) != sK2_skl ),
inference(forward_demodulation,[status(thm)],[f182,f604]) ).
fof(f4033,plain,
( sQ11_spl
| ~ sQ7_spl
| max(sK3_skl,sK2_skl) != sK2_skl ),
inference(forward_demodulation,[status(thm)],[f182,f332]) ).
fof(f4037,plain,
( ~ sQ16_spl
| ~ sQ7_spl
| max(sK3_skl,sK2_skl) = sK4_skl ),
inference(forward_demodulation,[status(thm)],[f182,f466]) ).
fof(f4193,definition,
( sQ96_spl
<=> lesseq(sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f4195,plain,
( sQ96_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f4193]) ).
fof(f4197,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4195,f16]) ).
fof(f4198,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f4197]) ).
fof(f4241,plain,
! [X0] :
( ~ sQ91_spl
| ~ model_max(sK3_skl,sK2_skl,X0)
| max(sK3_skl,X0) = X0 ),
inference(resolution,[status(thm)],[f3699,f97]) ).
fof(f4242,plain,
( ~ sQ91_spl
| sK3_skl = max(sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f3699,f114]) ).
fof(f4267,definition,
( sQ101_spl
<=> minsol_model_ub(sK2_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f4268,plain,
( ~ sQ101_spl
| minsol_model_ub(sK2_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f4267]) ).
fof(f4284,plain,
( ~ sQ101_spl
| ub(sK2_skl,sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f4268,f115]) ).
fof(f4289,plain,
( ~ sQ101_spl
| lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f4284,f35]) ).
fof(f4295,plain,
! [X0] :
( ~ sQ28_spl
| ~ sQ7_spl
| ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK3_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f182,f861]) ).
fof(f4303,plain,
( ~ sQ28_spl
| ~ sQ7_spl
| max(sK3_skl,sK3_skl) = sK3_skl
| ~ lesseq(sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f4295,f2217]) ).
fof(f4326,definition,
( sQ103_spl
<=> max(sK3_skl,sK3_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f4329,plain,
( ~ sQ28_spl
| ~ sQ7_spl
| sQ103_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f4303,f499,f4326,f181,f860]) ).
fof(f4333,plain,
! [X0] :
( ~ sQ29_spl
| ~ sQ7_spl
| ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK3_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f182,f865]) ).
fof(f4353,plain,
( ~ sQ29_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f4333,f22]) ).
fof(f4368,plain,
( ~ sQ29_spl
| ~ sQ7_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f4353,f4193,f181,f864]) ).
fof(f4372,plain,
! [X0] :
( sQ8_spl
| ~ sQ7_spl
| lesseq(X0,sK3_skl)
| ~ lesseq(X0,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f249]) ).
fof(f4549,plain,
! [X0] :
( sQ8_spl
| ~ sQ7_spl
| lesseq(sK2_skl,X0)
| lesseq(X0,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f1490]) ).
fof(f4597,plain,
( sQ8_spl
| ~ sQ7_spl
| lesseq(sK2_skl,sK3_skl)
| lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f4549,f4372]) ).
fof(f4667,plain,
( sQ8_spl
| ~ sQ7_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f4597,f666,f181,f188]) ).
fof(f4703,plain,
( sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2163,f90]) ).
fof(f4704,plain,
sQ60_spl,
inference(contradiction_clause,[status(thm)],[f4703]) ).
fof(f5072,plain,
( sQ38_spl
| lesseq(sK0_skl(sK3_skl,sK3_skl,sK2_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f1118,f22]) ).
fof(f5076,plain,
( sQ44_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK0_skl(sK4_skl,sK4_skl,sK3_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f1282]) ).
fof(f5077,plain,
( sQ44_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK4_skl,sK3_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f5076]) ).
fof(f5078,plain,
( sQ44_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK3_skl,sK3_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f5077]) ).
fof(f5094,plain,
( sQ44_spl
| ~ sQ7_spl
| lesseq(sK0_skl(sK3_skl,sK3_skl,sK3_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f5078,f22]) ).
fof(f5101,plain,
( sQ40_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK0_skl(sK4_skl,sK2_skl,sK4_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f1175]) ).
fof(f5102,plain,
( sQ40_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK2_skl,sK4_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f5101]) ).
fof(f5103,plain,
( sQ40_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK2_skl,sK3_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f5102]) ).
fof(f5119,plain,
( sQ40_spl
| ~ sQ7_spl
| lesseq(sK0_skl(sK3_skl,sK2_skl,sK3_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f5103,f22]) ).
fof(f5145,definition,
( sQ116_spl
<=> sK0_skl(sK3_skl,sK3_skl,sK3_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f5146,plain,
( ~ sQ116_spl
| sK0_skl(sK3_skl,sK3_skl,sK3_skl) = sK3_skl ),
inference(component_clause,[status(thm)],[f5145]) ).
fof(f5579,plain,
! [X0,X1] :
( sQ38_spl
| ~ lesseq(X1,sK0_skl(sK3_skl,sK3_skl,sK2_skl))
| ~ lesseq(X0,X1)
| sK0_skl(sK3_skl,sK3_skl,sK2_skl) = sK3_skl
| ~ lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f5072,f830]) ).
fof(f5593,plain,
! [X0] :
( sQ38_spl
| sK0_skl(sK3_skl,sK3_skl,sK2_skl) = sK3_skl
| ~ lesseq(X0,sK0_skl(sK3_skl,sK3_skl,sK2_skl))
| ~ lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f5072,f116]) ).
fof(f5604,definition,
( sQ120_spl
<=> sK0_skl(sK3_skl,sK3_skl,sK2_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f5605,plain,
( ~ sQ120_spl
| sK0_skl(sK3_skl,sK3_skl,sK2_skl) = sK3_skl ),
inference(component_clause,[status(thm)],[f5604]) ).
fof(f5606,plain,
( sQ120_spl
| sK0_skl(sK3_skl,sK3_skl,sK2_skl) != sK3_skl ),
inference(component_clause,[status(thm)],[f5604]) ).
fof(f5609,definition,
! [X0,X1] :
( sQ121_spl
<=> ( ~ lesseq(X1,sK0_skl(sK3_skl,sK3_skl,sK2_skl))
| ~ lesseq(X0,X1)
| ~ lesseq(sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f5612,plain,
( sQ38_spl
| sQ120_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f5579,f5609,f5604,f1116]) ).
fof(f5617,definition,
! [X0] :
( sQ123_spl
<=> ( ~ lesseq(X0,sK0_skl(sK3_skl,sK3_skl,sK2_skl))
| ~ lesseq(sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f5620,plain,
( sQ38_spl
| sQ120_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f5593,f5617,f5604,f1116]) ).
fof(f5623,plain,
( sQ38_spl
| ~ sQ120_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(backward_demodulation,[status(thm)],[f5605,f1118]) ).
fof(f5628,plain,
( sQ38_spl
| ~ sQ120_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f5623,f4193,f5604,f1116]) ).
fof(f5632,definition,
( sQ125_spl
<=> model_max(sK2_skl,sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f5633,plain,
( ~ sQ125_spl
| model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f5632]) ).
fof(f5639,definition,
( sQ127_spl
<=> lesseq(sK0_skl(sK3_skl,sK3_skl,sK2_skl),sK0_skl(sK3_skl,sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f5641,plain,
( sQ127_spl
| ~ lesseq(sK0_skl(sK3_skl,sK3_skl,sK2_skl),sK0_skl(sK3_skl,sK3_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f5639]) ).
fof(f5711,plain,
( sQ44_spl
| ~ sQ7_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK3_skl,sK3_skl))
| sK0_skl(sK3_skl,sK3_skl,sK3_skl) = sK3_skl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK3_skl,sK3_skl)) ),
inference(resolution,[status(thm)],[f5094,f830]) ).
fof(f5714,plain,
! [X0,X1] :
( sQ44_spl
| ~ sQ7_spl
| ~ lesseq(X1,sK0_skl(sK3_skl,sK3_skl,sK3_skl))
| ~ lesseq(X0,X1)
| sK0_skl(sK3_skl,sK3_skl,sK3_skl) = sK3_skl
| ~ lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f5094,f830]) ).
fof(f5728,plain,
! [X0] :
( sQ44_spl
| ~ sQ7_spl
| sK0_skl(sK3_skl,sK3_skl,sK3_skl) = sK3_skl
| ~ lesseq(X0,sK0_skl(sK3_skl,sK3_skl,sK3_skl))
| ~ lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f5094,f116]) ).
fof(f5733,definition,
( sQ129_spl
<=> lesseq(sK3_skl,sK0_skl(sK3_skl,sK3_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f5742,plain,
( sQ44_spl
| ~ sQ7_spl
| sQ116_spl
| ~ sQ129_spl ),
inference(split_clause,[status(thm)],[f5711,f5733,f5145,f181,f1280]) ).
fof(f5744,definition,
! [X0,X1] :
( sQ131_spl
<=> ( ~ lesseq(X1,sK0_skl(sK3_skl,sK3_skl,sK3_skl))
| ~ lesseq(X0,X1)
| ~ lesseq(sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f5747,plain,
( sQ44_spl
| ~ sQ7_spl
| sQ116_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f5714,f5744,f5145,f181,f1280]) ).
fof(f5752,definition,
! [X0] :
( sQ133_spl
<=> ( ~ lesseq(X0,sK0_skl(sK3_skl,sK3_skl,sK3_skl))
| ~ lesseq(sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f5755,plain,
( sQ44_spl
| ~ sQ7_spl
| sQ116_spl
| sQ133_spl ),
inference(split_clause,[status(thm)],[f5728,f5752,f5145,f181,f1280]) ).
fof(f5763,plain,
( ~ sQ116_spl
| ~ lesseq(sK3_skl,sK3_skl)
| minsol_model_max(sK3_skl,sK3_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f5146,f407]) ).
fof(f5769,definition,
( sQ135_spl
<=> minsol_model_max(sK3_skl,sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f5770,plain,
( ~ sQ135_spl
| minsol_model_max(sK3_skl,sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f5769]) ).
fof(f5772,definition,
( sQ136_spl
<=> model_max(sK3_skl,sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f5774,plain,
( sQ136_spl
| ~ model_max(sK3_skl,sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f5772]) ).
fof(f5780,definition,
( sQ138_spl
<=> lesseq(sK0_skl(sK3_skl,sK3_skl,sK3_skl),sK0_skl(sK3_skl,sK3_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f5782,plain,
( sQ138_spl
| ~ lesseq(sK0_skl(sK3_skl,sK3_skl,sK3_skl),sK0_skl(sK3_skl,sK3_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f5780]) ).
fof(f5788,plain,
( ~ sQ116_spl
| ~ sQ96_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f5763,f5769,f4193,f5145]) ).
fof(f5790,plain,
( sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5774,f90]) ).
fof(f5791,plain,
sQ136_spl,
inference(contradiction_clause,[status(thm)],[f5790]) ).
fof(f5803,plain,
! [X0] :
( ~ sQ135_spl
| ~ model_max(sK3_skl,sK3_skl,X0)
| max(sK3_skl,X0) = X0 ),
inference(resolution,[status(thm)],[f5770,f97]) ).
fof(f5869,plain,
! [X0,X1] :
( sQ40_spl
| ~ sQ7_spl
| ~ lesseq(X1,sK0_skl(sK3_skl,sK2_skl,sK3_skl))
| ~ lesseq(X0,X1)
| sK0_skl(sK3_skl,sK2_skl,sK3_skl) = sK3_skl
| ~ lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f5119,f830]) ).
fof(f5883,plain,
! [X0] :
( sQ40_spl
| ~ sQ7_spl
| sK0_skl(sK3_skl,sK2_skl,sK3_skl) = sK3_skl
| ~ lesseq(X0,sK0_skl(sK3_skl,sK2_skl,sK3_skl))
| ~ lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f5119,f116]) ).
fof(f5894,definition,
( sQ141_spl
<=> sK0_skl(sK3_skl,sK2_skl,sK3_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f5895,plain,
( ~ sQ141_spl
| sK0_skl(sK3_skl,sK2_skl,sK3_skl) = sK3_skl ),
inference(component_clause,[status(thm)],[f5894]) ).
fof(f5896,plain,
( sQ141_spl
| sK0_skl(sK3_skl,sK2_skl,sK3_skl) != sK3_skl ),
inference(component_clause,[status(thm)],[f5894]) ).
fof(f5899,definition,
! [X0,X1] :
( sQ142_spl
<=> ( ~ lesseq(X1,sK0_skl(sK3_skl,sK2_skl,sK3_skl))
| ~ lesseq(X0,X1)
| ~ lesseq(sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f5902,plain,
( sQ40_spl
| ~ sQ7_spl
| sQ141_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f5869,f5899,f5894,f181,f1173]) ).
fof(f5907,definition,
! [X0] :
( sQ144_spl
<=> ( ~ lesseq(X0,sK0_skl(sK3_skl,sK2_skl,sK3_skl))
| ~ lesseq(sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f5910,plain,
( sQ40_spl
| ~ sQ7_spl
| sQ141_spl
| sQ144_spl ),
inference(split_clause,[status(thm)],[f5883,f5907,f5894,f181,f1173]) ).
fof(f5922,definition,
( sQ146_spl
<=> model_max(sK3_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f5923,plain,
( ~ sQ146_spl
| model_max(sK3_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f5922]) ).
fof(f5929,definition,
( sQ148_spl
<=> lesseq(sK0_skl(sK3_skl,sK2_skl,sK3_skl),sK0_skl(sK3_skl,sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f5931,plain,
( sQ148_spl
| ~ lesseq(sK0_skl(sK3_skl,sK2_skl,sK3_skl),sK0_skl(sK3_skl,sK2_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f5929]) ).
fof(f5951,definition,
! [X0,X1] :
( sQ150_spl
<=> ( ~ model_ub(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_ub(X0,X1,sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f6275,definition,
! [X0,X1] :
( sQ157_spl
<=> ( ~ model_max(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_max(X0,X1,sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f6430,plain,
( ~ sQ91_spl
| max(sK3_skl,sK2_skl) = sK2_skl
| max(sK3_skl,sK3_skl) = sK3_skl ),
inference(resolution,[status(thm)],[f4241,f324]) ).
fof(f6436,plain,
( ~ sQ91_spl
| sQ34_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f6430,f4326,f1066,f3698]) ).
fof(f6500,plain,
( sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5931,f16]) ).
fof(f6501,plain,
sQ148_spl,
inference(contradiction_clause,[status(thm)],[f6500]) ).
fof(f6502,plain,
( sQ138_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5782,f16]) ).
fof(f6503,plain,
sQ138_spl,
inference(contradiction_clause,[status(thm)],[f6502]) ).
fof(f6504,plain,
( sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5641,f16]) ).
fof(f6505,plain,
sQ127_spl,
inference(contradiction_clause,[status(thm)],[f6504]) ).
fof(f6865,definition,
( sQ169_spl
<=> model_max(sK2_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f6866,plain,
( ~ sQ169_spl
| model_max(sK2_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f6865]) ).
fof(f6875,plain,
( ~ sQ169_spl
| sK3_skl = max(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f6866,f40]) ).
fof(f6878,definition,
( sQ170_spl
<=> minsol_model_max(sK2_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f6879,plain,
( ~ sQ170_spl
| minsol_model_max(sK2_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f6878]) ).
fof(f6889,plain,
( ~ sQ169_spl
| sK3_skl = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f76,f6875]) ).
fof(f6890,plain,
( ~ sQ169_spl
| sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6889,f504]) ).
fof(f6891,plain,
( ~ sQ169_spl
| sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f6890]) ).
fof(f6906,plain,
( ~ sQ170_spl
| sK3_skl = max(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f6879,f114]) ).
fof(f6914,plain,
( ~ sQ170_spl
| sK3_skl = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f76,f6906]) ).
fof(f6915,plain,
( ~ sQ170_spl
| sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6914,f504]) ).
fof(f6916,plain,
( ~ sQ170_spl
| sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f6915]) ).
fof(f7053,definition,
( sQ183_spl
<=> model_ub(sK2_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f7054,plain,
( ~ sQ183_spl
| model_ub(sK2_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f7053]) ).
fof(f7516,definition,
( sQ193_spl
<=> lesseq(sK0_skl(sK3_skl,sK2_skl,sK2_skl),sK0_skl(sK3_skl,sK2_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f7518,plain,
( sQ193_spl
| ~ lesseq(sK0_skl(sK3_skl,sK2_skl,sK2_skl),sK0_skl(sK3_skl,sK2_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f7516]) ).
fof(f7525,plain,
( sQ193_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7518,f16]) ).
fof(f7526,plain,
sQ193_spl,
inference(contradiction_clause,[status(thm)],[f7525]) ).
fof(f7669,plain,
! [X0,X1,X2] :
( lesseq(X1,X2)
| ~ lesseq(X0,X2)
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f1314,f127]) ).
fof(f7933,definition,
( sQ205_spl
<=> model_max(sK2_skl,sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f7934,plain,
( ~ sQ205_spl
| model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f7933]) ).
fof(f7953,plain,
( ~ sQ205_spl
| sK2_skl = max(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f7934,f40]) ).
fof(f7959,plain,
( ~ sQ205_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f7953,f1062,f7933]) ).
fof(f7971,definition,
( sQ210_spl
<=> ub(sK2_skl,sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f7972,plain,
( ~ sQ210_spl
| ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f7971]) ).
fof(f7973,plain,
( sQ210_spl
| ~ ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f7971]) ).
fof(f8102,definition,
( sQ226_spl
<=> model_max(sK3_skl,sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f8103,plain,
( ~ sQ226_spl
| model_max(sK3_skl,sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f8102]) ).
fof(f8108,plain,
( ~ sQ40_spl
| ~ sQ7_spl
| lesseq(sK3_skl,sK0_skl(sK4_skl,sK2_skl,sK4_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f1174]) ).
fof(f8109,plain,
( ~ sQ40_spl
| ~ sQ7_spl
| lesseq(sK3_skl,sK0_skl(sK3_skl,sK2_skl,sK4_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f8108]) ).
fof(f8110,plain,
( ~ sQ40_spl
| ~ sQ7_spl
| lesseq(sK3_skl,sK0_skl(sK3_skl,sK2_skl,sK3_skl)) ),
inference(forward_demodulation,[status(thm)],[f182,f8109]) ).
fof(f8123,plain,
( ~ sQ39_spl
| ~ sQ7_spl
| minsol_model_max(sK3_skl,sK2_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f1171]) ).
fof(f8124,plain,
( ~ sQ39_spl
| ~ sQ7_spl
| minsol_model_max(sK3_skl,sK2_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f8123]) ).
fof(f8132,plain,
( ~ sQ39_spl
| ~ sQ7_spl
| sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8124,f3700]) ).
fof(f8133,plain,
( ~ sQ39_spl
| ~ sQ7_spl
| sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f8132]) ).
fof(f8296,definition,
( sQ234_spl
<=> minsol_model_max(sK3_skl,sK2_skl,sK0_skl(sK2_skl,sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f8473,definition,
( sQ245_spl
<=> model_ub(sK2_skl,sK2_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f8474,plain,
( ~ sQ245_spl
| model_ub(sK2_skl,sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f8473]) ).
fof(f8475,plain,
( sQ245_spl
| ~ model_ub(sK2_skl,sK2_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f8473]) ).
fof(f8513,plain,
( sQ245_spl
| ~ lesseq(sK2_skl,sK2_skl)
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f8475,f232]) ).
fof(f8515,plain,
( sQ245_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f8513,f427,f8473]) ).
fof(f8709,plain,
! [X0,X1,X2] :
( lesseq(X2,X0)
| lesseq(X1,X2)
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f7669,f22]) ).
fof(f8756,plain,
( sQ93_spl
| ~ sQ141_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f5895,f3707]) ).
fof(f8757,plain,
( sQ93_spl
| ~ sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8756,f16]) ).
fof(f8758,plain,
( sQ93_spl
| ~ sQ141_spl ),
inference(contradiction_clause,[status(thm)],[f8757]) ).
fof(f9402,definition,
( sQ265_spl
<=> ub(sK2_skl,sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f9403,plain,
( ~ sQ265_spl
| ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f9402]) ).
fof(f9404,plain,
( sQ265_spl
| ~ ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f9402]) ).
fof(f9406,definition,
( sQ266_spl
<=> model_ub(sK2_skl,sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ266_spl])],[split_symbol_definition]) ).
fof(f9407,plain,
( ~ sQ266_spl
| model_ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f9406]) ).
fof(f9408,plain,
( sQ266_spl
| ~ model_ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f9406]) ).
fof(f9418,plain,
( ~ sQ266_spl
| ~ lesseq(sK2_skl,sK1_skl(sK2_skl,sK3_skl,sK2_skl))
| minsol_model_ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f9407,f61]) ).
fof(f9426,definition,
( sQ269_spl
<=> minsol_model_ub(sK2_skl,sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f9439,plain,
( ~ sQ265_spl
| model_ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f9403,f45]) ).
fof(f9442,plain,
( ~ sQ265_spl
| sQ266_spl ),
inference(split_clause,[status(thm)],[f9439,f9406,f9402]) ).
fof(f9469,plain,
( sQ266_spl
| ~ lesseq(sK3_skl,sK2_skl)
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f9408,f232]) ).
fof(f9471,plain,
( sQ266_spl
| ~ sQ18_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f9469,f427,f499,f9406]) ).
fof(f9472,plain,
( sQ265_spl
| ~ lesseq(sK3_skl,sK2_skl)
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f9404,f37]) ).
fof(f9473,plain,
( sQ265_spl
| ~ sQ18_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f9472,f427,f499,f9402]) ).
fof(f9932,plain,
( ~ sQ40_spl
| ~ sQ7_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f8110,f3705,f181,f1173]) ).
fof(f11000,plain,
( ~ sQ135_spl
| max(sK3_skl,sK3_skl) = sK3_skl
| max(sK3_skl,sK3_skl) = sK3_skl ),
inference(resolution,[status(thm)],[f5803,f1676]) ).
fof(f11009,plain,
( ~ sQ135_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f11000,f4326,f5769]) ).
fof(f11013,plain,
( ~ sQ183_spl
| ~ sQ54_spl
| max(sK2_skl,sK3_skl) = sK3_skl ),
inference(resolution,[status(thm)],[f3558,f7054]) ).
fof(f11043,plain,
! [X0,X1] :
( sQ8_spl
| ~ sQ7_spl
| ~ lesseq(X1,X0)
| ~ lesseq(sK3_skl,X1)
| ~ lesseq(X0,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f245]) ).
fof(f11046,plain,
! [X0] :
( sQ8_spl
| ~ sQ7_spl
| lesseq(sK2_skl,sK3_skl)
| ~ lesseq(sK3_skl,X0)
| ~ lesseq(X0,sK2_skl) ),
inference(resolution,[status(thm)],[f11043,f4549]) ).
fof(f11084,plain,
( sQ8_spl
| ~ sQ7_spl
| sQ25_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f11046,f883,f666,f181,f188]) ).
fof(f11298,definition,
! [X0] :
( sQ292_spl
<=> ( ~ lesseq(X0,sK2_skl)
| lesseq(X0,sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ292_spl])],[split_symbol_definition]) ).
fof(f11299,plain,
! [X0] :
( ~ sQ292_spl
| ~ lesseq(X0,sK2_skl)
| lesseq(X0,sK3_skl) ),
inference(component_clause,[status(thm)],[f11298]) ).
fof(f11336,plain,
( ~ sQ88_spl
| ~ sQ0_spl
| ~ sQ7_spl
| sK0_skl(sK3_skl,sK3_skl,sK2_skl) = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f1073,f3663]) ).
fof(f11337,plain,
( ~ sQ88_spl
| ~ sQ0_spl
| ~ sQ7_spl
| sQ120_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11336,f5606]) ).
fof(f11338,plain,
( ~ sQ88_spl
| ~ sQ0_spl
| ~ sQ7_spl
| sQ120_spl ),
inference(contradiction_clause,[status(thm)],[f11337]) ).
fof(f11346,plain,
( ~ sQ101_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f4289,f666,f4267]) ).
fof(f11352,plain,
( sQ25_spl
| sQ226_spl ),
inference(split_clause,[status(thm)],[f1375,f8102,f666]) ).
fof(f11353,plain,
( sQ25_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f1384,f7933,f666]) ).
fof(f11403,plain,
( sQ0_spl
| ~ sQ7_spl
| ~ minsol_model_ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f69]) ).
fof(f11404,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f71]) ).
fof(f11420,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ model_max(sK2_skl,sK3_skl,X0)
| X0 = sK3_skl
| ~ lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f11404,f110]) ).
fof(f11429,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| lesseq(sK3_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f189]) ).
fof(f11451,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| ~ lesseq(sK2_skl,sK3_skl)
| sK3_skl = sK2_skl
| ~ lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f11429,f830]) ).
fof(f11468,plain,
! [X0] :
( ~ sQ8_spl
| ~ sQ7_spl
| sK3_skl = sK2_skl
| ~ lesseq(X0,sK3_skl)
| ~ lesseq(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f11429,f116]) ).
fof(f11472,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| max(sK2_skl,sK3_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f11429,f31]) ).
fof(f11482,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ19_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f11451,f666,f502,f181,f188]) ).
fof(f11484,definition,
! [X0,X1] :
( sQ294_spl
<=> ( ~ lesseq(X1,sK3_skl)
| ~ lesseq(X0,X1)
| ~ lesseq(sK2_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition]) ).
fof(f11493,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ19_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f11468,f868,f502,f181,f188]) ).
fof(f11825,plain,
( sQ20_spl
| ~ sQ7_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f4031,f1062,f181,f602]) ).
fof(f11828,plain,
( sQ11_spl
| ~ sQ7_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f4033,f1066,f181,f330]) ).
fof(f11936,plain,
( ~ sQ25_spl
| max(sK2_skl,sK3_skl) = sK3_skl ),
inference(resolution,[status(thm)],[f667,f32]) ).
fof(f11992,plain,
( sQ18_spl
| max(sK2_skl,sK3_skl) = sK3_skl ),
inference(resolution,[status(thm)],[f501,f92]) ).
fof(f12031,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sK3_skl = max(sK2_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f618]) ).
fof(f12034,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| max(sK2_skl,sK3_skl) = sK3_skl
| sK3_skl = sK2_skl ),
inference(paramodulation,[status(thm)],[f98,f12031]) ).
fof(f12042,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f12031,f75]) ).
fof(f12045,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sQ24_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f12034,f502,f648,f181,f70]) ).
fof(f12184,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ lesseq(X1,sK3_skl)
| ~ lesseq(X0,X1)
| sK3_skl = sK4_skl
| ~ lesseq(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f173,f830]) ).
fof(f12217,definition,
! [X0,X1] :
( sQ299_spl
<=> ( ~ lesseq(X1,sK3_skl)
| ~ lesseq(X0,X1)
| ~ lesseq(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition]) ).
fof(f12220,plain,
( ~ sQ0_spl
| sQ7_spl
| sQ299_spl ),
inference(split_clause,[status(thm)],[f12184,f12217,f181,f67]) ).
fof(f12451,plain,
( ~ sQ210_spl
| model_ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f7972,f45]) ).
fof(f12453,plain,
( ~ sQ210_spl
| lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f7972,f35]) ).
fof(f12505,plain,
( ~ sQ24_spl
| max(sK3_skl,sK2_skl) = sK3_skl
| sK2_skl = sK3_skl ),
inference(paramodulation,[status(thm)],[f99,f649]) ).
fof(f12514,plain,
( ~ sQ24_spl
| model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f649,f75]) ).
fof(f12516,plain,
( ~ sQ24_spl
| sQ23_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f12505,f502,f644,f648]) ).
fof(f12525,plain,
( ~ sQ24_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f12514,f5632,f648]) ).
fof(f12536,plain,
( ~ sQ23_spl
| model_max(sK3_skl,sK2_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f645,f75]) ).
fof(f12547,plain,
( ~ sQ23_spl
| sQ146_spl ),
inference(split_clause,[status(thm)],[f12536,f5922,f644]) ).
fof(f12601,plain,
( ~ sQ35_spl
| ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f1091,f115]) ).
fof(f12625,plain,
( ~ sQ37_spl
| sK3_skl = max(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f1114,f114]) ).
fof(f12883,plain,
( ~ sQ0_spl
| lesseq(sK2_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f787,f35]) ).
fof(f12971,plain,
( ~ sQ0_spl
| sK0_skl(sK4_skl,sK3_skl,sK4_skl) = max(sK4_skl,sK3_skl)
| minsol_model_max(sK4_skl,sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f211,f404]) ).
fof(f12974,definition,
( sQ328_spl
<=> sK0_skl(sK4_skl,sK3_skl,sK4_skl) = max(sK4_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f12975,plain,
( ~ sQ328_spl
| sK0_skl(sK4_skl,sK3_skl,sK4_skl) = max(sK4_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f12974]) ).
fof(f12977,plain,
( ~ sQ0_spl
| sQ328_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f12971,f1327,f12974,f67]) ).
fof(f12995,plain,
( ~ sQ34_spl
| ~ sQ23_spl
| sK3_skl = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f645,f1067]) ).
fof(f12996,plain,
( ~ sQ34_spl
| ~ sQ23_spl
| sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12995,f504]) ).
fof(f12997,plain,
( ~ sQ34_spl
| ~ sQ23_spl
| sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f12996]) ).
fof(f12998,plain,
( sQ18_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f11992,f648,f499]) ).
fof(f12999,plain,
( ~ sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f11936,f648,f666]) ).
fof(f13000,plain,
( ~ sQ183_spl
| ~ sQ54_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f11013,f648,f2079,f7053]) ).
fof(f13009,plain,
( ~ sQ37_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f12625,f648,f1113]) ).
fof(f13031,plain,
( ~ sQ33_spl
| model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(paramodulation,[status(thm)],[f1063,f75]) ).
fof(f13048,plain,
( ~ sQ33_spl
| sQ205_spl ),
inference(split_clause,[status(thm)],[f13031,f7933,f1062]) ).
fof(f13073,plain,
( ~ sQ91_spl
| max(sK2_skl,sK3_skl) = sK3_skl
| sK3_skl = sK2_skl ),
inference(paramodulation,[status(thm)],[f100,f4242]) ).
fof(f13076,plain,
! [X0,X1] :
( ~ sQ91_spl
| ~ model_max(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_max(X0,X1,sK3_skl)
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f4242,f2251]) ).
fof(f13077,plain,
! [X0,X1] :
( ~ sQ91_spl
| ~ model_ub(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_ub(X0,X1,sK3_skl)
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f4242,f2250]) ).
fof(f13078,plain,
( ~ sQ91_spl
| ~ lesseq(max(sK3_skl,sK2_skl),sK0_skl(sK3_skl,sK2_skl,sK3_skl))
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f4242,f406]) ).
fof(f13079,plain,
( ~ sQ91_spl
| ~ lesseq(sK3_skl,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f4242,f406]) ).
fof(f13084,plain,
( ~ sQ91_spl
| sQ24_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f13073,f502,f648,f3698]) ).
fof(f13087,plain,
( ~ sQ91_spl
| sQ157_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13076,f3581,f6275,f3698]) ).
fof(f13088,plain,
( ~ sQ91_spl
| sQ150_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13077,f3581,f5951,f3698]) ).
fof(f13089,plain,
( ~ sQ91_spl
| ~ sQ94_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13078,f3581,f3721,f3698]) ).
fof(f13090,plain,
( ~ sQ91_spl
| ~ sQ95_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13079,f3581,f3725,f3698]) ).
fof(f13287,plain,
( ~ sQ0_spl
| ~ sQ210_spl
| max(sK4_skl,sK3_skl) = sK3_skl ),
inference(resolution,[status(thm)],[f12451,f1022]) ).
fof(f13290,plain,
( ~ sQ210_spl
| ~ lesseq(sK3_skl,sK1_skl(sK3_skl,sK3_skl,sK2_skl))
| minsol_model_ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f12451,f61]) ).
fof(f13293,plain,
( ~ sQ0_spl
| ~ sQ210_spl
| sK4_skl = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f806,f13287]) ).
fof(f13294,plain,
( ~ sQ0_spl
| ~ sQ210_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13293,f183]) ).
fof(f13295,plain,
( ~ sQ0_spl
| ~ sQ210_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f13294]) ).
fof(f13296,plain,
( ~ sQ35_spl
| sQ210_spl ),
inference(split_clause,[status(thm)],[f12601,f7971,f1090]) ).
fof(f13475,plain,
( ~ sQ146_spl
| sK0_skl(sK3_skl,sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f5923,f404]) ).
fof(f13476,plain,
( ~ sQ146_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK2_skl,sK3_skl))
| minsol_model_max(sK3_skl,sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f5923,f53]) ).
fof(f13478,plain,
( ~ sQ146_spl
| sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f13475,f3698,f3701,f5922]) ).
fof(f13479,plain,
( ~ sQ146_spl
| ~ sQ93_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f13476,f3698,f3705,f5922]) ).
fof(f13484,plain,
( ~ sQ125_spl
| sK0_skl(sK3_skl,sK3_skl,sK2_skl) = max(sK2_skl,sK3_skl)
| minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f5633,f404]) ).
fof(f13485,plain,
( ~ sQ125_spl
| ~ lesseq(sK3_skl,sK0_skl(sK3_skl,sK3_skl,sK2_skl))
| minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f5633,f53]) ).
fof(f13487,plain,
( ~ sQ125_spl
| sQ88_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f13484,f1113,f3662,f5632]) ).
fof(f13488,plain,
( ~ sQ125_spl
| ~ sQ38_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f13485,f1113,f1116,f5632]) ).
fof(f13493,plain,
( sQ210_spl
| ~ lesseq(sK3_skl,sK3_skl)
| ~ lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f7973,f37]) ).
fof(f13494,plain,
( sQ210_spl
| ~ sQ96_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f13493,f666,f4193,f7971]) ).
fof(f13502,definition,
( sQ335_spl
<=> lesseq(sK2_skl,sK1_skl(sK2_skl,sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition]) ).
fof(f13505,plain,
( ~ sQ266_spl
| ~ sQ335_spl
| sQ269_spl ),
inference(split_clause,[status(thm)],[f9418,f9426,f13502,f9406]) ).
fof(f13512,plain,
! [X0] :
( ~ sQ18_spl
| lesseq(X0,sK2_skl)
| lesseq(sK3_skl,X0) ),
inference(resolution,[status(thm)],[f500,f7669]) ).
fof(f13533,plain,
! [X0,X1] :
( ~ sQ18_spl
| ~ lesseq(X1,sK3_skl)
| ~ lesseq(X0,X1)
| sK3_skl = sK2_skl
| ~ lesseq(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f500,f830]) ).
fof(f13540,plain,
! [X0] :
( ~ sQ18_spl
| lesseq(X0,sK2_skl)
| max(sK3_skl,X0) = X0 ),
inference(resolution,[status(thm)],[f500,f1214]) ).
fof(f13545,plain,
! [X0] :
( ~ sQ18_spl
| max(sK2_skl,X0) = sK2_skl
| ~ lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f500,f118]) ).
fof(f13546,plain,
! [X0] :
( ~ sQ18_spl
| max(X0,sK2_skl) = sK2_skl
| ~ lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f500,f117]) ).
fof(f13565,plain,
( ~ sQ18_spl
| sQ19_spl
| sQ294_spl ),
inference(split_clause,[status(thm)],[f13533,f11484,f502,f499]) ).
fof(f13900,plain,
( sQ24_spl
| max(sK2_skl,sK3_skl) = sK3_skl
| sK2_skl != sK3_skl ),
inference(paramodulation,[status(thm)],[f98,f650]) ).
fof(f13903,plain,
( sQ24_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f13900,f502,f648]) ).
fof(f13919,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ model_max(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_max(X0,X1,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1067,f2251]) ).
fof(f13920,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ model_ub(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_ub(X0,X1,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1067,f2250]) ).
fof(f13921,plain,
( ~ sQ34_spl
| ~ lesseq(max(sK3_skl,sK2_skl),sK0_skl(sK2_skl,sK2_skl,sK3_skl))
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1067,f406]) ).
fof(f13922,plain,
( ~ sQ34_spl
| ~ lesseq(sK2_skl,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1067,f406]) ).
fof(f13930,definition,
! [X0,X1] :
( sQ336_spl
<=> ( ~ model_max(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_max(X0,X1,sK2_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition]) ).
fof(f13933,plain,
( ~ sQ34_spl
| sQ336_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13919,f3581,f13930,f1066]) ).
fof(f13934,definition,
! [X0,X1] :
( sQ337_spl
<=> ( ~ model_ub(X0,X1,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ minsol_model_ub(X0,X1,sK2_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition]) ).
fof(f13937,plain,
( ~ sQ34_spl
| sQ337_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13920,f3581,f13934,f1066]) ).
fof(f13938,plain,
( ~ sQ34_spl
| ~ sQ81_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13921,f3581,f3584,f1066]) ).
fof(f13939,plain,
( ~ sQ34_spl
| ~ sQ82_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f13922,f3581,f3588,f1066]) ).
fof(f13947,plain,
( ~ sQ18_spl
| max(sK3_skl,sK2_skl) = sK2_skl
| sK3_skl = sK2_skl ),
inference(paramodulation,[status(thm)],[f100,f712]) ).
fof(f13949,plain,
( ~ sQ18_spl
| max(sK2_skl,sK3_skl) = sK3_skl
| sK2_skl = sK2_skl ),
inference(paramodulation,[status(thm)],[f98,f712]) ).
fof(f13958,plain,
( ~ sQ18_spl
| sQ34_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f13947,f502,f1066,f499]) ).
fof(f13960,plain,
( ~ sQ18_spl
| sQ24_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f13949,f430,f648,f499]) ).
fof(f13973,plain,
( ~ sQ0_spl
| ~ sQ266_spl
| max(sK4_skl,sK2_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f9407,f1022]) ).
fof(f13974,plain,
( ~ sQ0_spl
| ~ sQ266_spl
| sK2_skl = sK4_skl
| ~ lesseq(sK2_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f9407,f1143]) ).
fof(f13979,plain,
( ~ sQ0_spl
| ~ sQ266_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f13973,f330,f9406,f67]) ).
fof(f13980,plain,
( ~ sQ0_spl
| ~ sQ266_spl
| sQ9_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f13974,f612,f191,f9406,f67]) ).
fof(f13988,plain,
( ~ sQ0_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f802,f465,f67]) ).
fof(f13992,plain,
( ~ sQ0_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f12883,f612,f67]) ).
fof(f14053,plain,
( sQ1_spl
| ~ sQ9_spl
| ~ minsol_model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f192,f72]) ).
fof(f14096,plain,
( ~ sQ226_spl
| sK0_skl(sK2_skl,sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f8103,f404]) ).
fof(f14099,definition,
( sQ338_spl
<=> sK0_skl(sK2_skl,sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ338_spl])],[split_symbol_definition]) ).
fof(f14100,plain,
( ~ sQ338_spl
| sK0_skl(sK2_skl,sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f14099]) ).
fof(f14102,plain,
( ~ sQ226_spl
| sQ338_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f14096,f1451,f14099,f8102]) ).
fof(f14104,plain,
( ~ sQ338_spl
| ~ sQ34_spl
| sK0_skl(sK2_skl,sK2_skl,sK3_skl) = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f1067,f14100]) ).
fof(f14224,plain,
( ~ sQ245_spl
| ~ lesseq(sK2_skl,sK1_skl(sK2_skl,sK2_skl,sK2_skl))
| minsol_model_ub(sK2_skl,sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f8474,f61]) ).
fof(f14227,plain,
( ~ sQ245_spl
| ~ sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f14224,f2079,f2082,f8473]) ).
fof(f14230,plain,
( sQ0_spl
| ~ sQ7_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f11403,f1090,f181,f67]) ).
fof(f14234,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f11472,f1062,f181,f188]) ).
fof(f14287,plain,
( ~ sQ328_spl
| ~ sQ9_spl
| sK0_skl(sK2_skl,sK3_skl,sK4_skl) = max(sK4_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f12975]) ).
fof(f14288,plain,
( ~ sQ328_spl
| ~ sQ9_spl
| sK0_skl(sK2_skl,sK3_skl,sK2_skl) = max(sK4_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f14287]) ).
fof(f14289,plain,
( ~ sQ328_spl
| ~ sQ9_spl
| sK0_skl(sK2_skl,sK3_skl,sK2_skl) = max(sK2_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f14288]) ).
fof(f14290,plain,
( ~ sQ328_spl
| ~ sQ9_spl
| ~ sQ18_spl
| sK0_skl(sK2_skl,sK3_skl,sK2_skl) = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f712,f14289]) ).
fof(f14331,plain,
( sQ0_spl
| ~ sQ19_spl
| ~ sQ9_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1775,f2079,f191,f502,f67]) ).
fof(f14334,plain,
( sQ0_spl
| ~ sQ9_spl
| ~ sQ269_spl ),
inference(split_clause,[status(thm)],[f586,f9426,f191,f67]) ).
fof(f14383,plain,
( ~ sQ1_spl
| ~ sQ9_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f587,f1460,f191,f70]) ).
fof(f14783,plain,
! [X0] :
( sQ6_spl
| ~ sQ9_spl
| lesseq(X0,sK2_skl)
| ~ lesseq(X0,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f239]) ).
fof(f14885,plain,
( ~ sQ45_spl
| ~ sQ9_spl
| minsol_model_max(sK2_skl,sK3_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f1328]) ).
fof(f14886,plain,
( ~ sQ45_spl
| ~ sQ9_spl
| minsol_model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f192,f14885]) ).
fof(f15065,plain,
( ~ sQ45_spl
| ~ sQ9_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14886,f14053]) ).
fof(f15066,plain,
( ~ sQ45_spl
| ~ sQ9_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f15065]) ).
fof(f15081,plain,
( ~ sQ292_spl
| lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f11299,f8709]) ).
fof(f15116,plain,
( ~ sQ292_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f15081,f666,f11298]) ).
fof(f15199,plain,
( ~ sQ34_spl
| sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,sK2_skl) ),
inference(paramodulation,[status(thm)],[f1067,f2231]) ).
fof(f15226,definition,
( sQ344_spl
<=> sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl) = max(sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition]) ).
fof(f15229,plain,
( ~ sQ34_spl
| sQ344_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f15199,f1451,f15226,f1066]) ).
fof(f15230,definition,
( sQ345_spl
<=> sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl) = max(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition]) ).
fof(f15254,plain,
( ~ sQ18_spl
| minsol_model_max(sK3_skl,sK3_skl,sK3_skl)
| lesseq(sK0_skl(sK3_skl,sK3_skl,sK3_skl),sK2_skl) ),
inference(resolution,[status(thm)],[f13512,f407]) ).
fof(f15371,definition,
( sQ346_spl
<=> lesseq(sK0_skl(sK3_skl,sK3_skl,sK3_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition]) ).
fof(f15374,plain,
( ~ sQ18_spl
| sQ135_spl
| sQ346_spl ),
inference(split_clause,[status(thm)],[f15254,f15371,f5769,f499]) ).
fof(f15447,plain,
( ~ sQ338_spl
| ~ sQ34_spl
| ~ model_max(sK3_skl,sK2_skl,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,sK2_skl)
| ~ lesseq(sK0_skl(sK2_skl,sK2_skl,sK3_skl),sK0_skl(sK2_skl,sK2_skl,sK3_skl))
| minsol_model_max(sK3_skl,sK2_skl,sK0_skl(sK2_skl,sK2_skl,sK3_skl)) ),
inference(paramodulation,[status(thm)],[f14104,f405]) ).
fof(f15458,definition,
( sQ351_spl
<=> lesseq(sK0_skl(sK2_skl,sK2_skl,sK3_skl),sK0_skl(sK2_skl,sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ351_spl])],[split_symbol_definition]) ).
fof(f15460,plain,
( sQ351_spl
| ~ lesseq(sK0_skl(sK2_skl,sK2_skl,sK3_skl),sK0_skl(sK2_skl,sK2_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f15458]) ).
fof(f15461,plain,
( ~ sQ338_spl
| ~ sQ34_spl
| ~ sQ226_spl
| sQ48_spl
| ~ sQ351_spl
| sQ234_spl ),
inference(split_clause,[status(thm)],[f15447,f8296,f15458,f1451,f8102,f1066,f14099]) ).
fof(f15467,plain,
( sQ351_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15460,f16]) ).
fof(f15468,plain,
sQ351_spl,
inference(contradiction_clause,[status(thm)],[f15467]) ).
fof(f15687,plain,
( sQ6_spl
| ~ sQ9_spl
| lesseq(sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f14783,f16]) ).
fof(f16016,plain,
! [X0] :
( ~ sQ34_spl
| ~ lesseq(X0,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ lesseq(sK2_skl,X0)
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1067,f2245]) ).
fof(f16017,plain,
! [X0] :
( ~ sQ18_spl
| ~ lesseq(X0,sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl))
| ~ lesseq(sK2_skl,X0)
| minsol_model_max(sK2_skl,sK3_skl,max(sK2_skl,sK3_skl)) ),
inference(paramodulation,[status(thm)],[f712,f2245]) ).
fof(f16030,definition,
! [X0] :
( sQ365_spl
<=> ( ~ lesseq(X0,sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl))
| ~ lesseq(sK2_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition]) ).
fof(f16033,plain,
( ~ sQ34_spl
| sQ365_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f16016,f3581,f16030,f1066]) ).
fof(f16034,definition,
! [X0] :
( sQ366_spl
<=> ( ~ lesseq(X0,sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl))
| ~ lesseq(sK2_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ366_spl])],[split_symbol_definition]) ).
fof(f16035,plain,
! [X0] :
( ~ sQ366_spl
| ~ lesseq(X0,sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl))
| ~ lesseq(sK2_skl,X0) ),
inference(component_clause,[status(thm)],[f16034]) ).
fof(f16037,plain,
( ~ sQ18_spl
| sQ366_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f16017,f3621,f16034,f499]) ).
fof(f16040,plain,
! [X0] :
( ~ sQ366_spl
| ~ sQ18_spl
| ~ lesseq(X0,sK0_skl(sK2_skl,sK3_skl,sK2_skl))
| ~ lesseq(sK2_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f712,f16035]) ).
fof(f16041,plain,
! [X0] :
( ~ sQ366_spl
| ~ sQ18_spl
| ~ sQ328_spl
| ~ sQ9_spl
| ~ lesseq(X0,sK2_skl)
| ~ lesseq(sK2_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f14290,f16040]) ).
fof(f16067,plain,
( ~ sQ366_spl
| ~ sQ18_spl
| ~ sQ328_spl
| ~ sQ9_spl
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f16041,f8709]) ).
fof(f16102,plain,
( ~ sQ366_spl
| ~ sQ18_spl
| ~ sQ328_spl
| ~ sQ9_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f16067,f427,f191,f12974,f499,f16034]) ).
fof(f16270,plain,
( ~ sQ18_spl
| ~ sQ30_spl
| max(sK3_skl,sK2_skl) = sK2_skl
| max(sK3_skl,sK2_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f1497,f13540]) ).
fof(f16313,plain,
( ~ sQ18_spl
| ~ sQ30_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f16270,f1066,f868,f499]) ).
fof(f16425,plain,
( ~ sQ83_spl
| ~ sQ18_spl
| minsol_model_max(sK2_skl,sK3_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f712,f3622]) ).
fof(f16426,plain,
( ~ sQ83_spl
| ~ sQ18_spl
| sQ1_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16425,f14053]) ).
fof(f16427,plain,
( ~ sQ83_spl
| ~ sQ18_spl
| sQ1_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f16426]) ).
fof(f16447,plain,
( ~ sQ210_spl
| ~ sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f13290,f1090,f1093,f7971]) ).
fof(f16448,plain,
( ~ sQ210_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f12453,f666,f7971]) ).
fof(f16491,plain,
( ~ sQ34_spl
| max(sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl),max(sK3_skl,sK2_skl)) = max(sK3_skl,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,sK2_skl) ),
inference(paramodulation,[status(thm)],[f1067,f2246]) ).
fof(f16513,definition,
( sQ368_spl
<=> max(sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl),max(sK3_skl,sK2_skl)) = max(sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ368_spl])],[split_symbol_definition]) ).
fof(f16516,plain,
( ~ sQ34_spl
| sQ368_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f16491,f1451,f16513,f1066]) ).
fof(f16517,definition,
( sQ369_spl
<=> max(sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl),max(sK2_skl,sK3_skl)) = max(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f16556,plain,
( ~ sQ34_spl
| max(max(sK3_skl,sK2_skl),sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl)) = max(sK3_skl,sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,sK2_skl) ),
inference(paramodulation,[status(thm)],[f1067,f2247]) ).
fof(f16578,definition,
( sQ371_spl
<=> max(max(sK3_skl,sK2_skl),sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl)) = max(sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition]) ).
fof(f16581,plain,
( ~ sQ34_spl
| sQ371_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f16556,f1451,f16578,f1066]) ).
fof(f16582,definition,
( sQ372_spl
<=> max(max(sK2_skl,sK3_skl),sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl)) = max(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition]) ).
fof(f16693,definition,
( sQ373_spl
<=> lesseq(max(sK2_skl,sK3_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition]) ).
fof(f16695,plain,
( sQ373_spl
| ~ lesseq(max(sK2_skl,sK3_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f16693]) ).
fof(f16700,plain,
( sQ373_spl
| ~ sQ18_spl
| ~ lesseq(sK2_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f712,f16695]) ).
fof(f16701,plain,
( sQ373_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16700,f16]) ).
fof(f16702,plain,
( sQ373_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f16701]) ).
fof(f16982,plain,
( ~ sQ18_spl
| minsol_model_max(sK3_skl,sK3_skl,sK3_skl)
| max(sK2_skl,sK0_skl(sK3_skl,sK3_skl,sK3_skl)) = sK2_skl ),
inference(resolution,[status(thm)],[f13545,f2189]) ).
fof(f17024,definition,
( sQ376_spl
<=> max(sK2_skl,sK0_skl(sK3_skl,sK3_skl,sK3_skl)) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition]) ).
fof(f17027,plain,
( ~ sQ18_spl
| sQ135_spl
| sQ376_spl ),
inference(split_clause,[status(thm)],[f16982,f17024,f5769,f499]) ).
fof(f17045,plain,
( ~ sQ18_spl
| minsol_model_max(sK3_skl,sK3_skl,sK3_skl)
| max(sK0_skl(sK3_skl,sK3_skl,sK3_skl),sK2_skl) = sK2_skl ),
inference(resolution,[status(thm)],[f13546,f2189]) ).
fof(f17087,definition,
( sQ377_spl
<=> max(sK0_skl(sK3_skl,sK3_skl,sK3_skl),sK2_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition]) ).
fof(f17090,plain,
( ~ sQ18_spl
| sQ135_spl
| sQ377_spl ),
inference(split_clause,[status(thm)],[f17045,f17087,f5769,f499]) ).
fof(f17161,plain,
( ~ sQ34_spl
| lesseq(sK0_skl(sK2_skl,sK2_skl,sK3_skl),max(sK3_skl,sK2_skl))
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1067,f2248]) ).
fof(f17175,plain,
( ~ sQ34_spl
| lesseq(sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl),sK2_skl)
| minsol_model_max(sK3_skl,sK2_skl,max(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f1067,f2248]) ).
fof(f17191,definition,
( sQ378_spl
<=> lesseq(sK0_skl(sK2_skl,sK2_skl,sK3_skl),max(sK3_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition]) ).
fof(f17194,plain,
( ~ sQ34_spl
| sQ378_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f17161,f3581,f17191,f1066]) ).
fof(f17201,definition,
( sQ380_spl
<=> lesseq(sK0_skl(max(sK3_skl,sK2_skl),sK2_skl,sK3_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition]) ).
fof(f17204,plain,
( ~ sQ34_spl
| sQ380_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f17175,f3581,f17201,f1066]) ).
fof(f17215,plain,
( ~ sQ245_spl
| lesseq(sK2_skl,sK1_skl(sK2_skl,sK2_skl,sK2_skl))
| minsol_model_ub(sK2_skl,sK2_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f2403,f8474]) ).
fof(f17220,plain,
( ~ sQ245_spl
| sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f17215,f2079,f2082,f8473]) ).
fof(f17489,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| max(max(sK2_skl,sK3_skl),sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl)) = max(sK2_skl,sK3_skl)
| minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f12031,f2247]) ).
fof(f17490,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| max(sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl),max(sK2_skl,sK3_skl)) = max(sK2_skl,sK3_skl)
| minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f12031,f2246]) ).
fof(f17492,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sK0_skl(max(sK2_skl,sK3_skl),sK3_skl,sK2_skl) = max(sK2_skl,sK3_skl)
| minsol_model_max(sK2_skl,sK3_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f12031,f2231]) ).
fof(f17512,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sQ372_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f17489,f1113,f16582,f181,f70]) ).
fof(f17513,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sQ369_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f17490,f1113,f16517,f181,f70]) ).
fof(f17518,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sQ345_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f17492,f1113,f15230,f181,f70]) ).
fof(f17559,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sK3_skl = sK3_skl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f12042,f11420]) ).
fof(f17568,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| sQ32_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f17559,f4193,f1059,f181,f70]) ).
fof(f17609,plain,
( ~ sQ16_spl
| ~ sQ7_spl
| sQ18_spl
| ~ sQ1_spl
| max(sK3_skl,sK2_skl) = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f654,f4037]) ).
fof(f17688,plain,
( ~ sQ92_spl
| ~ sQ16_spl
| ~ sQ7_spl
| sQ18_spl
| ~ sQ1_spl
| sK0_skl(sK3_skl,sK2_skl,sK3_skl) = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f17609,f3702]) ).
fof(f17689,plain,
( ~ sQ92_spl
| ~ sQ16_spl
| ~ sQ7_spl
| sQ18_spl
| ~ sQ1_spl
| sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17688,f5896]) ).
fof(f17690,plain,
( ~ sQ92_spl
| ~ sQ16_spl
| ~ sQ7_spl
| sQ18_spl
| ~ sQ1_spl
| sQ141_spl ),
inference(contradiction_clause,[status(thm)],[f17689]) ).
fof(f19384,plain,
( ~ sQ210_spl
| lesseq(sK3_skl,sK1_skl(sK3_skl,sK3_skl,sK2_skl))
| minsol_model_ub(sK2_skl,sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f12451,f2403]) ).
fof(f19399,plain,
( ~ sQ210_spl
| sQ36_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f19384,f1090,f1093,f7971]) ).
fof(f19487,plain,
( sQ6_spl
| ~ sQ9_spl
| ~ lesseq(sK2_skl,sK3_skl)
| sK3_skl = sK2_skl
| ~ lesseq(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f15687,f830]) ).
fof(f19512,plain,
( sQ6_spl
| ~ sQ9_spl
| sQ19_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f19487,f666,f502,f191,f178]) ).
fof(f19821,plain,
( ~ sQ266_spl
| lesseq(sK2_skl,sK1_skl(sK2_skl,sK3_skl,sK2_skl))
| minsol_model_ub(sK2_skl,sK3_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f9407,f2404]) ).
fof(f19833,plain,
( ~ sQ266_spl
| sQ335_spl
| sQ269_spl ),
inference(split_clause,[status(thm)],[f19821,f9426,f13502,f9406]) ).
fof(f19837,plain,
$false,
inference(sat_refutation,[status(thm)],[f73,f74,f158,f167,f184,f194,f271,f341,f484,f505,f552,f569,f570,f574,f576,f596,f647,f656,f669,f701,f784,f867,f871,f942,f972,f1121,f1273,f1377,f1457,f1518,f1519,f1715,f3450,f3451,f3618,f4198,f4329,f4368,f4667,f4704,f5612,f5620,f5628,f5742,f5747,f5755,f5788,f5791,f5902,f5910,f6436,f6501,f6503,f6505,f6891,f6916,f7526,f7959,f8133,f8515,f8758,f9442,f9471,f9473,f9932,f11009,f11084,f11338,f11346,f11352,f11353,f11482,f11493,f11825,f11828,f12045,f12220,f12516,f12525,f12547,f12977,f12997,f12998,f12999,f13000,f13009,f13048,f13084,f13087,f13088,f13089,f13090,f13295,f13296,f13478,f13479,f13487,f13488,f13494,f13505,f13565,f13903,f13933,f13937,f13938,f13939,f13958,f13960,f13979,f13980,f13988,f13992,f14102,f14227,f14230,f14234,f14331,f14334,f14383,f15066,f15116,f15229,f15374,f15461,f15468,f16033,f16037,f16102,f16313,f16427,f16447,f16448,f16516,f16581,f16702,f17027,f17090,f17194,f17204,f17220,f17512,f17513,f17518,f17568,f17690,f19399,f19512,f19833]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM858+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 03:15:16 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 59.89/8.01 % Refutation found
% 59.89/8.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 59.89/8.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.16/8.41 % Elapsed time: 8.044361 seconds
% 4.16/8.41 % CPU time: 61.019380 seconds
% 4.16/8.41 % Total memory used: 259.224 MB
% 4.16/8.41 % Net memory used: 207.594 MB
%------------------------------------------------------------------------------