%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM859+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 36.45s 6.32s
% Output : CNFRefutation 36.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 33
% Syntax : Number of formulae : 226 ( 7 unt; 21 def)
% Number of atoms : 684 ( 30 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 790 ( 332 ~; 383 |; 40 &)
% ( 30 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 22 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 320 ( 307 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : lesseq(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( lesseq(Y,Z)
& lesseq(X,Y) )
=> lesseq(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( ( lesseq(Y,X)
& lesseq(X,Y) )
=> X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( lesseq(Y,X)
| lesseq(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] :
( ~ lesseq(Y,X)
| max(X,Y) = X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] :
( ~ lesseq(X,Y)
| max(X,Y) = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,Z] :
( ub(X,Y,Z)
<=> ( lesseq(Y,Z)
& lesseq(X,Z) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y,N] :
( model_max(X,Y,N)
<=> lesseq(max(X,Y),N) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y,N] :
( model_ub(X,Y,N)
<=> ? [Z] :
( lesseq(Z,N)
& ub(X,Y,Z) ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,conjecture,
! [X,Y,Z] :
( minsol_model_ub(X,Y,Z)
<=> minsol_model_max(X,Y,Z) ),
file('/export/starexec/sandbox2/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(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] :
( ( ~ lesseq(max(X,Y),N)
| model_max(X,Y,N) )
& ( lesseq(max(X,Y),N)
| ~ model_max(X,Y,N) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f39,plain,
( ! [X,Y,N] :
( ~ lesseq(max(X,Y),N)
| model_max(X,Y,N) )
& ! [X,Y,N] :
( lesseq(max(X,Y),N)
| ~ model_max(X,Y,N) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0,X1,X2] :
( lesseq(max(X0,X1),X2)
| ~ model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [X0,X1,X2] :
( ~ lesseq(max(X0,X1),X2)
| model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f42,plain,
! [X,Y,N] :
( ( ! [Z] :
( ~ lesseq(Z,N)
| ~ ub(X,Y,Z) )
| model_ub(X,Y,N) )
& ( ? [Z] :
( lesseq(Z,N)
& ub(X,Y,Z) )
| ~ model_ub(X,Y,N) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f43,plain,
( ! [X,Y,N] :
( ! [Z] :
( ~ lesseq(Z,N)
| ~ ub(X,Y,Z) )
| model_ub(X,Y,N) )
& ! [X,Y,N] :
( ? [Z] :
( lesseq(Z,N)
& ub(X,Y,Z) )
| ~ model_ub(X,Y,N) ) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f44,plain,
( ! [X,Y,N] :
( ! [Z] :
( ~ lesseq(Z,N)
| ~ ub(X,Y,Z) )
| model_ub(X,Y,N) )
& ! [X,Y,N] :
( ( lesseq(sK0_skl(N,Y,X),N)
& ub(X,Y,sK0_skl(N,Y,X)) )
| ~ model_ub(X,Y,N) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Z,sK0_skl(N,Y,X))],[f43]) ).
fof(f45,plain,
! [X0,X1,X2] :
( ub(X0,X1,sK0_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( lesseq(sK0_skl(X2,X1,X0),X2)
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f47,plain,
! [X0,X1,X2,X3] :
( ~ lesseq(X3,X2)
| ~ ub(X0,X1,X3)
| model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f48,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(f49,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)],[f48]) ).
fof(f50,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)],[f49]) ).
fof(f51,plain,
( ! [X,Y,N] :
( ( ~ lesseq(N,sK1_skl(N,Y,X))
& model_max(X,Y,sK1_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,[sK1_skl]),skolemize(Z,sK1_skl(N,Y,X))],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( model_max(X0,X1,X2)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,plain,
! [X0,X1,X2,X3] :
( lesseq(X2,X3)
| ~ model_max(X0,X1,X3)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f54,plain,
! [X0,X1,X2] :
( model_max(X0,X1,sK1_skl(X2,X1,X0))
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ~ lesseq(X2,sK1_skl(X2,X1,X0))
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f56,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(f57,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)],[f56]) ).
fof(f58,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)],[f57]) ).
fof(f59,plain,
( ! [X,Y,N] :
( ( ~ lesseq(N,sK2_skl(N,Y,X))
& model_ub(X,Y,sK2_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,[sK2_skl]),skolemize(Z,sK2_skl(N,Y,X))],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( model_ub(X0,X1,X2)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [X0,X1,X2,X3] :
( lesseq(X2,X3)
| ~ model_ub(X0,X1,X3)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f62,plain,
! [X0,X1,X2] :
( model_ub(X0,X1,sK2_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ lesseq(X2,sK2_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f64,plain,
? [X,Y,Z] :
( minsol_model_ub(X,Y,Z)
<~> minsol_model_max(X,Y,Z) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f65,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)],[f64]) ).
fof(f66,plain,
( ( ~ minsol_model_max(sK3_skl,sK4_skl,sK5_skl)
| ~ minsol_model_ub(sK3_skl,sK4_skl,sK5_skl) )
& ( minsol_model_max(sK3_skl,sK4_skl,sK5_skl)
| minsol_model_ub(sK3_skl,sK4_skl,sK5_skl) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(X,sK3_skl),skolemize(Y,sK4_skl),skolemize(Z,sK5_skl)],[f65]) ).
fof(f67,plain,
( minsol_model_max(sK3_skl,sK4_skl,sK5_skl)
| minsol_model_ub(sK3_skl,sK4_skl,sK5_skl) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
( ~ minsol_model_max(sK3_skl,sK4_skl,sK5_skl)
| ~ minsol_model_ub(sK3_skl,sK4_skl,sK5_skl) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f69,definition,
( sQ0_spl
<=> minsol_model_ub(sK3_skl,sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f70,plain,
( ~ sQ0_spl
| minsol_model_ub(sK3_skl,sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f69]) ).
fof(f71,plain,
( sQ0_spl
| ~ minsol_model_ub(sK3_skl,sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f69]) ).
fof(f72,definition,
( sQ1_spl
<=> minsol_model_max(sK3_skl,sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f73,plain,
( ~ sQ1_spl
| minsol_model_max(sK3_skl,sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f72]) ).
fof(f74,plain,
( sQ1_spl
| ~ minsol_model_max(sK3_skl,sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f72]) ).
fof(f75,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f67,f69,f72]) ).
fof(f76,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f68,f69,f72]) ).
fof(f77,plain,
( ~ sQ1_spl
| model_max(sK3_skl,sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f52,f73]) ).
fof(f78,plain,
! [X0] :
( ~ sQ1_spl
| lesseq(sK5_skl,X0)
| ~ model_max(sK3_skl,sK4_skl,X0) ),
inference(resolution,[status(thm)],[f53,f73]) ).
fof(f82,plain,
! [X0,X1,X2] :
( lesseq(X2,X1)
| lesseq(X0,X2)
| ~ lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f19,f22]) ).
fof(f97,plain,
! [X0,X1,X2] :
( lesseq(X2,max(X0,X1))
| model_max(X0,X1,X2) ),
inference(resolution,[status(thm)],[f41,f22]) ).
fof(f98,plain,
! [X0,X1] : model_max(X0,X1,max(X0,X1)),
inference(resolution,[status(thm)],[f41,f16]) ).
fof(f99,plain,
( ~ sQ1_spl
| lesseq(sK5_skl,max(sK3_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f98,f78]) ).
fof(f101,plain,
( ~ sQ1_spl
| max(sK3_skl,sK4_skl) = sK5_skl
| ~ lesseq(max(sK3_skl,sK4_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f99,f21]) ).
fof(f102,definition,
( sQ2_spl
<=> lesseq(max(sK3_skl,sK4_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f104,plain,
( sQ2_spl
| ~ lesseq(max(sK3_skl,sK4_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f102]) ).
fof(f105,definition,
( sQ3_spl
<=> max(sK3_skl,sK4_skl) = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f106,plain,
( ~ sQ3_spl
| max(sK3_skl,sK4_skl) = sK5_skl ),
inference(component_clause,[status(thm)],[f105]) ).
fof(f107,plain,
( sQ3_spl
| max(sK3_skl,sK4_skl) != sK5_skl ),
inference(component_clause,[status(thm)],[f105]) ).
fof(f108,plain,
( ~ sQ1_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f101,f102,f105,f72]) ).
fof(f109,plain,
( sQ2_spl
| ~ model_max(sK3_skl,sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f104,f40]) ).
fof(f111,plain,
( sQ2_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f109,f77]) ).
fof(f112,plain,
( sQ2_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f111]) ).
fof(f114,plain,
( ~ sQ0_spl
| model_ub(sK3_skl,sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f70,f60]) ).
fof(f118,plain,
! [X0,X1,X2] :
( lesseq(X2,X0)
| lesseq(X1,X2)
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f82,f22]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( model_max(X2,X3,max(X0,X1))
| model_max(X0,X1,max(X2,X3)) ),
inference(resolution,[status(thm)],[f97,f41]) ).
fof(f136,plain,
! [X0,X1,X2,X3] :
( lesseq(X3,X2)
| lesseq(X1,X3)
| lesseq(X2,X0)
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f118,f82]) ).
fof(f138,plain,
! [X0,X1,X2,X3] :
( lesseq(X3,X2)
| ~ lesseq(X3,X1)
| lesseq(X2,X0)
| lesseq(X0,X1) ),
inference(resolution,[status(thm)],[f118,f19]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( lesseq(X3,X2)
| ~ lesseq(X3,sK0_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f46,f19]) ).
fof(f154,plain,
! [X0,X1,X2] :
( lesseq(X1,sK0_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f45,f36]) ).
fof(f155,plain,
! [X0,X1,X2] :
( lesseq(X0,sK0_skl(X2,X1,X0))
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f45,f35]) ).
fof(f165,plain,
! [X0,X1,X2,X3] :
( ~ lesseq(X1,X3)
| ~ lesseq(X0,X3)
| ~ lesseq(X3,X2)
| model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f47,f37]) ).
fof(f166,plain,
! [X0,X1,X2,X3] :
( ~ model_max(X2,X3,sK1_skl(max(X2,X3),X1,X0))
| ~ model_max(X0,X1,max(X2,X3))
| minsol_model_max(X0,X1,max(X2,X3)) ),
inference(resolution,[status(thm)],[f55,f40]) ).
fof(f466,plain,
! [X0,X1] :
( ~ sQ3_spl
| model_max(X0,X1,sK5_skl)
| model_max(sK3_skl,sK4_skl,max(X0,X1)) ),
inference(paramodulation,[status(thm)],[f106,f124]) ).
fof(f473,plain,
( ~ sQ3_spl
| ~ lesseq(sK3_skl,sK4_skl)
| sK5_skl = sK4_skl ),
inference(paramodulation,[status(thm)],[f106,f32]) ).
fof(f474,plain,
( ~ sQ3_spl
| ~ lesseq(sK4_skl,sK3_skl)
| sK5_skl = sK3_skl ),
inference(paramodulation,[status(thm)],[f106,f31]) ).
fof(f475,definition,
( sQ5_spl
<=> sK5_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f476,plain,
( ~ sQ5_spl
| sK5_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
( sQ6_spl
<=> lesseq(sK3_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f480,plain,
( sQ6_spl
| ~ lesseq(sK3_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( ~ sQ3_spl
| ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f473,f475,f478,f105]) ).
fof(f482,definition,
( sQ7_spl
<=> sK5_skl = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f483,plain,
( ~ sQ7_spl
| sK5_skl = sK3_skl ),
inference(component_clause,[status(thm)],[f482]) ).
fof(f485,definition,
( sQ8_spl
<=> lesseq(sK4_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( ~ sQ8_spl
| lesseq(sK4_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f485]) ).
fof(f488,plain,
( ~ sQ3_spl
| ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f474,f482,f485,f105]) ).
fof(f489,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| max(sK3_skl,sK4_skl) = sK4_skl ),
inference(backward_demodulation,[status(thm)],[f476,f106]) ).
fof(f518,definition,
( sQ10_spl
<=> lesseq(sK3_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f520,plain,
( sQ10_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f523,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f520,f16]) ).
fof(f524,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f523]) ).
fof(f526,plain,
( sQ6_spl
| lesseq(sK4_skl,sK3_skl)
| lesseq(sK4_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f480,f136]) ).
fof(f533,plain,
( sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f526,f485,f478]) ).
fof(f535,plain,
! [X0,X1] :
( ~ sQ8_spl
| lesseq(sK4_skl,X1)
| lesseq(X1,X0)
| lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f486,f138]) ).
fof(f536,plain,
! [X0] :
( ~ sQ8_spl
| lesseq(X0,sK3_skl)
| lesseq(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f486,f82]) ).
fof(f538,plain,
( ~ sQ8_spl
| sK3_skl = sK4_skl
| ~ lesseq(sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f486,f21]) ).
fof(f539,definition,
( sQ11_spl
<=> sK3_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f540,plain,
( ~ sQ11_spl
| sK3_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,plain,
( ~ sQ8_spl
| sQ11_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f538,f478,f539,f485]) ).
fof(f560,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| lesseq(sK4_skl,X2)
| lesseq(X2,X1)
| lesseq(X1,X0)
| lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f536,f138]) ).
fof(f562,plain,
! [X0,X1] :
( ~ sQ8_spl
| lesseq(X1,X0)
| ~ lesseq(X1,sK4_skl)
| lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f536,f19]) ).
fof(f583,definition,
( sQ12_spl
<=> lesseq(sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( sQ12_spl
| ~ lesseq(sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f583]) ).
fof(f601,plain,
! [X0,X1,X2] :
( ~ sQ8_spl
| lesseq(X2,X1)
| ~ lesseq(X2,sK4_skl)
| lesseq(X1,X0)
| lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f535,f19]) ).
fof(f603,definition,
! [X0] :
( sQ13_spl
<=> ( lesseq(sK4_skl,X0)
| lesseq(X0,sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f607,plain,
! [X0,X1] :
( ~ sQ8_spl
| lesseq(sK4_skl,X1)
| lesseq(X1,sK3_skl)
| lesseq(sK4_skl,X0)
| lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f562,f535]) ).
fof(f626,plain,
( ~ sQ8_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f607,f603,f485]) ).
fof(f836,plain,
! [X0,X1,X2] :
( ~ model_ub(X0,X1,X2)
| lesseq(X0,X2)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f152,f155]) ).
fof(f837,plain,
! [X0,X1,X2] :
( ~ model_ub(X0,X1,X2)
| lesseq(X1,X2)
| ~ model_ub(X0,X1,X2) ),
inference(resolution,[status(thm)],[f152,f154]) ).
fof(f850,plain,
! [X0,X1,X2] :
( lesseq(X0,X2)
| ~ model_ub(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f836]) ).
fof(f851,plain,
! [X0,X1,X2] :
( lesseq(X1,X2)
| ~ model_ub(X0,X1,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f837]) ).
fof(f920,definition,
! [X0,X1] :
( sQ14_spl
<=> ( lesseq(sK4_skl,X1)
| lesseq(X1,X0)
| lesseq(X0,sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f925,plain,
! [X0,X1,X2,X3] :
( ~ sQ8_spl
| lesseq(sK4_skl,X3)
| lesseq(X3,X2)
| lesseq(X2,sK3_skl)
| lesseq(sK4_skl,X1)
| lesseq(X1,X0)
| lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f601,f560]) ).
fof(f945,plain,
( ~ sQ8_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f925,f920,f485]) ).
fof(f988,plain,
( ~ sQ0_spl
| lesseq(sK3_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f850,f114]) ).
fof(f989,plain,
! [X0,X1,X2] :
( ~ model_ub(X0,X2,X1)
| minsol_model_ub(X0,X2,X1)
| lesseq(X0,sK2_skl(X1,X2,X0)) ),
inference(resolution,[status(thm)],[f850,f62]) ).
fof(f993,plain,
( ~ sQ0_spl
| sK5_skl = sK3_skl
| ~ lesseq(sK5_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f988,f21]) ).
fof(f994,definition,
( sQ15_spl
<=> lesseq(sK5_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f997,plain,
( ~ sQ0_spl
| sQ7_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f993,f994,f482,f69]) ).
fof(f1020,plain,
( sQ3_spl
| ~ sQ7_spl
| max(sK3_skl,sK4_skl) != sK3_skl ),
inference(backward_demodulation,[status(thm)],[f483,f107]) ).
fof(f1025,plain,
( sQ3_spl
| ~ sQ7_spl
| ~ lesseq(sK4_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f1020,f31]) ).
fof(f1026,plain,
( sQ3_spl
| ~ sQ7_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1025,f485,f482,f105]) ).
fof(f1131,definition,
( sQ18_spl
<=> lesseq(sK5_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1133,plain,
( sQ18_spl
| ~ lesseq(sK5_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1131]) ).
fof(f1151,plain,
! [X0,X1,X2] :
( ~ model_ub(X2,X0,X1)
| minsol_model_ub(X2,X0,X1)
| lesseq(X0,sK2_skl(X1,X0,X2)) ),
inference(resolution,[status(thm)],[f851,f62]) ).
fof(f1262,plain,
( ~ sQ0_spl
| lesseq(sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f114,f851]) ).
fof(f1267,plain,
( ~ sQ0_spl
| sK5_skl = sK4_skl
| ~ lesseq(sK5_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f1262,f21]) ).
fof(f1268,plain,
( ~ sQ0_spl
| sQ5_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1267,f1131,f475,f69]) ).
fof(f1269,plain,
! [X0] :
( ~ sQ0_spl
| lesseq(sK5_skl,X0)
| ~ model_ub(sK3_skl,sK4_skl,X0) ),
inference(resolution,[status(thm)],[f70,f61]) ).
fof(f1274,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| model_ub(sK3_skl,sK4_skl,sK4_skl) ),
inference(backward_demodulation,[status(thm)],[f476,f114]) ).
fof(f1281,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| lesseq(sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f1274,f850]) ).
fof(f1322,plain,
! [X0,X1] :
( ~ model_max(X0,X1,max(X0,X1))
| minsol_model_max(X0,X1,max(X0,X1))
| ~ model_max(X0,X1,max(X0,X1))
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(resolution,[status(thm)],[f166,f54]) ).
fof(f1323,plain,
! [X0,X1] :
( ~ model_max(X0,X1,max(X0,X1))
| minsol_model_max(X0,X1,max(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f1322]) ).
fof(f1324,plain,
! [X0,X1] : minsol_model_max(X0,X1,max(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f1323,f98]) ).
fof(f1359,definition,
( sQ19_spl
<=> minsol_model_ub(sK3_skl,sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1360,plain,
( ~ sQ19_spl
| minsol_model_ub(sK3_skl,sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1359]) ).
fof(f1361,plain,
( sQ19_spl
| ~ minsol_model_ub(sK3_skl,sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1359]) ).
fof(f1362,definition,
( sQ20_spl
<=> model_ub(sK3_skl,sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1364,plain,
( sQ20_spl
| ~ model_ub(sK3_skl,sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1362]) ).
fof(f1615,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ lesseq(sK4_skl,X1)
| ~ lesseq(sK3_skl,X1)
| ~ lesseq(X1,X0)
| lesseq(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1269,f165]) ).
fof(f1825,plain,
( sQ20_spl
| ~ sQ11_spl
| ~ model_ub(sK3_skl,sK4_skl,sK3_skl) ),
inference(backward_demodulation,[status(thm)],[f540,f1364]) ).
fof(f1832,plain,
( sQ20_spl
| ~ sQ11_spl
| ~ model_ub(sK3_skl,sK3_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f540,f1825]) ).
fof(f1838,plain,
! [X0] :
( sQ20_spl
| ~ sQ11_spl
| ~ lesseq(sK3_skl,X0)
| ~ lesseq(sK3_skl,X0)
| ~ lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f1832,f165]) ).
fof(f1839,plain,
! [X0] :
( sQ20_spl
| ~ sQ11_spl
| ~ lesseq(sK3_skl,X0)
| ~ lesseq(X0,sK3_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1838]) ).
fof(f1859,plain,
( sQ20_spl
| ~ sQ11_spl
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f1839,f16]) ).
fof(f1865,plain,
( sQ20_spl
| ~ sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1859,f518,f539,f1362]) ).
fof(f1900,plain,
( ~ sQ19_spl
| model_ub(sK3_skl,sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f1360,f60]) ).
fof(f1908,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| lesseq(sK5_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f1900,f1269]) ).
fof(f1910,plain,
( ~ sQ19_spl
| lesseq(sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f1900,f850]) ).
fof(f1911,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1908,f1133]) ).
fof(f1912,plain,
( ~ sQ0_spl
| ~ sQ19_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f1911]) ).
fof(f1913,plain,
( ~ sQ19_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1910,f478,f1359]) ).
fof(f1914,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1281,f478,f475,f69]) ).
fof(f2091,plain,
! [X0] :
( ~ sQ0_spl
| ~ lesseq(sK4_skl,sK3_skl)
| ~ lesseq(sK3_skl,X0)
| lesseq(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1615,f16]) ).
fof(f2119,definition,
! [X0] :
( sQ25_spl
<=> ( ~ lesseq(sK3_skl,X0)
| lesseq(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f2120,plain,
! [X0] :
( ~ sQ25_spl
| ~ lesseq(sK3_skl,X0)
| lesseq(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f2119]) ).
fof(f2128,plain,
( ~ sQ0_spl
| ~ sQ8_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f2091,f2119,f485,f69]) ).
fof(f2165,plain,
( sQ0_spl
| ~ sQ5_spl
| ~ minsol_model_ub(sK3_skl,sK4_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f476,f71]) ).
fof(f2169,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ5_spl
| ~ model_max(sK3_skl,sK4_skl,sK1_skl(sK4_skl,X1,X0))
| ~ model_max(X0,X1,max(sK3_skl,sK4_skl))
| minsol_model_max(X0,X1,max(sK3_skl,sK4_skl)) ),
inference(paramodulation,[status(thm)],[f489,f166]) ).
fof(f2181,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| ~ lesseq(sK4_skl,sK3_skl)
| sK4_skl = sK3_skl ),
inference(paramodulation,[status(thm)],[f489,f31]) ).
fof(f2185,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ5_spl
| ~ model_max(sK3_skl,sK4_skl,sK1_skl(sK4_skl,X1,X0))
| ~ model_max(X0,X1,max(sK3_skl,sK4_skl))
| minsol_model_max(X0,X1,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f489,f2169]) ).
fof(f2186,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ5_spl
| ~ model_max(sK3_skl,sK4_skl,sK1_skl(sK4_skl,X1,X0))
| ~ model_max(X0,X1,sK4_skl)
| minsol_model_max(X0,X1,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f489,f2185]) ).
fof(f2192,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| ~ sQ8_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2181,f539,f485,f475,f105]) ).
fof(f2274,definition,
( sQ28_spl
<=> minsol_model_max(sK3_skl,sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f2275,plain,
( ~ sQ28_spl
| minsol_model_max(sK3_skl,sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f2274]) ).
fof(f2277,definition,
( sQ29_spl
<=> model_max(sK3_skl,sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f2406,plain,
( ~ sQ25_spl
| lesseq(sK5_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f2120,f16]) ).
fof(f2412,plain,
( ~ sQ25_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f2406,f994,f2119]) ).
fof(f2852,definition,
( sQ34_spl
<=> max(sK3_skl,sK4_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f2853,plain,
( ~ sQ34_spl
| max(sK3_skl,sK4_skl) = sK4_skl ),
inference(component_clause,[status(thm)],[f2852]) ).
fof(f2936,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ5_spl
| model_max(X0,X1,sK4_skl)
| model_max(sK3_skl,sK4_skl,max(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f476,f466]) ).
fof(f2943,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| model_max(sK3_skl,sK4_skl,sK4_skl)
| model_max(sK3_skl,sK4_skl,sK4_skl) ),
inference(paramodulation,[status(thm)],[f489,f2936]) ).
fof(f2945,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f2943,f2277,f475,f105]) ).
fof(f3319,plain,
( ~ sQ3_spl
| ~ sQ7_spl
| max(sK3_skl,sK4_skl) = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f483,f106]) ).
fof(f3327,plain,
( ~ sQ3_spl
| ~ sQ7_spl
| minsol_model_max(sK3_skl,sK4_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f3319,f1324]) ).
fof(f3515,plain,
( ~ sQ34_spl
| ~ lesseq(sK4_skl,sK3_skl)
| sK4_skl = sK3_skl ),
inference(paramodulation,[status(thm)],[f2853,f31]) ).
fof(f3525,plain,
( ~ sQ34_spl
| ~ sQ8_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f3515,f539,f485,f2852]) ).
fof(f4059,plain,
! [X0,X1] :
( ~ model_ub(X0,X1,X0)
| minsol_model_ub(X0,X1,X0)
| ~ model_ub(X0,X1,X0)
| minsol_model_ub(X0,X1,X0) ),
inference(resolution,[status(thm)],[f989,f63]) ).
fof(f4064,plain,
! [X0,X1] :
( ~ model_ub(X0,X1,X0)
| minsol_model_ub(X0,X1,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f4059]) ).
fof(f4065,plain,
! [X0,X1,X2] :
( ~ lesseq(X1,X2)
| ~ lesseq(X0,X2)
| ~ lesseq(X2,X0)
| minsol_model_ub(X0,X1,X0) ),
inference(resolution,[status(thm)],[f4064,f165]) ).
fof(f4070,plain,
! [X0,X1] :
( ~ model_ub(X0,X1,X1)
| minsol_model_ub(X0,X1,X1)
| ~ model_ub(X0,X1,X1)
| minsol_model_ub(X0,X1,X1) ),
inference(resolution,[status(thm)],[f1151,f63]) ).
fof(f4075,plain,
! [X0,X1] :
( ~ model_ub(X0,X1,X1)
| minsol_model_ub(X0,X1,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f4070]) ).
fof(f4207,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| ~ model_max(sK3_skl,sK4_skl,sK4_skl)
| minsol_model_max(sK3_skl,sK4_skl,sK4_skl)
| ~ model_max(sK3_skl,sK4_skl,sK4_skl)
| minsol_model_max(sK3_skl,sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f2186,f54]) ).
fof(f4208,plain,
( ~ sQ3_spl
| ~ sQ5_spl
| ~ sQ29_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f4207,f2274,f2277,f475,f105]) ).
fof(f4219,plain,
! [X0,X1,X2] :
( ~ lesseq(X1,X2)
| ~ lesseq(X0,X2)
| ~ lesseq(X2,X1)
| minsol_model_ub(X0,X1,X1) ),
inference(resolution,[status(thm)],[f4075,f165]) ).
fof(f4220,plain,
! [X0] :
( sQ0_spl
| ~ sQ5_spl
| ~ lesseq(sK4_skl,X0)
| ~ lesseq(sK3_skl,X0)
| ~ lesseq(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f4219,f2165]) ).
fof(f4282,plain,
( sQ0_spl
| ~ sQ5_spl
| ~ lesseq(sK3_skl,sK4_skl)
| ~ lesseq(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f4220,f16]) ).
fof(f4310,plain,
( sQ0_spl
| ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f4282,f583,f478,f475,f69]) ).
fof(f4313,plain,
( sQ3_spl
| ~ sQ5_spl
| max(sK3_skl,sK4_skl) != sK4_skl ),
inference(forward_demodulation,[status(thm)],[f476,f107]) ).
fof(f4615,plain,
( sQ1_spl
| ~ sQ5_spl
| ~ minsol_model_max(sK3_skl,sK4_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f476,f74]) ).
fof(f4624,plain,
( sQ3_spl
| ~ sQ5_spl
| ~ lesseq(sK3_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f4313,f32]) ).
fof(f4625,plain,
( sQ3_spl
| ~ sQ5_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4624,f478,f475,f105]) ).
fof(f4641,plain,
( sQ1_spl
| ~ sQ5_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4615,f2275]) ).
fof(f4642,plain,
( sQ1_spl
| ~ sQ5_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f4641]) ).
fof(f4643,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f585,f16]) ).
fof(f4644,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f4643]) ).
fof(f4705,plain,
! [X0] :
( sQ19_spl
| ~ lesseq(sK4_skl,X0)
| ~ lesseq(sK3_skl,X0)
| ~ lesseq(X0,sK4_skl) ),
inference(resolution,[status(thm)],[f1361,f4219]) ).
fof(f4846,plain,
( sQ0_spl
| ~ sQ7_spl
| ~ minsol_model_ub(sK3_skl,sK4_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f483,f71]) ).
fof(f4847,plain,
! [X0] :
( sQ0_spl
| ~ sQ7_spl
| ~ lesseq(sK4_skl,X0)
| ~ lesseq(sK3_skl,X0)
| ~ lesseq(X0,sK3_skl) ),
inference(resolution,[status(thm)],[f4846,f4065]) ).
fof(f5401,plain,
( sQ19_spl
| ~ lesseq(sK3_skl,sK4_skl)
| ~ lesseq(sK4_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f4705,f16]) ).
fof(f5420,plain,
( sQ19_spl
| ~ sQ6_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f5401,f583,f478,f1359]) ).
fof(f5491,plain,
( sQ0_spl
| ~ sQ7_spl
| ~ lesseq(sK4_skl,sK3_skl)
| ~ lesseq(sK3_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f4847,f16]) ).
fof(f5532,plain,
( sQ0_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f5491,f518,f485,f482,f69]) ).
fof(f5545,plain,
( sQ1_spl
| ~ sQ7_spl
| ~ minsol_model_max(sK3_skl,sK4_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f483,f74]) ).
fof(f5940,plain,
( sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5545,f3327]) ).
fof(f5941,plain,
( sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f5940]) ).
fof(f5942,plain,
$false,
inference(sat_refutation,[status(thm)],[f75,f76,f108,f112,f481,f488,f524,f533,f542,f626,f945,f997,f1026,f1268,f1865,f1912,f1913,f1914,f2128,f2192,f2412,f2945,f3525,f4208,f4310,f4625,f4642,f4644,f5420,f5532,f5941]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM859+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 03:14:09 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 36.45/6.32 % Refutation found
% 36.45/6.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 36.45/6.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 36.45/6.35 % Elapsed time: 5.976708 seconds
% 36.45/6.35 % CPU time: 47.122394 seconds
% 36.45/6.35 % Total memory used: 250.057 MB
% 36.45/6.35 % Net memory used: 205.390 MB
%------------------------------------------------------------------------------