%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM858+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 02:26:56 PM UTC 2026
% Result : Theorem 9.17s 4.27s
% Output : CNFRefutation 9.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 18
% Syntax : Number of formulae : 395 ( 25 unt; 0 def)
% Number of atoms : 1112 ( 343 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1170 ( 453 ~; 664 |; 39 &)
% ( 9 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 466 ( 0 sgn 454 !; 12 ?; 296 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : lesseq(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_ref) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( lesseq(X1,X2)
& lesseq(X0,X1) )
=> lesseq(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_trans) ).
fof(f3,axiom,
! [X0,X1] :
( ( lesseq(X1,X0)
& lesseq(X0,X1) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_antisymmetric) ).
fof(f4,axiom,
! [X0,X1] :
( lesseq(X1,X0)
| lesseq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_total) ).
fof(f7,axiom,
! [X0,X1] :
( ~ lesseq(X1,X0)
| max(X0,X1) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_1) ).
fof(f8,axiom,
! [X0,X1] :
( ~ lesseq(X0,X1)
| max(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_2) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ub(X0,X1,X2)
<=> ( lesseq(X1,X2)
& lesseq(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ub) ).
fof(f10,axiom,
! [X0,X1,X2] :
( model_max(X0,X1,X2)
<=> X2 = max(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_max_1) ).
fof(f11,axiom,
! [X0,X1,X2] :
( model_ub(X0,X1,X2)
<=> ub(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_ub_1) ).
fof(f12,axiom,
! [X0,X1,X2] :
( minsol_model_max(X0,X1,X2)
<=> ( ! [X3] :
( model_max(X0,X1,X3)
=> lesseq(X2,X3) )
& model_max(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_max) ).
fof(f13,axiom,
! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> ( ! [X3] :
( model_ub(X0,X1,X3)
=> lesseq(X2,X3) )
& model_ub(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_ub) ).
fof(f14,conjecture,
! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> minsol_model_max(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_is_ub_1) ).
fof(f15,negated_conjecture,
~ ! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> minsol_model_max(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
? [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<~> minsol_model_max(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f17,plain,
! [X0,X1,X2] :
( minsol_model_max(X0,X1,X2)
<=> ( ! [X3] :
( ~ model_max(X0,X1,X3)
| lesseq(X2,X3) )
& model_max(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f18,plain,
! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> ( ! [X3] :
( ~ model_ub(X0,X1,X3)
| lesseq(X2,X3) )
& model_ub(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f13]) ).
fof(f19,plain,
! [X0,X1,X2] :
( ~ lesseq(X1,X2)
| ~ lesseq(X0,X1)
| lesseq(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f20,plain,
! [X0,X1,X2] :
( ~ lesseq(X1,X2)
| ~ lesseq(X0,X1)
| lesseq(X0,X2) ),
inference(flattening,[],[f19]) ).
fof(f21,plain,
! [X0,X1] :
( ~ lesseq(X1,X0)
| ~ lesseq(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f3]) ).
fof(f22,plain,
! [X0,X1] :
( ~ lesseq(X1,X0)
| ~ lesseq(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f21]) ).
fof(f23,plain,
? [X0,X1,X2] :
( ( minsol_model_ub(X0,X1,X2)
| minsol_model_max(X0,X1,X2) )
& ( ~ minsol_model_ub(X0,X1,X2)
| ~ minsol_model_max(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f24,plain,
( ( minsol_model_ub(sK0,sK1,sK2)
| minsol_model_max(sK0,sK1,sK2) )
& ( ~ minsol_model_ub(sK0,sK1,sK2)
| ~ minsol_model_max(sK0,sK1,sK2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f23]) ).
fof(f25,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_max(X0,X1,X2)
| ( ! [X3] :
( ~ model_max(X0,X1,X3)
| lesseq(X2,X3) )
& model_max(X0,X1,X2) ) )
& ( ? [X3] :
( model_max(X0,X1,X3)
& ~ lesseq(X2,X3) )
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f26,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_max(X0,X1,X2)
| ( ! [X3] :
( ~ model_max(X0,X1,X3)
| lesseq(X2,X3) )
& model_max(X0,X1,X2) ) )
& ( ? [X3] :
( model_max(X0,X1,X3)
& ~ lesseq(X2,X3) )
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_max(X0,X1,X2)
| ( ! [X4] :
( ~ model_max(X0,X1,X4)
| lesseq(X2,X4) )
& model_max(X0,X1,X2) ) )
& ( ? [X3] :
( model_max(X0,X1,X3)
& ~ lesseq(X2,X3) )
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ) ),
inference(rectify,[],[f26]) ).
fof(f28,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_max(X0,X1,X2)
| ( ! [X4] :
( ~ model_max(X0,X1,X4)
| lesseq(X2,X4) )
& model_max(X0,X1,X2) ) )
& ( ( model_max(X0,X1,sK3(X0,X1,X2))
& ~ lesseq(X2,sK3(X0,X1,X2)) )
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f27]) ).
fof(f29,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_ub(X0,X1,X2)
| ( ! [X3] :
( ~ model_ub(X0,X1,X3)
| lesseq(X2,X3) )
& model_ub(X0,X1,X2) ) )
& ( ? [X3] :
( model_ub(X0,X1,X3)
& ~ lesseq(X2,X3) )
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_ub(X0,X1,X2)
| ( ! [X3] :
( ~ model_ub(X0,X1,X3)
| lesseq(X2,X3) )
& model_ub(X0,X1,X2) ) )
& ( ? [X3] :
( model_ub(X0,X1,X3)
& ~ lesseq(X2,X3) )
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ) ),
inference(flattening,[],[f29]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_ub(X0,X1,X2)
| ( ! [X4] :
( ~ model_ub(X0,X1,X4)
| lesseq(X2,X4) )
& model_ub(X0,X1,X2) ) )
& ( ? [X3] :
( model_ub(X0,X1,X3)
& ~ lesseq(X2,X3) )
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ) ),
inference(rectify,[],[f30]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ( ~ minsol_model_ub(X0,X1,X2)
| ( ! [X4] :
( ~ model_ub(X0,X1,X4)
| lesseq(X2,X4) )
& model_ub(X0,X1,X2) ) )
& ( ( model_ub(X0,X1,sK4(X0,X1,X2))
& ~ lesseq(X2,sK4(X0,X1,X2)) )
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X3,sK4(X0,X1,X2))],[f31]) ).
fof(f33,plain,
! [X0,X1,X2] :
( ( ~ model_max(X0,X1,X2)
| X2 = max(X0,X1) )
& ( max(X0,X1) != X2
| model_max(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f34,plain,
! [X0,X1,X2] :
( ( ~ model_ub(X0,X1,X2)
| ub(X0,X1,X2) )
& ( ~ ub(X0,X1,X2)
| model_ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f35,plain,
! [X0,X1,X2] :
( ( ~ ub(X0,X1,X2)
| ( lesseq(X1,X2)
& lesseq(X0,X2) ) )
& ( ~ lesseq(X1,X2)
| ~ lesseq(X0,X2)
| ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ( ~ ub(X0,X1,X2)
| ( lesseq(X1,X2)
& lesseq(X0,X2) ) )
& ( ~ lesseq(X1,X2)
| ~ lesseq(X0,X2)
| ub(X0,X1,X2) ) ),
inference(flattening,[],[f35]) ).
fof(f37,plain,
( minsol_model_ub(sK0,sK1,sK2)
| minsol_model_max(sK0,sK1,sK2) ),
inference(cnf_transformation,[],[f24]) ).
fof(f38,plain,
( ~ minsol_model_ub(sK0,sK1,sK2)
| ~ minsol_model_max(sK0,sK1,sK2) ),
inference(cnf_transformation,[],[f24]) ).
fof(f39,plain,
! [X2,X0,X1,X4] :
( ~ minsol_model_max(X0,X1,X2)
| ~ model_max(X0,X1,X4)
| lesseq(X2,X4) ),
inference(cnf_transformation,[],[f28]) ).
fof(f40,plain,
! [X2,X0,X1] :
( ~ minsol_model_max(X0,X1,X2)
| model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f41,plain,
! [X2,X0,X1] :
( model_max(X0,X1,sK3(X0,X1,X2))
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f42,plain,
! [X2,X0,X1] :
( ~ lesseq(X2,sK3(X0,X1,X2))
| ~ model_max(X0,X1,X2)
| minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f28]) ).
fof(f43,plain,
! [X2,X0,X1,X4] :
( ~ minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X4)
| lesseq(X2,X4) ),
inference(cnf_transformation,[],[f32]) ).
fof(f44,plain,
! [X2,X0,X1] :
( ~ minsol_model_ub(X0,X1,X2)
| model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f32]) ).
fof(f45,plain,
! [X2,X0,X1] :
( model_ub(X0,X1,sK4(X0,X1,X2))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f32]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ lesseq(X2,sK4(X0,X1,X2))
| ~ model_ub(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f32]) ).
fof(f47,plain,
! [X0,X1] :
( lesseq(X1,X0)
| lesseq(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f48,plain,
! [X2,X0,X1] :
( ~ lesseq(X1,X2)
| ~ lesseq(X0,X1)
| lesseq(X0,X2) ),
inference(cnf_transformation,[],[f20]) ).
fof(f49,plain,
! [X0] : lesseq(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f50,plain,
! [X2,X0,X1] :
( ~ model_max(X0,X1,X2)
| max(X0,X1) = X2 ),
inference(cnf_transformation,[],[f33]) ).
fof(f51,plain,
! [X2,X0,X1] :
( max(X0,X1) != X2
| model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f33]) ).
fof(f52,plain,
! [X2,X0,X1] :
( ~ model_ub(X0,X1,X2)
| ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f53,plain,
! [X2,X0,X1] :
( ~ ub(X0,X1,X2)
| model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f54,plain,
! [X0,X1] :
( ~ lesseq(X0,X1)
| max(X0,X1) = X1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f55,plain,
! [X0,X1] :
( ~ lesseq(X1,X0)
| max(X0,X1) = X0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f56,plain,
! [X0,X1] :
( ~ lesseq(X1,X0)
| ~ lesseq(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f22]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ ub(X0,X1,X2)
| lesseq(X1,X2) ),
inference(cnf_transformation,[],[f36]) ).
fof(f58,plain,
! [X2,X0,X1] :
( ~ ub(X0,X1,X2)
| lesseq(X0,X2) ),
inference(cnf_transformation,[],[f36]) ).
fof(f59,plain,
! [X2,X0,X1] :
( ~ lesseq(X1,X2)
| ~ lesseq(X0,X2)
| ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f36]) ).
fof(f60,plain,
! [X0,X1] : model_max(X0,X1,max(X0,X1)),
inference(equality_resolution,[],[f51]) ).
tcf(c_49,negated_conjecture,
( ~ minsol_model_ub(sK0,sK1,sK2)
| ~ minsol_model_max(sK0,sK1,sK2) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_50,negated_conjecture,
( minsol_model_ub(sK0,sK1,sK2)
| minsol_model_max(sK0,sK1,sK2) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_max(X1,X2,X0)
| ~ model_max(X1,X2,X0)
| ~ lesseq(X0,sK3(X1,X2,X0)) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_max(X0,X1,X2)
| model_max(X0,X1,sK3(X0,X1,X2))
| ~ model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_max(X0,X1,X2)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( lesseq(X2,X3)
| ~ model_max(X0,X1,X3)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_ub(X1,X2,X0)
| ~ model_ub(X1,X2,X0)
| ~ lesseq(X0,sK4(X1,X2,X0)) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_ub(X0,X1,X2)
| model_ub(X0,X1,sK4(X0,X1,X2))
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_ub(X0,X1,X2)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( lesseq(X2,X3)
| ~ model_ub(X0,X1,X3)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( lesseq(X1,X0)
| lesseq(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i] :
( lesseq(X0,X2)
| ~ lesseq(X1,X2)
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_61,plain,
! [X0: $i] : lesseq(X0,X0),
inference(cnf_transformation,[],[f49]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : model_max(X0,X1,max(X0,X1)),
inference(cnf_transformation,[],[f60]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( max(X0,X1) = X2 )
| ~ model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_ub(X0,X1,X2)
| ~ ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( ( max(X0,X1) = X1 )
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( ( max(X1,X0) = X1 )
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ lesseq(X1,X0)
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( ub(X0,X2,X1)
| ~ lesseq(X2,X1)
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( lesseq(X0,X2)
| ~ ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( lesseq(X1,X2)
| ~ ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_72,plain,
lesseq(sK0,sK0),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_75,plain,
( model_ub(sK0,sK0,sK0)
| ~ ub(sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_80,plain,
( ub(sK0,sK0,sK0)
| ~ lesseq(sK0,sK0) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_81,plain,
( ( sK0 = sK0 )
| ~ lesseq(sK0,sK0) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_86,plain,
( ~ minsol_model_max(sK0,sK1,sK2)
| ~ minsol_model_ub(sK0,sK1,sK2) ),
inference(prop_impl_just,[status(thm)],[c_49]) ).
tcf(c_87,plain,
( ~ minsol_model_ub(sK0,sK1,sK2)
| ~ minsol_model_max(sK0,sK1,sK2) ),
inference(renaming,[status(thm)],[c_86]) ).
tcf(c_88,plain,
( minsol_model_max(sK0,sK1,sK2)
| minsol_model_ub(sK0,sK1,sK2) ),
inference(prop_impl_just,[status(thm)],[c_50]) ).
tcf(c_89,plain,
( minsol_model_ub(sK0,sK1,sK2)
| minsol_model_max(sK0,sK1,sK2) ),
inference(renaming,[status(thm)],[c_88]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_ub(X0,X1,X2)
| ~ ub(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_64]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_max(X0,X1,X2)
| ~ minsol_model_max(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_53]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i] :
( ub(X0,X1,X2)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_65,c_57]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_ub(X0,X1,X2)
| model_ub(X0,X1,sK4(X0,X1,X2))
| ~ ub(X0,X1,X2) ),
inference(bin_hyper_res,[status(thm)],[c_56,c_92]) ).
tcf(c_487,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( lesseq(X2,X3)
| minsol_model_ub(sK0,sK1,sK2)
| ~ model_max(X0,X1,X3)
| ( X2 != sK2 )
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_89,c_54]) ).
tcf(c_488,plain,
! [X0: $i] :
( lesseq(sK2,X0)
| minsol_model_ub(sK0,sK1,sK2)
| ~ model_max(sK0,sK1,X0) ),
inference(unflattening,[status(thm)],[c_487]) ).
tcf(c_499,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_ub(sK0,sK1,sK2)
| model_max(X0,X1,X2)
| ( X2 != sK2 )
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_89,c_94]) ).
tcf(c_500,plain,
( model_max(sK0,sK1,sK2)
| minsol_model_ub(sK0,sK1,sK2) ),
inference(unflattening,[status(thm)],[c_499]) ).
tcf(c_507,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_max(X0,X1,sK3(X0,X1,X2))
| ~ minsol_model_ub(sK0,sK1,sK2)
| ~ model_max(X0,X1,X2)
| ( X2 != sK2 )
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_87,c_52]) ).
tcf(c_508,plain,
( model_max(sK0,sK1,sK3(sK0,sK1,sK2))
| ~ model_max(sK0,sK1,sK2)
| ~ minsol_model_ub(sK0,sK1,sK2) ),
inference(unflattening,[status(thm)],[c_507]) ).
tcf(c_518,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ minsol_model_ub(sK0,sK1,sK2)
| ~ model_max(X0,X1,X2)
| ~ lesseq(X2,sK3(X0,X1,X2))
| ( X2 != sK2 )
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_87,c_51]) ).
tcf(c_519,plain,
( ~ model_max(sK0,sK1,sK2)
| ~ minsol_model_ub(sK0,sK1,sK2)
| ~ lesseq(sK2,sK3(sK0,sK1,sK2)) ),
inference(unflattening,[status(thm)],[c_518]) ).
tcf(c_672,plain,
! [X0: $i] :
( lesseq(sK2,X0)
| ~ model_max(sK0,sK1,sK2)
| ~ model_max(sK0,sK1,X0)
| ~ lesseq(sK2,sK3(sK0,sK1,sK2)) ),
inference(resolution,[status(thm)],[c_488,c_519]) ).
tcf(c_673,plain,
( lesseq(sK2,sK0)
| ~ model_max(sK0,sK1,sK2)
| ~ model_max(sK0,sK1,sK0)
| ~ lesseq(sK2,sK3(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_672]) ).
tcf(c_674,plain,
! [X0: $i] :
( lesseq(sK2,X0)
| model_max(sK0,sK1,sK3(sK0,sK1,sK2))
| ~ model_max(sK0,sK1,sK2)
| ~ model_max(sK0,sK1,X0) ),
inference(resolution,[status(thm)],[c_488,c_508]) ).
tcf(c_675,plain,
( lesseq(sK2,sK0)
| model_max(sK0,sK1,sK3(sK0,sK1,sK2))
| ~ model_max(sK0,sK1,sK2)
| ~ model_max(sK0,sK1,sK0) ),
inference(instantiation,[status(thm)],[c_674]) ).
tcf(c_847,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_849,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_850,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( minsol_model_ub(X0,X2,X4)
| ~ minsol_model_ub(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_851,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( model_max(X0,X2,X4)
| ~ model_max(X1,X3,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_853,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( lesseq(X0,X2)
| ~ lesseq(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_854,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( model_ub(X2,X3,X0)
| ~ model_ub(X2,X3,X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_1407,plain,
! [X0: $i] :
( lesseq(sK2,X0)
| model_max(sK0,sK1,sK2)
| ~ model_ub(sK0,sK1,X0) ),
inference(superposition,[status(thm)],[c_500,c_58]) ).
tcf(c_1415,plain,
( ub(sK0,sK1,sK2)
| model_max(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_500,c_100]) ).
tcf(c_1422,plain,
! [X0: $i,X1: $i] :
( lesseq(X1,X0)
| ( max(X0,X1) = X1 ) ),
inference(superposition,[status(thm)],[c_59,c_66]) ).
tcf(c_1443,plain,
! [X0: $i,X1: $i,X2: $i] :
( lesseq(X2,X1)
| lesseq(X0,X2)
| ~ lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_59,c_60]) ).
tcf(c_1456,plain,
( lesseq(sK1,sK2)
| model_max(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_1415,c_71]) ).
tcf(c_1457,plain,
( lesseq(sK0,sK2)
| model_max(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_1415,c_70]) ).
tcf(c_1482,plain,
! [X0: $i,X1: $i] :
( ( max(X0,X1) = X1 )
| ( max(X0,X1) = X0 ) ),
inference(superposition,[status(thm)],[c_1422,c_67]) ).
tcf(c_1560,plain,
( lesseq(sK0,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_1457,c_63]) ).
tcf(c_1561,plain,
( lesseq(sK1,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_1456,c_63]) ).
tcf(c_1572,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_1560,c_60]) ).
tcf(c_1606,plain,
( ( sK0 = sK2 )
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,sK0) ),
inference(superposition,[status(thm)],[c_1560,c_68]) ).
tcf(c_1621,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_ub(X0,X2,X1)
| ~ lesseq(X2,X1)
| ~ lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_69,c_64]) ).
tcf(c_1656,plain,
model_max(sK0,sK1,max(sK0,sK1)),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_1658,plain,
( minsol_model_ub(sK0,sK1,sK2)
| ~ model_ub(sK0,sK1,sK2)
| ~ lesseq(sK2,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_1659,plain,
( minsol_model_ub(sK0,sK1,sK2)
| model_ub(sK0,sK1,sK4(sK0,sK1,sK2))
| ~ ub(sK0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_170]) ).
tcf(c_1664,plain,
( ( sK1 = sK2 )
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,sK1) ),
inference(superposition,[status(thm)],[c_1561,c_68]) ).
tcf(c_1666,plain,
! [X0: $i] :
( lesseq(sK1,X0)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_1561,c_60]) ).
tcf(c_1682,plain,
( lesseq(sK1,sK0)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,sK0) ),
inference(instantiation,[status(thm)],[c_1666]) ).
tcf(c_1683,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_ub(sK0,sK1,sK2)
| ~ minsol_model_ub(X0,X1,X2)
| ( sK2 != X2 )
| ( sK1 != X1 )
| ( sK0 != X0 ) ),
inference(instantiation,[status(thm)],[c_850]) ).
tcf(c_1684,plain,
( minsol_model_ub(sK0,sK1,sK2)
| ~ minsol_model_ub(sK0,sK0,sK0)
| ( sK2 != sK0 )
| ( sK1 != sK0 )
| ( sK0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_1683]) ).
tcf(c_1685,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( model_max(sK0,sK1,X0)
| ~ model_max(X2,X3,X1)
| ( sK1 != X3 )
| ( sK0 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_851]) ).
tcf(c_1698,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK2,max(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_62,c_488]) ).
tcf(c_1705,plain,
! [X0: $i] :
( model_ub(sK0,sK1,sK2)
| ~ model_ub(sK0,sK1,X0)
| ( sK2 != X0 ) ),
inference(instantiation,[status(thm)],[c_854]) ).
tcf(c_1711,plain,
( minsol_model_ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(max(sK0,sK1),sK2) ),
inference(superposition,[status(thm)],[c_1698,c_68]) ).
tcf(c_1731,plain,
( ub(sK0,sK1,sK2)
| ~ minsol_model_ub(sK0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_1732,plain,
( ub(sK0,sK1,sK2)
| ~ model_ub(sK0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_1733,plain,
( ub(sK0,sK1,sK2)
| ~ lesseq(sK1,sK2)
| ~ lesseq(sK0,sK2) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_1750,plain,
( lesseq(sK2,sK1)
| minsol_model_ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK0 ) ),
inference(superposition,[status(thm)],[c_1482,c_1698]) ).
tcf(c_1777,plain,
! [X0: $i,X1: $i] :
( lesseq(sK2,sK3(sK0,sK1,sK2))
| ~ lesseq(X1,X0)
| ( sK2 != X1 )
| ( sK3(sK0,sK1,sK2) != X0 ) ),
inference(instantiation,[status(thm)],[c_853]) ).
tcf(c_1898,plain,
! [X0: $i] :
( lesseq(sK2,X0)
| model_max(sK0,sK1,sK2)
| ~ lesseq(sK1,X0)
| ~ lesseq(sK0,X0) ),
inference(superposition,[status(thm)],[c_1621,c_1407]) ).
tcf(c_1903,plain,
( lesseq(sK2,sK0)
| model_max(sK0,sK1,sK2)
| ~ lesseq(sK1,sK0)
| ~ lesseq(sK0,sK0) ),
inference(instantiation,[status(thm)],[c_1898]) ).
tcf(c_1984,plain,
! [X0: $i,X1: $i,X2: $i] :
( model_max(sK0,sK1,X0)
| ~ model_max(X2,sK1,X1)
| ( sK1 != sK1 )
| ( sK0 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_1685]) ).
tcf(c_1985,plain,
sK1 = sK1,
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1986,plain,
! [X0: $i,X1: $i] :
( ( sK1 = X0 )
| ( sK1 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_1993,plain,
! [X0: $i] :
( lesseq(sK1,X0)
| lesseq(X0,sK1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_1994,plain,
( lesseq(sK1,sK0)
| lesseq(sK0,sK1) ),
inference(instantiation,[status(thm)],[c_1993]) ).
tcf(c_1995,plain,
! [X0: $i,X1: $i,X2: $i] :
( lesseq(X0,sK1)
| ~ lesseq(X1,X2)
| ( sK1 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_853]) ).
tcf(c_1996,plain,
! [X0: $i,X1: $i] :
( lesseq(X0,sK1)
| ~ lesseq(X1,sK1)
| ~ lesseq(X0,X1) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_2102,plain,
( ub(sK0,sK1,sK2)
| model_max(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_500,c_100]) ).
tcf(c_2109,plain,
! [X0: $i,X1: $i] :
( lesseq(X1,X0)
| ( max(X0,X1) = X1 ) ),
inference(superposition,[status(thm)],[c_59,c_66]) ).
tcf(c_2118,plain,
! [X0: $i] :
( ( sK1 = X0 )
| ( sK1 != sK1 )
| ( X0 != sK1 ) ),
inference(instantiation,[status(thm)],[c_1986]) ).
tcf(c_2202,plain,
! [X0: $i,X1: $i] :
( model_max(sK0,sK1,X0)
| ~ model_max(X1,sK1,max(X1,sK1))
| ( sK1 != sK1 )
| ( sK0 != X1 )
| ( X0 != max(X1,sK1) ) ),
inference(instantiation,[status(thm)],[c_1984]) ).
tcf(c_2204,plain,
( model_max(sK0,sK1,sK0)
| ~ model_max(sK0,sK1,max(sK0,sK1))
| ( sK1 != sK1 )
| ( sK0 != sK0 )
| ( sK0 != max(sK0,sK1) ) ),
inference(instantiation,[status(thm)],[c_2202]) ).
tcf(c_2205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( model_max(X0,sK1,X2)
| ~ model_max(X1,X4,X3)
| ( sK1 != X4 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_851]) ).
tcf(c_2220,plain,
! [X0: $i,X1: $i] :
( ( sK1 = max(X0,X1) )
| ( sK1 != sK1 )
| ( max(X0,X1) != sK1 ) ),
inference(instantiation,[status(thm)],[c_2118]) ).
tcf(c_2301,plain,
! [X0: $i,X1: $i] :
( ( max(X0,X1) = sK3(sK0,sK1,sK2) )
| ~ model_max(X0,X1,sK3(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_2306,plain,
! [X0: $i] :
( ( X0 = sK3(sK0,sK1,sK2) )
| ~ lesseq(X0,sK3(sK0,sK1,sK2))
| ~ lesseq(sK3(sK0,sK1,sK2),X0) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_2382,plain,
( lesseq(sK0,sK2)
| model_max(sK0,sK1,sK2) ),
inference(superposition,[status(thm)],[c_2102,c_70]) ).
tcf(c_2491,plain,
! [X0: $i,X1: $i] :
( lesseq(X0,sK1)
| ~ lesseq(X1,sK1)
| ( sK1 != sK1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_1995]) ).
tcf(c_2501,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = max(X0,sK1) )
| ( X2 != X1 )
| ( max(X0,sK1) != X1 ) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_2502,plain,
( ( sK0 = max(sK0,sK1) )
| ( sK0 != sK0 )
| ( max(sK0,sK1) != sK0 ) ),
inference(instantiation,[status(thm)],[c_2501]) ).
tcf(c_2513,plain,
! [X0: $i,X1: $i] :
( ( max(X0,X1) = X1 )
| ( max(X0,X1) = X0 ) ),
inference(superposition,[status(thm)],[c_2109,c_67]) ).
tcf(c_2613,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( model_max(X0,sK1,X2)
| ~ model_max(X1,sK1,X3)
| ( sK1 != sK1 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_2205]) ).
tcf(c_2637,plain,
( ( sK3(sK0,sK1,sK2) = sK3(sK0,sK1,sK2) )
| ~ lesseq(sK3(sK0,sK1,sK2),sK3(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_2306]) ).
tcf(c_2638,plain,
lesseq(sK3(sK0,sK1,sK2),sK3(sK0,sK1,sK2)),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_2799,plain,
! [X0: $i] :
( ( sK1 = max(X0,sK1) )
| ( sK1 != sK1 )
| ( max(X0,sK1) != sK1 ) ),
inference(instantiation,[status(thm)],[c_2220]) ).
tcf(c_2801,plain,
( ( sK1 = max(sK0,sK1) )
| ( sK1 != sK1 )
| ( max(sK0,sK1) != sK1 ) ),
inference(instantiation,[status(thm)],[c_2799]) ).
tcf(c_2889,plain,
( lesseq(sK0,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_2382,c_63]) ).
tcf(c_2968,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_2889,c_60]) ).
tcf(c_2970,plain,
( ( max(sK0,sK2) = sK2 )
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_2889,c_66]) ).
tcf(c_3102,plain,
( ( max(sK0,sK1) = sK3(sK0,sK1,sK2) )
| ~ model_max(sK0,sK1,sK3(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_2301]) ).
tcf(c_3106,plain,
! [X0: $i,X1: $i] :
( ( sK3(sK0,sK1,sK2) = X1 )
| ( X1 != X0 )
| ( sK3(sK0,sK1,sK2) != X0 ) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_3160,plain,
lesseq(sK1,sK1),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_3240,plain,
! [X0: $i] :
( ( max(X0,sK1) = sK1 )
| ~ lesseq(X0,sK1) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_3242,plain,
( ( max(sK0,sK1) = sK1 )
| ~ lesseq(sK0,sK1) ),
inference(instantiation,[status(thm)],[c_3240]) ).
tcf(c_3477,plain,
! [X0: $i,X1: $i] :
( lesseq(X1,max(X0,sK1))
| lesseq(max(X0,sK1),X1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_3479,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( lesseq(max(X0,sK1),X2)
| ~ lesseq(X1,X3)
| ( X2 != X3 )
| ( max(X0,sK1) != X1 ) ),
inference(instantiation,[status(thm)],[c_853]) ).
tcf(c_3483,plain,
( lesseq(max(sK0,sK1),sK0)
| ~ lesseq(sK0,sK0)
| ( sK0 != sK0 )
| ( max(sK0,sK1) != sK0 ) ),
inference(instantiation,[status(thm)],[c_3479]) ).
tcf(c_3595,plain,
! [X0: $i,X1: $i] :
( ( max(X0,sK1) = X1 )
| ~ model_max(X0,sK1,X1) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_3599,plain,
! [X0: $i] :
( ( max(X0,sK1) = X0 )
| ~ lesseq(sK1,X0) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_3600,plain,
( ( max(sK0,sK1) = sK0 )
| ~ lesseq(sK1,sK0) ),
inference(instantiation,[status(thm)],[c_3599]) ).
tcf(c_3604,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( max(X0,sK1) = X2 )
| ( X2 != X1 )
| ( max(X0,sK1) != X1 ) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_3723,plain,
! [X0: $i,X1: $i] :
( model_max(X0,sK1,X1)
| ~ model_max(sK0,sK1,max(sK0,sK1))
| ( sK1 != sK1 )
| ( X1 != max(sK0,sK1) )
| ( X0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_2613]) ).
tcf(c_3798,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK2,max(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_62,c_488]) ).
tcf(c_3945,plain,
! [X0: $i] :
( lesseq(X0,sK1)
| ~ lesseq(sK1,sK1)
| ( sK1 != sK1 )
| ( X0 != sK1 ) ),
inference(instantiation,[status(thm)],[c_2491]) ).
tcf(c_3999,plain,
( model_max(sK0,sK1,sK2)
| ( sK1 = sK2 )
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK1,sK1)
| ~ lesseq(sK0,sK1) ),
inference(superposition,[status(thm)],[c_1898,c_1664]) ).
tcf(c_4000,plain,
! [X0: $i] :
( lesseq(sK2,X0)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK1,X0)
| ~ lesseq(sK0,X0) ),
inference(superposition,[status(thm)],[c_1898,c_63]) ).
tcf(c_4045,plain,
( model_max(sK0,sK1,sK2)
| ( sK1 = sK2 )
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3999,c_61]) ).
tcf(c_4060,plain,
( lesseq(sK2,sK0)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK1,sK0)
| ~ lesseq(sK0,sK0) ),
inference(instantiation,[status(thm)],[c_4000]) ).
tcf(c_4128,plain,
( lesseq(sK2,sK1)
| minsol_model_ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK0 ) ),
inference(superposition,[status(thm)],[c_2513,c_3798]) ).
tcf(c_4132,plain,
( lesseq(sK2,sK0)
| minsol_model_ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_2513,c_3798]) ).
tcf(c_4461,plain,
! [X0: $i] :
( lesseq(sK2,sK4(sK0,sK1,sK2))
| ~ lesseq(sK2,X0)
| ~ lesseq(X0,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_4464,plain,
( lesseq(sK2,sK4(sK0,sK1,sK2))
| ~ lesseq(sK2,sK0)
| ~ lesseq(sK0,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_4461]) ).
tcf(c_4702,plain,
! [X0: $i] :
( ( sK2 = X0 )
| ~ lesseq(sK2,X0)
| ~ lesseq(X0,sK2) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_4703,plain,
( ( sK2 = sK0 )
| ~ lesseq(sK2,sK0)
| ~ lesseq(sK0,sK2) ),
inference(instantiation,[status(thm)],[c_4702]) ).
tcf(c_4704,plain,
! [X0: $i] :
( lesseq(sK2,sK3(sK0,sK1,sK2))
| ~ lesseq(sK2,X0)
| ( sK2 != sK2 )
| ( sK3(sK0,sK1,sK2) != X0 ) ),
inference(instantiation,[status(thm)],[c_1777]) ).
tcf(c_4705,plain,
sK2 = sK2,
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_4707,plain,
! [X0: $i,X1: $i] :
( ( sK2 = X0 )
| ( sK2 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_4752,plain,
! [X0: $i] :
( ( sK3(sK0,sK1,sK2) = X0 )
| ( X0 != sK3(sK0,sK1,sK2) )
| ( sK3(sK0,sK1,sK2) != sK3(sK0,sK1,sK2) ) ),
inference(instantiation,[status(thm)],[c_3106]) ).
tcf(c_4775,plain,
! [X0: $i,X1: $i] :
( ( X0 = sK2 )
| ( sK2 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_4887,plain,
! [X0: $i] :
( lesseq(sK1,max(X0,sK1))
| lesseq(max(X0,sK1),sK1) ),
inference(instantiation,[status(thm)],[c_3477]) ).
tcf(c_4894,plain,
( lesseq(sK1,max(sK0,sK1))
| lesseq(max(sK0,sK1),sK1) ),
inference(instantiation,[status(thm)],[c_4887]) ).
tcf(c_5303,plain,
! [X0: $i,X1: $i] :
( lesseq(X0,sK1)
| ~ lesseq(max(X1,sK1),sK1)
| ~ lesseq(X0,max(X1,sK1)) ),
inference(instantiation,[status(thm)],[c_1996]) ).
tcf(c_5305,plain,
( lesseq(sK0,sK1)
| ~ lesseq(sK0,max(sK0,sK1))
| ~ lesseq(max(sK0,sK1),sK1) ),
inference(instantiation,[status(thm)],[c_5303]) ).
tcf(c_5329,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( lesseq(X2,max(X0,sK1))
| ~ lesseq(X3,X1)
| ( X2 != X3 )
| ( max(X0,sK1) != X1 ) ),
inference(instantiation,[status(thm)],[c_853]) ).
tcf(c_5333,plain,
( lesseq(sK0,max(sK0,sK1))
| ~ lesseq(sK0,sK0)
| ( sK0 != sK0 )
| ( max(sK0,sK1) != sK0 ) ),
inference(instantiation,[status(thm)],[c_5329]) ).
tcf(c_5446,plain,
! [X0: $i] :
( model_max(X0,sK1,sK2)
| ~ model_max(sK0,sK1,max(sK0,sK1))
| ( sK2 != max(sK0,sK1) )
| ( sK1 != sK1 )
| ( X0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_3723]) ).
tcf(c_5447,plain,
( model_max(sK0,sK1,sK2)
| ~ model_max(sK0,sK1,max(sK0,sK1))
| ( sK2 != max(sK0,sK1) )
| ( sK1 != sK1 )
| ( sK0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_5446]) ).
tcf(c_5829,plain,
! [X0: $i,X1: $i] :
( lesseq(sK2,sK3(sK0,sK1,sK2))
| ~ lesseq(max(X1,sK1),X0)
| ( sK2 != max(X1,sK1) )
| ( sK3(sK0,sK1,sK2) != X0 ) ),
inference(instantiation,[status(thm)],[c_1777]) ).
tcf(c_5831,plain,
( lesseq(sK2,sK3(sK0,sK1,sK2))
| ~ lesseq(max(sK0,sK1),sK0)
| ( sK2 != max(sK0,sK1) )
| ( sK3(sK0,sK1,sK2) != sK0 ) ),
inference(instantiation,[status(thm)],[c_5829]) ).
tcf(c_5844,plain,
! [X0: $i,X1: $i] :
( ( sK3(sK0,sK1,sK2) = X1 )
| ( X1 != max(X0,sK1) )
| ( sK3(sK0,sK1,sK2) != max(X0,sK1) ) ),
inference(instantiation,[status(thm)],[c_3106]) ).
tcf(c_5848,plain,
( ( sK3(sK0,sK1,sK2) = sK0 )
| ( sK0 != max(sK0,sK1) )
| ( sK3(sK0,sK1,sK2) != max(sK0,sK1) ) ),
inference(instantiation,[status(thm)],[c_5844]) ).
tcf(c_6008,plain,
! [X0: $i] :
( ( max(X0,sK1) = sK2 )
| ~ model_max(X0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_3595]) ).
tcf(c_6010,plain,
( ( max(sK0,sK1) = sK2 )
| ~ model_max(sK0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_6008]) ).
tcf(c_6892,plain,
! [X0: $i,X1: $i] :
( lesseq(sK0,sK2)
| ~ lesseq(X0,X1)
| ( sK2 != X1 )
| ( sK0 != X0 ) ),
inference(instantiation,[status(thm)],[c_853]) ).
tcf(c_6896,plain,
( lesseq(sK0,sK2)
| ~ lesseq(sK0,sK0)
| ( sK2 != sK0 )
| ( sK0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_6892]) ).
tcf(c_7068,plain,
! [X0: $i] :
( model_ub(sK0,sK1,sK2)
| ~ model_ub(sK0,sK1,max(X0,sK1))
| ( sK2 != max(X0,sK1) ) ),
inference(instantiation,[status(thm)],[c_1705]) ).
tcf(c_7070,plain,
( model_ub(sK0,sK1,sK2)
| ~ model_ub(sK0,sK1,max(sK0,sK1))
| ( sK2 != max(sK0,sK1) ) ),
inference(instantiation,[status(thm)],[c_7068]) ).
tcf(c_7190,plain,
! [X0: $i] :
( ( sK3(sK0,sK1,sK2) = max(X0,sK1) )
| ( max(X0,sK1) != sK3(sK0,sK1,sK2) )
| ( sK3(sK0,sK1,sK2) != sK3(sK0,sK1,sK2) ) ),
inference(instantiation,[status(thm)],[c_4752]) ).
tcf(c_7192,plain,
( ( sK3(sK0,sK1,sK2) = max(sK0,sK1) )
| ( max(sK0,sK1) != sK3(sK0,sK1,sK2) )
| ( sK3(sK0,sK1,sK2) != sK3(sK0,sK1,sK2) ) ),
inference(instantiation,[status(thm)],[c_7190]) ).
tcf(c_7201,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_ub(X0,X1,X2)
| ub(X0,X1,sK4(X0,X1,X2))
| ~ ub(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_170,c_65]) ).
tcf(c_7211,plain,
( minsol_model_ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_1711,c_500,c_6010]) ).
tcf(c_7217,plain,
( ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_7211,c_100]) ).
tcf(c_7218,plain,
! [X0: $i] :
( lesseq(sK2,X0)
| ( max(sK0,sK1) = sK2 )
| ~ model_ub(sK0,sK1,X0) ),
inference(superposition,[status(thm)],[c_7211,c_58]) ).
tcf(c_7519,plain,
! [X0: $i] :
( ( sK2 = X0 )
| ( sK2 != sK2 )
| ( X0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_4707]) ).
tcf(c_7520,plain,
( ( sK2 = sK0 )
| ( sK2 != sK2 )
| ( sK0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_7519]) ).
tcf(c_7787,plain,
lesseq(sK2,sK2),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_7792,plain,
( lesseq(sK2,sK1)
| lesseq(sK1,sK2) ),
inference(instantiation,[status(thm)],[c_1993]) ).
tcf(c_9306,plain,
! [X0: $i,X1: $i] :
( ( max(X0,sK1) = sK2 )
| ( sK2 != X1 )
| ( max(X0,sK1) != X1 ) ),
inference(instantiation,[status(thm)],[c_3604]) ).
tcf(c_9308,plain,
( ( max(sK0,sK1) = sK2 )
| ( sK2 != sK0 )
| ( max(sK0,sK1) != sK0 ) ),
inference(instantiation,[status(thm)],[c_9306]) ).
tcf(c_10283,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK0,max(sK0,sK1))
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_3798,c_2968]) ).
tcf(c_10605,plain,
( ( sK2 = max(sK0,sK1) )
| ( sK2 != sK2 )
| ( max(sK0,sK1) != sK2 ) ),
inference(instantiation,[status(thm)],[c_7519]) ).
tcf(c_10997,plain,
( lesseq(sK2,sK1)
| ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK0 ) ),
inference(superposition,[status(thm)],[c_4128,c_100]) ).
tcf(c_11160,plain,
( lesseq(sK2,sK0)
| ( max(sK0,sK1) = sK1 ) ),
inference(global_subsumption_just,[status(thm)],[c_4132,c_72,c_81,c_673,c_675,c_1656,c_1903,c_1985,c_1994,c_2204,c_2502,c_2637,c_2638,c_3102,c_3242,c_3483,c_3600,c_4060,c_4705,c_5831,c_5848,c_7192,c_10605]) ).
tcf(c_11172,plain,
( ( max(sK0,sK2) = sK0 )
| ( max(sK0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_11160,c_67]) ).
tcf(c_12250,plain,
! [X0: $i] :
( lesseq(X0,sK1)
| ~ lesseq(sK2,sK1)
| ~ lesseq(X0,sK2) ),
inference(instantiation,[status(thm)],[c_1996]) ).
tcf(c_12286,plain,
( ( sK0 = sK2 )
| ( max(sK0,sK1) = sK2 )
| ( max(sK0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_11172,c_2970]) ).
tcf(c_12690,plain,
! [X0: $i] :
( lesseq(sK0,sK2)
| ~ lesseq(X0,sK2)
| ( sK2 != sK2 )
| ( sK0 != X0 ) ),
inference(instantiation,[status(thm)],[c_6892]) ).
tcf(c_12694,plain,
! [X0: $i,X1: $i] :
( lesseq(sK0,sK2)
| ~ lesseq(X0,max(X1,sK1))
| ( sK2 != max(X1,sK1) )
| ( sK0 != X0 ) ),
inference(instantiation,[status(thm)],[c_6892]) ).
tcf(c_12697,plain,
! [X0: $i,X1: $i] :
( ( X0 = sK2 )
| ( sK2 != max(X1,sK1) )
| ( X0 != max(X1,sK1) ) ),
inference(instantiation,[status(thm)],[c_4775]) ).
tcf(c_12701,plain,
( ( sK0 = sK2 )
| ( sK2 != max(sK0,sK1) )
| ( sK0 != max(sK0,sK1) ) ),
inference(instantiation,[status(thm)],[c_12697]) ).
tcf(c_12704,plain,
( lesseq(sK0,sK2)
| ~ lesseq(sK0,max(sK0,sK1))
| ( sK2 != max(sK0,sK1) )
| ( sK0 != sK0 ) ),
inference(instantiation,[status(thm)],[c_12694]) ).
tcf(c_12927,plain,
! [X0: $i] :
( model_ub(sK0,sK1,max(X0,sK1))
| ~ ub(sK0,sK1,max(X0,sK1)) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_12928,plain,
( model_ub(sK0,sK1,max(sK0,sK1))
| ~ ub(sK0,sK1,max(sK0,sK1)) ),
inference(instantiation,[status(thm)],[c_12927]) ).
tcf(c_14172,plain,
( ( sK0 = sK2 )
| ( max(sK0,sK1) = sK1 ) ),
inference(global_subsumption_just,[status(thm)],[c_12286,c_72,c_81,c_1606,c_1994,c_2502,c_3242,c_3600,c_4705,c_10605,c_11160,c_12701]) ).
tcf(c_14183,plain,
( model_max(sK0,sK1,sK1)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_14172,c_62]) ).
tcf(c_14598,plain,
( lesseq(sK2,sK1)
| ub(sK0,sK1,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_10997,c_72,c_81,c_1731,c_1733,c_1750,c_4705,c_5333,c_7217,c_7792,c_10605,c_12704]) ).
tcf(c_14606,plain,
( lesseq(sK2,sK1)
| lesseq(sK0,sK2) ),
inference(superposition,[status(thm)],[c_14598,c_70]) ).
tcf(c_15881,plain,
( minsol_model_ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_10283,c_7211]) ).
tcf(c_15891,plain,
( ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_15881,c_100]) ).
tcf(c_15901,plain,
! [X0: $i,X1: $i] :
( lesseq(X1,X0)
| ( max(X0,X1) = X1 ) ),
inference(superposition,[status(thm)],[c_59,c_66]) ).
tcf(c_15921,plain,
! [X0: $i,X1: $i,X2: $i] :
( lesseq(X2,X1)
| lesseq(X0,X2)
| ~ lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_59,c_60]) ).
tcf(c_15961,plain,
! [X0: $i,X1: $i] :
( ( max(X0,X1) = X1 )
| ( max(X0,X1) = X0 ) ),
inference(superposition,[status(thm)],[c_15901,c_67]) ).
tcf(c_15987,plain,
( lesseq(sK1,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_15891,c_71]) ).
tcf(c_15988,plain,
( lesseq(sK0,sK2)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_15891,c_70]) ).
tcf(c_16049,plain,
( ( sK1 = sK2 )
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,sK1) ),
inference(superposition,[status(thm)],[c_15987,c_68]) ).
tcf(c_16050,plain,
( ( sK0 = sK2 )
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,sK0) ),
inference(superposition,[status(thm)],[c_15988,c_68]) ).
tcf(c_16083,plain,
( ( sK1 = sK2 )
| ( max(sK0,sK1) = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_16049,c_72,c_1560,c_1682,c_1903,c_1994,c_3600,c_4045,c_4703,c_6010,c_9308]) ).
tcf(c_16089,plain,
( model_max(sK0,sK1,sK2)
| ( sK1 = sK2 ) ),
inference(superposition,[status(thm)],[c_16083,c_62]) ).
tcf(c_16092,plain,
( ~ lesseq(sK2,sK0)
| ( max(sK0,sK1) = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_16050,c_1560,c_1682,c_3600,c_4703,c_9308]) ).
tcf(c_16093,plain,
( ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK2,sK0) ),
inference(renaming,[status(thm)],[c_16092]) ).
tcf(c_16217,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK2,max(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_62,c_488]) ).
tcf(c_16285,plain,
( ( sK1 = sK2 )
| ( max(sK0,sK1) = sK0 ) ),
inference(superposition,[status(thm)],[c_15961,c_16083]) ).
tcf(c_16289,plain,
( lesseq(sK2,sK0)
| minsol_model_ub(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_15961,c_16217]) ).
tcf(c_16320,plain,
( lesseq(sK2,sK0)
| ( max(sK0,sK1) = sK1 ) ),
inference(global_subsumption_just,[status(thm)],[c_16289,c_11160]) ).
tcf(c_16327,plain,
( ( sK0 = sK2 )
| ( max(sK0,sK1) = sK1 )
| ~ lesseq(sK0,sK2) ),
inference(superposition,[status(thm)],[c_16320,c_68]) ).
tcf(c_16401,plain,
( model_max(sK0,sK1,sK0)
| ( sK1 = sK2 ) ),
inference(superposition,[status(thm)],[c_16285,c_62]) ).
tcf(c_16402,plain,
( lesseq(sK2,sK0)
| minsol_model_ub(sK0,sK1,sK2)
| ( sK1 = sK2 ) ),
inference(superposition,[status(thm)],[c_16285,c_16217]) ).
tcf(c_16403,plain,
( ( sK1 = sK2 )
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_16285,c_16083]) ).
tcf(c_16427,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK1,max(sK0,sK1))
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_16403,c_16217]) ).
tcf(c_16516,plain,
( lesseq(sK2,sK0)
| ( sK1 = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_16402,c_72,c_81,c_673,c_675,c_2502,c_2637,c_2638,c_3102,c_3483,c_4705,c_5831,c_5848,c_7192,c_10605,c_16083,c_16089,c_16285,c_16401]) ).
tcf(c_16592,plain,
( ( sK0 = sK2 )
| ( max(sK0,sK1) = sK1 ) ),
inference(global_subsumption_just,[status(thm)],[c_16327,c_14172]) ).
tcf(c_16604,plain,
( lesseq(sK2,sK1)
| minsol_model_ub(sK0,sK1,sK2)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_16592,c_16217]) ).
tcf(c_16622,plain,
( lesseq(sK2,sK1)
| ub(sK0,sK1,sK2)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_16604,c_100]) ).
tcf(c_16768,plain,
( lesseq(sK2,sK1)
| ub(sK0,sK1,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_16622,c_14598]) ).
tcf(c_16777,plain,
( lesseq(sK2,sK1)
| lesseq(sK0,sK2) ),
inference(superposition,[status(thm)],[c_16768,c_70]) ).
tcf(c_16832,plain,
! [X0: $i] :
( lesseq(sK0,sK2)
| lesseq(sK2,X0)
| lesseq(X0,sK1) ),
inference(superposition,[status(thm)],[c_16777,c_15921]) ).
tcf(c_16833,plain,
( lesseq(sK0,sK2)
| ( sK1 = sK2 )
| ~ lesseq(sK1,sK2) ),
inference(superposition,[status(thm)],[c_16777,c_68]) ).
tcf(c_16945,plain,
( lesseq(sK0,sK2)
| ( sK1 = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_16833,c_72,c_81,c_4705,c_5333,c_10605,c_12704,c_16083,c_16285]) ).
tcf(c_17064,plain,
! [X0: $i] :
( lesseq(sK0,sK2)
| lesseq(X0,sK1)
| ( X0 = sK2 )
| ~ lesseq(X0,sK2) ),
inference(superposition,[status(thm)],[c_16832,c_68]) ).
tcf(c_17068,plain,
( lesseq(sK0,sK2)
| lesseq(sK0,sK1)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_16832,c_16093]) ).
tcf(c_17231,plain,
( lesseq(sK0,sK2)
| lesseq(sK0,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_17068,c_72,c_81,c_673,c_675,c_1606,c_1656,c_1903,c_1985,c_1994,c_2204,c_2502,c_2637,c_2638,c_3102,c_3483,c_3600,c_4060,c_4705,c_5831,c_5848,c_6896,c_7192,c_7520,c_10605,c_12701]) ).
tcf(c_17237,plain,
( lesseq(sK0,sK1)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_16403,c_17231]) ).
tcf(c_17238,plain,
! [X0: $i] :
( lesseq(sK0,sK1)
| lesseq(sK0,X0)
| lesseq(X0,sK2) ),
inference(superposition,[status(thm)],[c_17231,c_15921]) ).
tcf(c_17675,plain,
! [X0: $i,X1: $i] :
( lesseq(sK0,X1)
| lesseq(sK0,X0)
| lesseq(X1,sK1)
| lesseq(X0,sK2) ),
inference(superposition,[status(thm)],[c_17238,c_15921]) ).
tcf(c_18217,plain,
! [X0: $i,X1: $i,X2: $i] :
( minsol_model_ub(X0,X1,X2)
| lesseq(X1,sK4(X0,X1,X2))
| ~ ub(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_7201,c_71]) ).
tcf(c_18232,plain,
! [X0: $i,X1: $i] :
( minsol_model_ub(X0,X1,X1)
| ~ ub(X0,X1,X1)
| ~ model_ub(X0,X1,X1) ),
inference(superposition,[status(thm)],[c_18217,c_55]) ).
tcf(c_18351,plain,
( minsol_model_ub(sK0,sK0,sK0)
| ~ ub(sK0,sK0,sK0)
| ~ model_ub(sK0,sK0,sK0) ),
inference(instantiation,[status(thm)],[c_18232]) ).
tcf(c_18480,plain,
! [X0: $i,X1: $i] :
( minsol_model_ub(X0,X1,X1)
| ~ ub(X0,X1,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18232,c_64]) ).
tcf(c_18487,plain,
! [X0: $i,X1: $i] :
( minsol_model_ub(X0,X1,X1)
| ~ lesseq(X1,X1)
| ~ lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_69,c_18480]) ).
tcf(c_18488,plain,
! [X0: $i,X1: $i] :
( minsol_model_ub(X0,X1,X1)
| ~ lesseq(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18487,c_61]) ).
tcf(c_18496,plain,
! [X0: $i,X1: $i] :
( ub(X0,X1,X1)
| ~ lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_18488,c_100]) ).
tcf(c_18507,plain,
! [X0: $i,X1: $i] :
( model_ub(X0,X1,X1)
| ~ lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_18496,c_64]) ).
tcf(c_18518,plain,
( lesseq(sK2,sK1)
| ( max(sK0,sK1) = sK2 )
| ~ lesseq(sK0,sK1) ),
inference(superposition,[status(thm)],[c_18507,c_7218]) ).
tcf(c_18519,plain,
( lesseq(sK2,sK1)
| model_max(sK0,sK1,sK2)
| ~ lesseq(sK0,sK1) ),
inference(superposition,[status(thm)],[c_18507,c_1407]) ).
tcf(c_18526,plain,
( lesseq(sK2,sK1)
| model_max(sK0,sK1,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_18519,c_72,c_81,c_1457,c_1656,c_1682,c_1903,c_1985,c_1994,c_3600,c_4703,c_4705,c_5447,c_9308,c_10605,c_18518]) ).
tcf(c_18532,plain,
( lesseq(sK2,sK1)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_18526,c_63]) ).
tcf(c_18540,plain,
( ( sK1 = sK2 )
| ( max(sK0,sK1) = sK2 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1664,c_18532]) ).
tcf(c_18561,plain,
( lesseq(sK0,sK1)
| ( max(sK0,sK1) = sK2 ) ),
inference(superposition,[status(thm)],[c_18532,c_1572]) ).
tcf(c_18645,plain,
( ( max(sK0,sK1) = sK2 )
| ( max(sK0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_18561,c_66]) ).
tcf(c_18700,plain,
( ( sK1 = sK2 )
| ( max(sK0,sK1) = sK0 ) ),
inference(superposition,[status(thm)],[c_18540,c_1482]) ).
tcf(c_18779,plain,
( ( sK1 = sK2 )
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_18700,c_18540]) ).
tcf(c_18923,plain,
( lesseq(sK2,sK1)
| model_max(sK0,sK1,sK1)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_18779,c_18526]) ).
tcf(c_19008,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK1,max(sK0,sK1))
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_18779,c_1698]) ).
tcf(c_19363,plain,
( lesseq(sK0,sK2)
| ~ lesseq(sK2,sK2)
| ( sK2 != sK2 )
| ( sK0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_12690]) ).
tcf(c_20087,plain,
( ( sK0 = sK2 )
| model_max(sK0,sK1,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_18923,c_14183]) ).
tcf(c_20088,plain,
( model_max(sK0,sK1,sK1)
| ( sK0 = sK2 ) ),
inference(renaming,[status(thm)],[c_20087]) ).
tcf(c_20094,plain,
( lesseq(sK2,sK1)
| minsol_model_ub(sK0,sK1,sK2)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_20088,c_488]) ).
tcf(c_20530,plain,
( model_max(sK0,sK1,sK2)
| ( max(sK0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_18645,c_62]) ).
tcf(c_20601,plain,
( lesseq(sK2,sK1)
| minsol_model_ub(sK0,sK1,sK1)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_18779,c_20094]) ).
tcf(c_20602,plain,
( lesseq(sK2,sK1)
| ub(sK0,sK1,sK2)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_20094,c_100]) ).
tcf(c_20687,plain,
( lesseq(sK2,sK1)
| ub(sK0,sK1,sK1)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_20601,c_100]) ).
tcf(c_20696,plain,
( lesseq(sK2,sK1)
| ub(sK0,sK1,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_20602,c_14598]) ).
tcf(c_20705,plain,
( lesseq(sK2,sK1)
| lesseq(sK0,sK2) ),
inference(superposition,[status(thm)],[c_20696,c_70]) ).
tcf(c_20727,plain,
( lesseq(sK0,sK2)
| ( sK1 = sK2 )
| ~ lesseq(sK1,sK2) ),
inference(superposition,[status(thm)],[c_20705,c_68]) ).
tcf(c_20728,plain,
! [X0: $i] :
( lesseq(sK0,sK2)
| lesseq(sK2,X0)
| lesseq(X0,sK1) ),
inference(superposition,[status(thm)],[c_20705,c_1443]) ).
tcf(c_20833,plain,
! [X0: $i,X1: $i] :
( lesseq(sK0,sK2)
| lesseq(sK2,X1)
| lesseq(X0,sK1)
| ~ lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_20728,c_60]) ).
tcf(c_20976,plain,
! [X0: $i] :
( lesseq(sK0,sK2)
| lesseq(X0,sK1)
| ~ lesseq(X0,sK2) ),
inference(global_subsumption_just,[status(thm)],[c_17064,c_12250,c_14606]) ).
tcf(c_21723,plain,
! [X0: $i] :
( ( sK1 = X0 )
| ( sK1 != sK2 )
| ( X0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_1986]) ).
tcf(c_21724,plain,
( ( sK1 = sK0 )
| ( sK1 != sK2 )
| ( sK0 != sK2 ) ),
inference(instantiation,[status(thm)],[c_21723]) ).
tcf(c_21756,plain,
( lesseq(sK2,sK1)
| lesseq(sK0,sK1)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_20687,c_70]) ).
tcf(c_21761,plain,
( ( sK0 = sK2 )
| lesseq(sK0,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_21756,c_17237]) ).
tcf(c_21762,plain,
( lesseq(sK0,sK1)
| ( sK0 = sK2 ) ),
inference(renaming,[status(thm)],[c_21761]) ).
tcf(c_21779,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| ( sK0 = sK2 )
| ~ lesseq(sK1,X0) ),
inference(superposition,[status(thm)],[c_21762,c_60]) ).
tcf(c_21845,plain,
( lesseq(sK0,sK2)
| ( sK1 = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_20727,c_16945]) ).
tcf(c_21864,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| ( sK1 = sK2 )
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_21845,c_60]) ).
tcf(c_22508,plain,
! [X0: $i,X1: $i] :
( lesseq(X0,sK4(sK0,sK1,sK2))
| ~ ub(X0,X1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_22511,plain,
! [X0: $i,X1: $i] :
( lesseq(X1,sK4(sK0,sK1,sK2))
| ~ ub(X0,X1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_22516,plain,
( lesseq(sK2,sK4(sK0,sK1,sK2))
| ~ lesseq(sK2,sK1)
| ~ lesseq(sK1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_4461]) ).
tcf(c_22677,plain,
( lesseq(sK0,sK2)
| lesseq(sK0,sK1)
| ( sK1 = sK2 ) ),
inference(superposition,[status(thm)],[c_20705,c_21864]) ).
tcf(c_22809,plain,
( ( sK2 = sK1 )
| ( sK2 != sK2 )
| ( sK1 != sK2 ) ),
inference(instantiation,[status(thm)],[c_7519]) ).
tcf(c_22871,plain,
( lesseq(sK0,sK2)
| lesseq(sK0,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_22677,c_17231]) ).
tcf(c_22889,plain,
! [X0: $i] :
( lesseq(sK0,sK1)
| lesseq(sK0,X0)
| lesseq(X0,sK2) ),
inference(superposition,[status(thm)],[c_22871,c_1443]) ).
tcf(c_22890,plain,
! [X0: $i] :
( lesseq(sK0,sK1)
| lesseq(sK0,X0)
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_22871,c_60]) ).
tcf(c_23032,plain,
! [X0: $i,X1: $i] :
( lesseq(sK0,X1)
| lesseq(sK0,X0)
| lesseq(X1,sK1)
| lesseq(X0,sK2) ),
inference(superposition,[status(thm)],[c_22889,c_1443]) ).
tcf(c_23079,plain,
( lesseq(sK1,sK2)
| lesseq(sK0,sK1) ),
inference(equality_factoring,[status(thm)],[c_22889]) ).
tcf(c_23250,plain,
( lesseq(sK2,sK1)
| ~ lesseq(sK1,sK1)
| ( sK2 != sK1 )
| ( sK1 != sK1 ) ),
inference(instantiation,[status(thm)],[c_3945]) ).
tcf(c_23728,plain,
( lesseq(sK0,sK1)
| minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK0,max(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_1698,c_22890]) ).
tcf(c_24216,plain,
! [X0: $i] :
( lesseq(sK0,sK1)
| lesseq(sK1,X0)
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_23079,c_60]) ).
tcf(c_24668,plain,
( lesseq(sK0,sK1)
| minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK1,max(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_1698,c_24216]) ).
tcf(c_25964,plain,
! [X0: $i] :
( ub(sK0,sK1,max(X0,sK1))
| ~ lesseq(sK1,max(X0,sK1))
| ~ lesseq(sK0,max(X0,sK1)) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_25965,plain,
( ub(sK0,sK1,max(sK0,sK1))
| ~ lesseq(sK1,max(sK0,sK1))
| ~ lesseq(sK0,max(sK0,sK1)) ),
inference(instantiation,[status(thm)],[c_25964]) ).
tcf(c_26962,plain,
( lesseq(sK2,sK3(sK0,sK1,sK2))
| ~ lesseq(sK2,sK2)
| ( sK2 != sK2 )
| ( sK3(sK0,sK1,sK2) != sK2 ) ),
inference(instantiation,[status(thm)],[c_4704]) ).
tcf(c_28842,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| lesseq(X0,sK2)
| lesseq(X0,sK1) ),
inference(equality_factoring,[status(thm)],[c_23032]) ).
tcf(c_29227,plain,
! [X0: $i,X1: $i] :
( lesseq(sK0,X0)
| lesseq(X1,sK2)
| lesseq(X0,sK1)
| lesseq(X0,X1) ),
inference(superposition,[status(thm)],[c_28842,c_1443]) ).
tcf(c_29687,plain,
! [X0: $i] :
( ( sK3(sK0,sK1,sK2) = sK2 )
| ( sK2 != max(X0,sK1) )
| ( sK3(sK0,sK1,sK2) != max(X0,sK1) ) ),
inference(instantiation,[status(thm)],[c_12697]) ).
tcf(c_29704,plain,
( ( sK3(sK0,sK1,sK2) = sK2 )
| ( sK2 != max(sK0,sK1) )
| ( sK3(sK0,sK1,sK2) != max(sK0,sK1) ) ),
inference(instantiation,[status(thm)],[c_29687]) ).
tcf(c_31200,plain,
( lesseq(sK0,sK1)
| lesseq(sK0,max(sK0,sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_23728,c_72,c_81,c_1994,c_3600,c_5333]) ).
tcf(c_33170,plain,
( lesseq(sK0,sK1)
| lesseq(sK1,max(sK0,sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_24668,c_4894,c_5305,c_31200]) ).
tcf(c_35400,plain,
( lesseq(sK2,sK1)
| lesseq(sK2,sK0)
| lesseq(sK0,sK2) ),
inference(equality_factoring,[status(thm)],[c_29227]) ).
tcf(c_35405,plain,
! [X0: $i] :
( lesseq(sK1,sK2)
| lesseq(sK0,X0)
| lesseq(X0,sK1) ),
inference(equality_factoring,[status(thm)],[c_29227]) ).
tcf(c_36160,plain,
( lesseq(sK2,sK1)
| lesseq(sK2,sK0) ),
inference(global_subsumption_just,[status(thm)],[c_35400,c_1985,c_3160,c_4705,c_16516,c_22809,c_23250]) ).
tcf(c_36178,plain,
! [X0: $i] :
( lesseq(sK2,sK0)
| lesseq(sK2,X0)
| lesseq(X0,sK1) ),
inference(superposition,[status(thm)],[c_36160,c_1443]) ).
tcf(c_36653,plain,
! [X0: $i,X1: $i] :
( lesseq(sK1,X1)
| lesseq(sK0,X0)
| lesseq(X1,sK2)
| lesseq(X0,sK1) ),
inference(superposition,[status(thm)],[c_35405,c_1443]) ).
tcf(c_36688,plain,
! [X0: $i,X1: $i] :
( lesseq(sK1,sK2)
| lesseq(sK0,X1)
| lesseq(X1,X0)
| ~ lesseq(sK1,X0) ),
inference(superposition,[status(thm)],[c_35405,c_60]) ).
tcf(c_36997,plain,
! [X0: $i] :
( ( sK1 = sK2 )
| ( sK2 != max(X0,sK1) )
| ( sK1 != max(X0,sK1) ) ),
inference(instantiation,[status(thm)],[c_12697]) ).
tcf(c_37001,plain,
( ( sK1 = sK2 )
| ( sK2 != max(sK0,sK1) )
| ( sK1 != max(sK0,sK1) ) ),
inference(instantiation,[status(thm)],[c_36997]) ).
tcf(c_37427,plain,
! [X0: $i] :
( lesseq(sK2,sK0)
| lesseq(sK2,X0)
| ( max(X0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_36178,c_66]) ).
tcf(c_38164,plain,
! [X0: $i,X1: $i] :
( ub(X0,X1,sK4(sK0,sK1,sK2))
| ~ model_ub(X0,X1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_43884,plain,
( lesseq(sK2,sK1)
| lesseq(sK1,sK0)
| lesseq(sK0,sK2) ),
inference(equality_factoring,[status(thm)],[c_36653]) ).
tcf(c_44259,plain,
( lesseq(sK2,sK1)
| lesseq(sK1,sK0) ),
inference(global_subsumption_just,[status(thm)],[c_43884,c_1985,c_1994,c_2801,c_3160,c_3242,c_4705,c_10605,c_16083,c_22809,c_23250,c_37001]) ).
tcf(c_44276,plain,
( lesseq(sK1,sK0)
| ( sK1 = sK2 )
| ~ lesseq(sK1,sK2) ),
inference(superposition,[status(thm)],[c_44259,c_68]) ).
tcf(c_45496,plain,
( lesseq(sK1,sK0)
| ( sK1 = sK2 ) ),
inference(global_subsumption_just,[status(thm)],[c_44276,c_1985,c_1994,c_2801,c_3242,c_4705,c_10605,c_16083,c_37001]) ).
tcf(c_45512,plain,
( ( sK1 = sK2 )
| ( sK0 = sK1 )
| ~ lesseq(sK0,sK1) ),
inference(superposition,[status(thm)],[c_45496,c_68]) ).
tcf(c_47076,plain,
( lesseq(sK2,sK0)
| ( max(sK0,sK1) = sK1 ) ),
inference(equality_factoring,[status(thm)],[c_37427]) ).
tcf(c_53375,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| lesseq(X0,sK2)
| lesseq(X0,sK1) ),
inference(equality_factoring,[status(thm)],[c_17675]) ).
tcf(c_54585,plain,
! [X0: $i] :
( lesseq(sK0,sK2)
| lesseq(sK0,X0)
| lesseq(X0,sK1) ),
inference(superposition,[status(thm)],[c_53375,c_20976]) ).
tcf(c_56608,plain,
( ( sK1 = sK2 )
| ~ lesseq(sK0,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_45512,c_1985,c_2801,c_3242,c_4705,c_10605,c_16083,c_37001]) ).
tcf(c_57785,plain,
( ub(sK0,sK1,sK4(sK0,sK1,sK2))
| ~ model_ub(sK0,sK1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_38164]) ).
tcf(c_60941,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK1,max(sK0,sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_19008,c_72,c_75,c_80,c_81,c_1684,c_4705,c_7520,c_16427,c_18351,c_21724,c_33170,c_56608]) ).
tcf(c_60979,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK0,max(sK0,sK1))
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_60941,c_21779]) ).
tcf(c_61811,plain,
lesseq(sK0,sK2),
inference(global_subsumption_just,[status(thm)],[c_20833,c_72,c_81,c_508,c_519,c_1457,c_1560,c_2637,c_2638,c_3102,c_4705,c_6010,c_7192,c_7787,c_10605,c_12704,c_19363,c_26962,c_29704,c_60979]) ).
tcf(c_61826,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_61811,c_60]) ).
tcf(c_61828,plain,
max(sK0,sK2) = sK2,
inference(superposition,[status(thm)],[c_61811,c_66]) ).
tcf(c_62014,plain,
model_max(sK0,sK2,sK2),
inference(superposition,[status(thm)],[c_61828,c_62]) ).
tcf(c_62139,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK0,max(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_1698,c_61826]) ).
tcf(c_65397,plain,
lesseq(sK0,sK2),
inference(global_subsumption_just,[status(thm)],[c_54585,c_61811]) ).
tcf(c_65402,plain,
! [X0: $i] :
( lesseq(sK0,X0)
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_65397,c_60]) ).
tcf(c_65545,plain,
( minsol_model_ub(sK0,sK1,sK2)
| lesseq(sK0,max(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_16217,c_65402]) ).
tcf(c_66135,plain,
( lesseq(sK0,sK1)
| minsol_model_ub(sK0,sK1,sK2)
| ( sK0 = sK2 ) ),
inference(superposition,[status(thm)],[c_16592,c_65545]) ).
tcf(c_73731,plain,
! [X0: $i] :
( lesseq(sK1,sK4(sK0,sK1,sK2))
| ~ ub(X0,sK1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_22511]) ).
tcf(c_73732,plain,
! [X0: $i] :
( lesseq(X0,sK4(sK0,sK1,sK2))
| ~ ub(X0,sK1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_22508]) ).
tcf(c_73734,plain,
( lesseq(sK0,sK4(sK0,sK1,sK2))
| ~ ub(sK0,sK1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_73732]) ).
tcf(c_73735,plain,
( lesseq(sK1,sK4(sK0,sK1,sK2))
| ~ ub(sK0,sK1,sK4(sK0,sK1,sK2)) ),
inference(instantiation,[status(thm)],[c_73731]) ).
tcf(c_74495,plain,
minsol_model_ub(sK0,sK1,sK2),
inference(global_subsumption_just,[status(thm)],[c_66135,c_1658,c_1659,c_1732,c_4464,c_4705,c_7070,c_7211,c_10605,c_12928,c_22516,c_25965,c_36160,c_57785,c_60941,c_62139,c_73734,c_73735]) ).
tcf(c_76983,plain,
lesseq(sK1,sK2),
inference(global_subsumption_just,[status(thm)],[c_36688,c_508,c_519,c_1456,c_1658,c_1659,c_1732,c_2637,c_2638,c_3102,c_4464,c_4705,c_6010,c_7070,c_7192,c_7211,c_7787,c_10605,c_12928,c_22516,c_25965,c_26962,c_29704,c_36160,c_57785,c_60941,c_62139,c_73734,c_73735]) ).
tcf(c_76999,plain,
! [X0: $i] :
( lesseq(sK1,X0)
| ~ lesseq(sK2,X0) ),
inference(superposition,[status(thm)],[c_76983,c_60]) ).
tcf(c_77289,plain,
( lesseq(sK1,sK0)
| ( max(sK0,sK1) = sK1 ) ),
inference(superposition,[status(thm)],[c_47076,c_76999]) ).
tcf(c_79252,plain,
max(sK0,sK1) = sK1,
inference(global_subsumption_just,[status(thm)],[c_77289,c_508,c_519,c_1658,c_1659,c_1732,c_2637,c_2638,c_3102,c_4464,c_4705,c_6010,c_7070,c_7192,c_7211,c_7787,c_10605,c_12928,c_20530,c_22516,c_25965,c_26962,c_29704,c_36160,c_57785,c_60941,c_62139,c_73734,c_73735]) ).
tcf(c_79284,plain,
sK1 = sK2,
inference(demodulation,[status(thm)],[c_18540,c_79252]) ).
tcf(c_79402,plain,
model_max(sK0,sK1,sK1),
inference(demodulation,[status(thm)],[c_62014,c_79284]) ).
tcf(c_96390,plain,
~ model_max(sK0,sK1,sK2),
inference(global_subsumption_just,[status(thm)],[c_508,c_508,c_519,c_2637,c_2638,c_3102,c_4705,c_6010,c_7192,c_7787,c_10605,c_26962,c_29704,c_74495]) ).
tcf(c_96392,plain,
~ model_max(sK0,sK1,sK1),
inference(light_normalisation,[status(thm)],[c_96390,c_79284]) ).
tcf(c_96393,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_96392,c_79402]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM858+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 05:35:28 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 9.17/4.27 % SZS status Started for theBenchmark.p
% 9.17/4.27 % SZS status Theorem for theBenchmark.p
% 9.17/4.27
% 9.17/4.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 9.17/4.27
% 9.17/4.27 % ------ iProver source info
% 9.17/4.27
% 9.17/4.27 % git: date: 2026-07-19 20:42:38 +0200
% 9.17/4.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 9.17/4.27 % git: non_committed_changes: false
% 9.17/4.27
% 9.17/4.27 % ------ Parsing...
% 9.17/4.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 9.17/4.27
% 9.17/4.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e %
% 9.17/4.27
% 9.17/4.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 9.17/4.27
% 9.17/4.27 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 9.17/4.27 % ------ Proving...
% 9.17/4.27 % ------ Problem Properties
% 9.17/4.27
% 9.17/4.27 %
% 9.17/4.27 % clauses 23
% 9.17/4.27 % conjectures 0
% 9.17/4.27 % EPR 13
% 9.17/4.27 % Horn 18
% 9.17/4.27 % unary 2
% 9.17/4.27 % binary 10
% 9.17/4.27 % lits 57
% 9.17/4.27 % lits eq 4
% 9.17/4.27 % fd_pure 0
% 9.17/4.27 % fd_pseudo 0
% 9.17/4.27 % fd_cond 0
% 9.17/4.27 % fd_pseudo_cond 2
% 9.17/4.27 % AC symbols 0
% 9.17/4.27
% 9.17/4.27 % ------ Schedule dynamic 5 is on
% 9.17/4.27
% 9.17/4.27 % ------ no conjectures: strip conj schedule
% 9.17/4.27
% 9.17/4.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 9.17/4.27
% 9.17/4.27
% 9.17/4.27 % ------
% 9.17/4.27 % Current options:
% 9.17/4.27 % ------
% 9.17/4.27
% 9.17/4.27
% 9.17/4.27 %
% 9.17/4.27
% 9.17/4.27 % ------ Proving...
% 9.17/4.27 %
% 9.17/4.27
% 9.17/4.27 % SZS status Theorem for theBenchmark.p
% 9.17/4.27
% 9.17/4.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 9.17/4.28
% 9.17/4.28
%------------------------------------------------------------------------------