%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV036+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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 03:16:16 PM UTC 2026
% Result : Theorem 8.60s 1.74s
% Output : CNFRefutation 8.60s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f362ERROR: Could not build tree for root c_22639ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( X0 = X1
| gt(X1,X0)
| gt(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',totality) ).
fof(f3,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( leq(X1,X2)
& leq(X0,X1) )
=> leq(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',transitivity_leq) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(f53,conjecture,
( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X3] :
( ( leq(X3,n2)
& leq(n0,X3) )
=> a_select2(s_center7_init,X3) = init )
& ! [X2] :
( ( leq(X2,n3)
& leq(n0,X2) )
=> a_select2(s_values7_init,X2) = init )
& ! [X0] :
( ( leq(X0,n2)
& leq(n0,X0) )
=> ! [X1] :
( ( leq(X1,n3)
& leq(n0,X1) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n2,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init )
=> ( ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X19] :
( ( leq(X19,n2)
& leq(n0,X19) )
=> a_select2(s_center7_init,X19) = init )
& ! [X18] :
( ( leq(X18,n3)
& leq(n0,X18) )
=> a_select2(s_values7_init,X18) = init )
& ! [X16] :
( ( leq(X16,n2)
& leq(n0,X16) )
=> ! [X17] :
( ( leq(X17,n3)
& leq(n0,X17) )
=> a_select3(simplex7_init,X17,X16) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(n0,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& s_worst7_init = init
& s_sworst7_init = init
& init = init ) )
& ( ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X15] :
( ( leq(X15,n2)
& leq(n0,X15) )
=> a_select2(s_center7_init,X15) = init )
& ! [X14] :
( ( leq(X14,n3)
& leq(n0,X14) )
=> a_select2(s_values7_init,X14) = init )
& ! [X12] :
( ( leq(X12,n2)
& leq(n0,X12) )
=> ! [X13] :
( ( leq(X13,n3)
& leq(n0,X13) )
=> a_select3(simplex7_init,X13,X12) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_best7,n3)
& leq(n0,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_best7_init = init
& init = init ) )
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X11] :
( ( leq(X11,n2)
& leq(n0,X11) )
=> a_select2(s_center7_init,X11) = init )
& ! [X10] :
( ( leq(X10,n3)
& leq(n0,X10) )
=> a_select2(s_values7_init,X10) = init )
& ! [X8] :
( ( leq(X8,n2)
& leq(n0,X8) )
=> ! [X9] :
( ( leq(X9,n3)
& leq(n0,X9) )
=> a_select3(simplex7_init,X9,X8) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_best7,n3)
& leq(n0,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_best7_init = init
& init = init ) )
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X7] :
( ( leq(X7,n2)
& leq(n0,X7) )
=> a_select2(s_center7_init,X7) = init )
& ! [X6] :
( ( leq(X6,n3)
& leq(n0,X6) )
=> a_select2(s_values7_init,X6) = init )
& ! [X4] :
( ( leq(X4,n2)
& leq(n0,X4) )
=> ! [X5] :
( ( leq(X5,n3)
& leq(n0,X5) )
=> a_select3(simplex7_init,X5,X4) = init ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ) )
& a_select2(s_values7_init,pv1388) = init
& a_select2(s_values7_init,s_sworst7) = init
& s_sworst7_init = init
& init = init ) )
& a_select2(s_values7_init,pv1388) = init
& a_select2(s_values7_init,s_worst7) = init
& s_worst7_init = init
& init = init ) )
& a_select2(s_values7_init,pv1388) = init
& a_select2(s_values7_init,s_best7) = init
& s_best7_init = init
& init = init ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gauss_init_0057) ).
fof(f54,negated_conjecture,
~ ( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X3] :
( ( leq(X3,n2)
& leq(n0,X3) )
=> a_select2(s_center7_init,X3) = init )
& ! [X2] :
( ( leq(X2,n3)
& leq(n0,X2) )
=> a_select2(s_values7_init,X2) = init )
& ! [X0] :
( ( leq(X0,n2)
& leq(n0,X0) )
=> ! [X1] :
( ( leq(X1,n3)
& leq(n0,X1) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n2,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init )
=> ( ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X19] :
( ( leq(X19,n2)
& leq(n0,X19) )
=> a_select2(s_center7_init,X19) = init )
& ! [X18] :
( ( leq(X18,n3)
& leq(n0,X18) )
=> a_select2(s_values7_init,X18) = init )
& ! [X16] :
( ( leq(X16,n2)
& leq(n0,X16) )
=> ! [X17] :
( ( leq(X17,n3)
& leq(n0,X17) )
=> a_select3(simplex7_init,X17,X16) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(n0,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& s_worst7_init = init
& s_sworst7_init = init
& init = init ) )
& ( ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X15] :
( ( leq(X15,n2)
& leq(n0,X15) )
=> a_select2(s_center7_init,X15) = init )
& ! [X14] :
( ( leq(X14,n3)
& leq(n0,X14) )
=> a_select2(s_values7_init,X14) = init )
& ! [X12] :
( ( leq(X12,n2)
& leq(n0,X12) )
=> ! [X13] :
( ( leq(X13,n3)
& leq(n0,X13) )
=> a_select3(simplex7_init,X13,X12) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_best7,n3)
& leq(n0,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_best7_init = init
& init = init ) )
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X11] :
( ( leq(X11,n2)
& leq(n0,X11) )
=> a_select2(s_center7_init,X11) = init )
& ! [X10] :
( ( leq(X10,n3)
& leq(n0,X10) )
=> a_select2(s_values7_init,X10) = init )
& ! [X8] :
( ( leq(X8,n2)
& leq(n0,X8) )
=> ! [X9] :
( ( leq(X9,n3)
& leq(n0,X9) )
=> a_select3(simplex7_init,X9,X8) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_best7,n3)
& leq(n0,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_best7_init = init
& init = init ) )
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X7] :
( ( leq(X7,n2)
& leq(n0,X7) )
=> a_select2(s_center7_init,X7) = init )
& ! [X6] :
( ( leq(X6,n3)
& leq(n0,X6) )
=> a_select2(s_values7_init,X6) = init )
& ! [X4] :
( ( leq(X4,n2)
& leq(n0,X4) )
=> ! [X5] :
( ( leq(X5,n3)
& leq(n0,X5) )
=> a_select3(simplex7_init,X5,X4) = init ) )
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init ) )
& a_select2(s_values7_init,pv1388) = init
& a_select2(s_values7_init,s_sworst7) = init
& s_sworst7_init = init
& init = init ) )
& a_select2(s_values7_init,pv1388) = init
& a_select2(s_values7_init,s_worst7) = init
& s_worst7_init = init
& init = init ) )
& a_select2(s_values7_init,pv1388) = init
& a_select2(s_values7_init,s_best7) = init
& s_best7_init = init
& init = init ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f65,axiom,
gt(n2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_0) ).
fof(f87,plain,
( ( ~ gt(loopcounter,n1)
| ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X3] :
( ~ leq(X3,n2)
| ~ leq(n0,X3)
| a_select2(s_center7_init,X3) = init )
& ! [X2] :
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| a_select2(s_values7_init,X2) = init )
& ! [X0] :
( ~ leq(X0,n2)
| ~ leq(n0,X0)
| ! [X1] :
( ~ leq(X1,n3)
| ~ leq(n0,X1)
| a_select3(simplex7_init,X1,X0) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n2,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init
& ( ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X19] :
( leq(X19,n2)
& leq(n0,X19)
& init != a_select2(s_center7_init,X19) )
| ? [X18] :
( leq(X18,n3)
& leq(n0,X18)
& init != a_select2(s_values7_init,X18) )
| ? [X16] :
( leq(X16,n2)
& leq(n0,X16)
& ? [X17] :
( leq(X17,n3)
& leq(n0,X17)
& init != a_select3(simplex7_init,X17,X16) ) )
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| init != s_worst7_init
| init != s_sworst7_init
| init != init ) )
| ( ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X15] :
( leq(X15,n2)
& leq(n0,X15)
& init != a_select2(s_center7_init,X15) )
| ? [X14] :
( leq(X14,n3)
& leq(n0,X14)
& init != a_select2(s_values7_init,X14) )
| ? [X12] :
( leq(X12,n2)
& leq(n0,X12)
& ? [X13] :
( leq(X13,n3)
& leq(n0,X13)
& init != a_select3(simplex7_init,X13,X12) ) )
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| s_best7_init != init
| init != init ) )
| ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
& ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X11] :
( leq(X11,n2)
& leq(n0,X11)
& init != a_select2(s_center7_init,X11) )
| ? [X10] :
( leq(X10,n3)
& leq(n0,X10)
& init != a_select2(s_values7_init,X10) )
| ? [X8] :
( leq(X8,n2)
& leq(n0,X8)
& ? [X9] :
( leq(X9,n3)
& leq(n0,X9)
& init != a_select3(simplex7_init,X9,X8) ) )
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| s_best7_init != init
| init != init ) )
| ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X7] :
( leq(X7,n2)
& leq(n0,X7)
& init != a_select2(s_center7_init,X7) )
| ? [X6] :
( leq(X6,n3)
& leq(n0,X6)
& init != a_select2(s_values7_init,X6) )
| ? [X4] :
( leq(X4,n2)
& leq(n0,X4)
& ? [X5] :
( leq(X5,n3)
& leq(n0,X5)
& init != a_select3(simplex7_init,X5,X4) ) )
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| init != s_sworst7_init
| s_best7_init != init ) )
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_sworst7)
| init != s_sworst7_init
| init != init ) )
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_worst7)
| init != s_worst7_init
| init != init ) )
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_best7)
| s_best7_init != init
| init != init ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f88,plain,
( ( ~ gt(loopcounter,n1)
| ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X3] :
( ~ leq(X3,n2)
| ~ leq(n0,X3)
| a_select2(s_center7_init,X3) = init )
& ! [X2] :
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| a_select2(s_values7_init,X2) = init )
& ! [X0] :
( ~ leq(X0,n2)
| ~ leq(n0,X0)
| ! [X1] :
( ~ leq(X1,n3)
| ~ leq(n0,X1)
| a_select3(simplex7_init,X1,X0) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n2,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init
& ( ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X19] :
( leq(X19,n2)
& leq(n0,X19)
& init != a_select2(s_center7_init,X19) )
| ? [X18] :
( leq(X18,n3)
& leq(n0,X18)
& init != a_select2(s_values7_init,X18) )
| ? [X16] :
( leq(X16,n2)
& leq(n0,X16)
& ? [X17] :
( leq(X17,n3)
& leq(n0,X17)
& init != a_select3(simplex7_init,X17,X16) ) )
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| init != s_worst7_init
| init != s_sworst7_init
| init != init ) )
| ( ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X15] :
( leq(X15,n2)
& leq(n0,X15)
& init != a_select2(s_center7_init,X15) )
| ? [X14] :
( leq(X14,n3)
& leq(n0,X14)
& init != a_select2(s_values7_init,X14) )
| ? [X12] :
( leq(X12,n2)
& leq(n0,X12)
& ? [X13] :
( leq(X13,n3)
& leq(n0,X13)
& init != a_select3(simplex7_init,X13,X12) ) )
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| s_best7_init != init
| init != init ) )
| ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
& ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X11] :
( leq(X11,n2)
& leq(n0,X11)
& init != a_select2(s_center7_init,X11) )
| ? [X10] :
( leq(X10,n3)
& leq(n0,X10)
& init != a_select2(s_values7_init,X10) )
| ? [X8] :
( leq(X8,n2)
& leq(n0,X8)
& ? [X9] :
( leq(X9,n3)
& leq(n0,X9)
& init != a_select3(simplex7_init,X9,X8) ) )
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| s_best7_init != init
| init != init ) )
| ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| ? [X7] :
( leq(X7,n2)
& leq(n0,X7)
& init != a_select2(s_center7_init,X7) )
| ? [X6] :
( leq(X6,n3)
& leq(n0,X6)
& init != a_select2(s_values7_init,X6) )
| ? [X4] :
( leq(X4,n2)
& leq(n0,X4)
& ? [X5] :
( leq(X5,n3)
& leq(n0,X5)
& init != a_select3(simplex7_init,X5,X4) ) )
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| init != s_sworst7_init
| s_best7_init != init ) )
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_sworst7)
| init != s_sworst7_init
| init != init ) )
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_worst7)
| init != s_worst7_init
| init != init ) )
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_best7)
| s_best7_init != init
| init != init ) ),
inference(flattening,[],[f87]) ).
fof(f94,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(flattening,[],[f98]) ).
fof(f131,plain,
( ~ sP7
| ? [X7] :
( leq(X7,n2)
& leq(n0,X7)
& init != a_select2(s_center7_init,X7) ) ),
inference(nnf_transformation,[],[f117]) ).
fof(f132,plain,
( ~ sP7
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& init != a_select2(s_center7_init,X0) ) ),
inference(rectify,[],[f131]) ).
fof(f133,plain,
( ~ sP7
| ( leq(sK14,n2)
& leq(n0,sK14)
& init != a_select2(s_center7_init,sK14) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X0,sK14)],[f132]) ).
fof(f134,plain,
( ~ sP6
| ? [X4] :
( leq(X4,n2)
& leq(n0,X4)
& ? [X5] :
( leq(X5,n3)
& leq(n0,X5)
& init != a_select3(simplex7_init,X5,X4) ) ) ),
inference(nnf_transformation,[],[f116]) ).
fof(f135,plain,
( ~ sP6
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& ? [X1] :
( leq(X1,n3)
& leq(n0,X1)
& init != a_select3(simplex7_init,X1,X0) ) ) ),
inference(rectify,[],[f134]) ).
fof(f136,plain,
( ~ sP6
| ( leq(sK15,n2)
& leq(n0,sK15)
& leq(sK16,n3)
& leq(n0,sK16)
& init != a_select3(simplex7_init,sK16,sK15) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X0,sK15),skolemize(X1,sK16)],[f135]) ).
fof(f137,plain,
( ~ sP5
| ? [X11] :
( leq(X11,n2)
& leq(n0,X11)
& init != a_select2(s_center7_init,X11) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f138,plain,
( ~ sP5
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& init != a_select2(s_center7_init,X0) ) ),
inference(rectify,[],[f137]) ).
fof(f139,plain,
( ~ sP5
| ( leq(sK17,n2)
& leq(n0,sK17)
& init != a_select2(s_center7_init,sK17) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X0,sK17)],[f138]) ).
fof(f140,plain,
( ~ sP4
| ? [X8] :
( leq(X8,n2)
& leq(n0,X8)
& ? [X9] :
( leq(X9,n3)
& leq(n0,X9)
& init != a_select3(simplex7_init,X9,X8) ) ) ),
inference(nnf_transformation,[],[f114]) ).
fof(f141,plain,
( ~ sP4
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& ? [X1] :
( leq(X1,n3)
& leq(n0,X1)
& init != a_select3(simplex7_init,X1,X0) ) ) ),
inference(rectify,[],[f140]) ).
fof(f142,plain,
( ~ sP4
| ( leq(sK18,n2)
& leq(n0,sK18)
& leq(sK19,n3)
& leq(n0,sK19)
& init != a_select3(simplex7_init,sK19,sK18) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19]),skolemize(X0,sK18),skolemize(X1,sK19)],[f141]) ).
fof(f143,plain,
( ~ sP3
| ? [X15] :
( leq(X15,n2)
& leq(n0,X15)
& init != a_select2(s_center7_init,X15) ) ),
inference(nnf_transformation,[],[f113]) ).
fof(f144,plain,
( ~ sP3
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& init != a_select2(s_center7_init,X0) ) ),
inference(rectify,[],[f143]) ).
fof(f145,plain,
( ~ sP3
| ( leq(sK20,n2)
& leq(n0,sK20)
& init != a_select2(s_center7_init,sK20) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X0,sK20)],[f144]) ).
fof(f146,plain,
( ~ sP2
| ? [X12] :
( leq(X12,n2)
& leq(n0,X12)
& ? [X13] :
( leq(X13,n3)
& leq(n0,X13)
& init != a_select3(simplex7_init,X13,X12) ) ) ),
inference(nnf_transformation,[],[f112]) ).
fof(f147,plain,
( ~ sP2
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& ? [X1] :
( leq(X1,n3)
& leq(n0,X1)
& init != a_select3(simplex7_init,X1,X0) ) ) ),
inference(rectify,[],[f146]) ).
fof(f148,plain,
( ~ sP2
| ( leq(sK21,n2)
& leq(n0,sK21)
& leq(sK22,n3)
& leq(n0,sK22)
& init != a_select3(simplex7_init,sK22,sK21) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22]),skolemize(X0,sK21),skolemize(X1,sK22)],[f147]) ).
fof(f149,plain,
( ~ sP1
| ? [X19] :
( leq(X19,n2)
& leq(n0,X19)
& init != a_select2(s_center7_init,X19) ) ),
inference(nnf_transformation,[],[f111]) ).
fof(f150,plain,
( ~ sP1
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& init != a_select2(s_center7_init,X0) ) ),
inference(rectify,[],[f149]) ).
fof(f151,plain,
( ~ sP1
| ( leq(sK23,n2)
& leq(n0,sK23)
& init != a_select2(s_center7_init,sK23) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(X0,sK23)],[f150]) ).
fof(f155,plain,
( ( ~ gt(loopcounter,n1)
| ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X4] :
( ~ leq(X4,n2)
| ~ leq(n0,X4)
| init = a_select2(s_center7_init,X4) )
& ! [X3] :
( ~ leq(X3,n3)
| ~ leq(n0,X3)
| init = a_select2(s_values7_init,X3) )
& ! [X1] :
( ~ leq(X1,n2)
| ~ leq(n0,X1)
| ! [X2] :
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| init = a_select3(simplex7_init,X2,X1) ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n2,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init
& ( ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| sP1
| ? [X0] :
( leq(X0,n3)
& leq(n0,X0)
& init != a_select2(s_values7_init,X0) )
| sP0
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| init != s_worst7_init
| init != s_sworst7_init
| init != init ) )
| sP10
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_best7)
| s_best7_init != init
| init != init ) ),
inference(rectify,[],[f121]) ).
fof(f156,plain,
( ( ~ gt(loopcounter,n1)
| ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X4] :
( ~ leq(X4,n2)
| ~ leq(n0,X4)
| init = a_select2(s_center7_init,X4) )
& ! [X3] :
( ~ leq(X3,n3)
| ~ leq(n0,X3)
| init = a_select2(s_values7_init,X3) )
& ! [X1] :
( ~ leq(X1,n2)
| ~ leq(n0,X1)
| ! [X2] :
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| init = a_select3(simplex7_init,X2,X1) ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n2,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init
& ( ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| sP1
| ( leq(sK26,n3)
& leq(n0,sK26)
& init != a_select2(s_values7_init,sK26) )
| sP0
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| init != s_worst7_init
| init != s_sworst7_init
| init != init ) )
| sP10
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_best7)
| s_best7_init != init
| init != init ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(X0,sK26)],[f155]) ).
fof(f182,plain,
( ~ sP7
| leq(sK14,n2) ),
inference(cnf_transformation,[],[f133]) ).
fof(f183,plain,
( ~ sP7
| leq(n0,sK14) ),
inference(cnf_transformation,[],[f133]) ).
fof(f184,plain,
( ~ sP7
| init != a_select2(s_center7_init,sK14) ),
inference(cnf_transformation,[],[f133]) ).
fof(f185,plain,
( ~ sP6
| leq(sK15,n2) ),
inference(cnf_transformation,[],[f136]) ).
fof(f186,plain,
( ~ sP6
| leq(n0,sK15) ),
inference(cnf_transformation,[],[f136]) ).
fof(f187,plain,
( ~ sP6
| leq(sK16,n3) ),
inference(cnf_transformation,[],[f136]) ).
fof(f188,plain,
( ~ sP6
| leq(n0,sK16) ),
inference(cnf_transformation,[],[f136]) ).
fof(f189,plain,
( ~ sP6
| init != a_select3(simplex7_init,sK16,sK15) ),
inference(cnf_transformation,[],[f136]) ).
fof(f190,plain,
( ~ sP5
| leq(sK17,n2) ),
inference(cnf_transformation,[],[f139]) ).
fof(f191,plain,
( ~ sP5
| leq(n0,sK17) ),
inference(cnf_transformation,[],[f139]) ).
fof(f192,plain,
( ~ sP5
| init != a_select2(s_center7_init,sK17) ),
inference(cnf_transformation,[],[f139]) ).
fof(f193,plain,
( ~ sP4
| leq(sK18,n2) ),
inference(cnf_transformation,[],[f142]) ).
fof(f194,plain,
( ~ sP4
| leq(n0,sK18) ),
inference(cnf_transformation,[],[f142]) ).
fof(f195,plain,
( ~ sP4
| leq(sK19,n3) ),
inference(cnf_transformation,[],[f142]) ).
fof(f196,plain,
( ~ sP4
| leq(n0,sK19) ),
inference(cnf_transformation,[],[f142]) ).
fof(f197,plain,
( ~ sP4
| init != a_select3(simplex7_init,sK19,sK18) ),
inference(cnf_transformation,[],[f142]) ).
fof(f198,plain,
( ~ sP3
| leq(sK20,n2) ),
inference(cnf_transformation,[],[f145]) ).
fof(f199,plain,
( ~ sP3
| leq(n0,sK20) ),
inference(cnf_transformation,[],[f145]) ).
fof(f200,plain,
( ~ sP3
| init != a_select2(s_center7_init,sK20) ),
inference(cnf_transformation,[],[f145]) ).
fof(f201,plain,
( ~ sP2
| leq(sK21,n2) ),
inference(cnf_transformation,[],[f148]) ).
fof(f202,plain,
( ~ sP2
| leq(n0,sK21) ),
inference(cnf_transformation,[],[f148]) ).
fof(f203,plain,
( ~ sP2
| leq(sK22,n3) ),
inference(cnf_transformation,[],[f148]) ).
fof(f204,plain,
( ~ sP2
| leq(n0,sK22) ),
inference(cnf_transformation,[],[f148]) ).
fof(f205,plain,
( ~ sP2
| init != a_select3(simplex7_init,sK22,sK21) ),
inference(cnf_transformation,[],[f148]) ).
fof(f206,plain,
( ~ sP1
| leq(sK23,n2) ),
inference(cnf_transformation,[],[f151]) ).
fof(f207,plain,
( ~ sP1
| leq(n0,sK23) ),
inference(cnf_transformation,[],[f151]) ).
fof(f208,plain,
( ~ sP1
| init != a_select2(s_center7_init,sK23) ),
inference(cnf_transformation,[],[f151]) ).
fof(f214,plain,
( ~ gt(loopcounter,n1)
| init = pvar1402_init ),
inference(cnf_transformation,[],[f156]) ).
fof(f215,plain,
( ~ gt(loopcounter,n1)
| init = pvar1401_init ),
inference(cnf_transformation,[],[f156]) ).
fof(f216,plain,
( ~ gt(loopcounter,n1)
| init = pvar1400_init ),
inference(cnf_transformation,[],[f156]) ).
fof(f217,plain,
! [X4] :
( ~ leq(X4,n2)
| ~ leq(n0,X4)
| init = a_select2(s_center7_init,X4) ),
inference(cnf_transformation,[],[f156]) ).
fof(f218,plain,
! [X3] :
( ~ leq(X3,n3)
| ~ leq(n0,X3)
| init = a_select2(s_values7_init,X3) ),
inference(cnf_transformation,[],[f156]) ).
fof(f219,plain,
! [X2,X1] :
( ~ leq(X1,n2)
| ~ leq(n0,X1)
| ~ leq(X2,n3)
| ~ leq(n0,X2)
| init = a_select3(simplex7_init,X2,X1) ),
inference(cnf_transformation,[],[f156]) ).
fof(f220,plain,
leq(pv1388,n3),
inference(cnf_transformation,[],[f156]) ).
fof(f221,plain,
leq(s_worst7,n3),
inference(cnf_transformation,[],[f156]) ).
fof(f222,plain,
leq(s_sworst7,n3),
inference(cnf_transformation,[],[f156]) ).
fof(f223,plain,
leq(s_best7,n3),
inference(cnf_transformation,[],[f156]) ).
fof(f224,plain,
leq(n2,pv1388),
inference(cnf_transformation,[],[f156]) ).
fof(f225,plain,
leq(n0,s_worst7),
inference(cnf_transformation,[],[f156]) ).
fof(f226,plain,
leq(n0,s_sworst7),
inference(cnf_transformation,[],[f156]) ).
fof(f227,plain,
leq(n0,s_best7),
inference(cnf_transformation,[],[f156]) ).
fof(f228,plain,
init = s_worst7_init,
inference(cnf_transformation,[],[f156]) ).
fof(f229,plain,
init = s_sworst7_init,
inference(cnf_transformation,[],[f156]) ).
fof(f240,plain,
! [X0,X1] :
( X0 = X1
| gt(X1,X0)
| gt(X0,X1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f245,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f246,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f251,plain,
! [X2,X0,X1] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f267,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f65]) ).
fof(f316,plain,
( ~ sP7
| s_sworst7_init != a_select2(s_center7_init,sK14) ),
inference(definition_unfolding,[],[f184,f229]) ).
fof(f317,plain,
( ~ sP6
| s_sworst7_init != a_select3(simplex7_init,sK16,sK15) ),
inference(definition_unfolding,[],[f189,f229]) ).
fof(f318,plain,
( ~ sP5
| s_sworst7_init != a_select2(s_center7_init,sK17) ),
inference(definition_unfolding,[],[f192,f229]) ).
fof(f319,plain,
( ~ sP4
| s_sworst7_init != a_select3(simplex7_init,sK19,sK18) ),
inference(definition_unfolding,[],[f197,f229]) ).
fof(f320,plain,
( ~ sP3
| s_sworst7_init != a_select2(s_center7_init,sK20) ),
inference(definition_unfolding,[],[f200,f229]) ).
fof(f321,plain,
( ~ sP2
| s_sworst7_init != a_select3(simplex7_init,sK22,sK21) ),
inference(definition_unfolding,[],[f205,f229]) ).
fof(f322,plain,
( ~ sP1
| s_sworst7_init != a_select2(s_center7_init,sK23) ),
inference(definition_unfolding,[],[f208,f229]) ).
fof(f331,plain,
s_sworst7_init = s_worst7_init,
inference(definition_unfolding,[],[f228,f229]) ).
fof(f332,plain,
! [X2,X1] :
( ~ leq(X1,n2)
| ~ leq(n0,X1)
| ~ leq(X2,n3)
| ~ leq(n0,X2)
| s_sworst7_init = a_select3(simplex7_init,X2,X1) ),
inference(definition_unfolding,[],[f219,f229]) ).
fof(f333,plain,
! [X3] :
( ~ leq(X3,n3)
| ~ leq(n0,X3)
| s_sworst7_init = a_select2(s_values7_init,X3) ),
inference(definition_unfolding,[],[f218,f229]) ).
fof(f334,plain,
! [X4] :
( ~ leq(X4,n2)
| ~ leq(n0,X4)
| s_sworst7_init = a_select2(s_center7_init,X4) ),
inference(definition_unfolding,[],[f217,f229]) ).
fof(f335,plain,
( ~ gt(loopcounter,n1)
| s_sworst7_init = pvar1400_init ),
inference(definition_unfolding,[],[f216,f229]) ).
fof(f336,plain,
( ~ gt(loopcounter,n1)
| s_sworst7_init = pvar1401_init ),
inference(definition_unfolding,[],[f215,f229]) ).
fof(f337,plain,
( ~ gt(loopcounter,n1)
| s_sworst7_init = pvar1402_init ),
inference(definition_unfolding,[],[f214,f229]) ).
tcf(c_49,negated_conjecture,
( sP3
| sP2
| sP9
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK11) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_50,negated_conjecture,
( sP3
| sP2
| sP9
| gt(loopcounter,n1)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK11) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f361]) ).
tcf(c_51,negated_conjecture,
( sP3
| sP2
| sP9
| leq(n0,sK11)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f362]) ).
tcf(c_52,negated_conjecture,
( sP3
| sP2
| sP9
| gt(loopcounter,n1)
| leq(n0,sK11)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f363]) ).
tcf(c_53,negated_conjecture,
( sP3
| sP2
| sP9
| leq(sK11,n3)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f364]) ).
tcf(c_54,negated_conjecture,
( sP3
| sP2
| sP9
| gt(loopcounter,n1)
| leq(sK11,n3)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f365]) ).
tcf(c_57,negated_conjecture,
( sP8
| sP7
| sP6
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK12) != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_58,negated_conjecture,
( sP8
| sP7
| sP6
| gt(loopcounter,n1)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK12) != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f368]) ).
tcf(c_59,negated_conjecture,
( sP8
| sP7
| sP6
| leq(n0,sK12)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f369]) ).
tcf(c_60,negated_conjecture,
( sP8
| sP7
| sP6
| gt(loopcounter,n1)
| leq(n0,sK12)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_61,negated_conjecture,
( sP8
| sP7
| sP6
| leq(sK12,n3)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_62,negated_conjecture,
( sP8
| sP7
| sP6
| gt(loopcounter,n1)
| leq(sK12,n3)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_65,negated_conjecture,
( sP5
| sP4
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_66,negated_conjecture,
( sP5
| sP4
| gt(loopcounter,n1)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f375]) ).
tcf(c_67,negated_conjecture,
( sP5
| sP4
| leq(n0,sK13)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init ) ),
inference(cnf_transformation,[],[f376]) ).
tcf(c_68,negated_conjecture,
( sP5
| sP4
| gt(loopcounter,n1)
| leq(n0,sK13)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init ) ),
inference(cnf_transformation,[],[f377]) ).
tcf(c_69,negated_conjecture,
( sP5
| sP4
| leq(sK13,n3)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init ) ),
inference(cnf_transformation,[],[f378]) ).
tcf(c_70,negated_conjecture,
( sP5
| sP4
| gt(loopcounter,n1)
| leq(sK13,n3)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init ) ),
inference(cnf_transformation,[],[f379]) ).
tcf(c_72,negated_conjecture,
( ~ sP7
| ( a_select2(s_center7_init,sK14) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_73,plain,
( leq(n0,sK14)
| ~ sP7 ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_74,plain,
( leq(sK14,n2)
| ~ sP7 ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_75,negated_conjecture,
( ~ sP6
| ( a_select3(simplex7_init,sK16,sK15) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_76,plain,
( leq(n0,sK16)
| ~ sP6 ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_77,plain,
( leq(sK16,n3)
| ~ sP6 ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_78,plain,
( leq(n0,sK15)
| ~ sP6 ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_79,plain,
( leq(sK15,n2)
| ~ sP6 ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_80,negated_conjecture,
( ~ sP5
| ( a_select2(s_center7_init,sK17) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_81,plain,
( leq(n0,sK17)
| ~ sP5 ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_82,plain,
( leq(sK17,n2)
| ~ sP5 ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_83,negated_conjecture,
( ~ sP4
| ( a_select3(simplex7_init,sK19,sK18) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_84,plain,
( leq(n0,sK19)
| ~ sP4 ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_85,plain,
( leq(sK19,n3)
| ~ sP4 ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_86,plain,
( leq(n0,sK18)
| ~ sP4 ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_87,plain,
( leq(sK18,n2)
| ~ sP4 ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_88,negated_conjecture,
( ~ sP3
| ( a_select2(s_center7_init,sK20) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_89,plain,
( leq(n0,sK20)
| ~ sP3 ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_90,plain,
( leq(sK20,n2)
| ~ sP3 ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_91,negated_conjecture,
( ~ sP2
| ( a_select3(simplex7_init,sK22,sK21) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_92,plain,
( leq(n0,sK22)
| ~ sP2 ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_93,plain,
( leq(sK22,n3)
| ~ sP2 ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_94,plain,
( leq(n0,sK21)
| ~ sP2 ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_95,plain,
( leq(sK21,n2)
| ~ sP2 ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_96,negated_conjecture,
( ~ sP1
| ( a_select2(s_center7_init,sK23) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_97,plain,
( leq(n0,sK23)
| ~ sP1 ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_98,plain,
( leq(sK23,n2)
| ~ sP1 ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_104,negated_conjecture,
( sP0
| sP1
| sP10
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK26) != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f380]) ).
tcf(c_105,negated_conjecture,
( sP0
| sP1
| sP10
| gt(loopcounter,n1)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,sK26) != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f381]) ).
tcf(c_106,negated_conjecture,
( sP0
| sP1
| sP10
| leq(n0,sK26)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f382]) ).
tcf(c_107,negated_conjecture,
( sP0
| sP1
| sP10
| gt(loopcounter,n1)
| leq(n0,sK26)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_108,negated_conjecture,
( sP0
| sP1
| sP10
| leq(sK26,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f384]) ).
tcf(c_109,negated_conjecture,
( sP0
| sP1
| sP10
| gt(loopcounter,n1)
| leq(sK26,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f385]) ).
tcf(c_110,negated_conjecture,
( sP10
| gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
| ( s_sworst7_init != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f386]) ).
tcf(c_111,negated_conjecture,
s_sworst7_init = s_worst7_init,
inference(cnf_transformation,[],[f331]) ).
tcf(c_112,negated_conjecture,
leq(n0,s_best7),
inference(cnf_transformation,[],[f227]) ).
tcf(c_113,negated_conjecture,
leq(n0,s_sworst7),
inference(cnf_transformation,[],[f226]) ).
tcf(c_114,negated_conjecture,
leq(n0,s_worst7),
inference(cnf_transformation,[],[f225]) ).
tcf(c_115,negated_conjecture,
leq(n2,pv1388),
inference(cnf_transformation,[],[f224]) ).
tcf(c_116,negated_conjecture,
leq(s_best7,n3),
inference(cnf_transformation,[],[f223]) ).
tcf(c_117,negated_conjecture,
leq(s_sworst7,n3),
inference(cnf_transformation,[],[f222]) ).
tcf(c_118,negated_conjecture,
leq(s_worst7,n3),
inference(cnf_transformation,[],[f221]) ).
tcf(c_119,negated_conjecture,
leq(pv1388,n3),
inference(cnf_transformation,[],[f220]) ).
tcf(c_120,negated_conjecture,
! [X0: $i,X1: $i] :
( ( a_select3(simplex7_init,X0,X1) = s_sworst7_init )
| ~ leq(n0,X1)
| ~ leq(n0,X0)
| ~ leq(X1,n2)
| ~ leq(X0,n3) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_121,negated_conjecture,
! [X0: $i] :
( ( a_select2(s_values7_init,X0) = s_sworst7_init )
| ~ leq(n0,X0)
| ~ leq(X0,n3) ),
inference(cnf_transformation,[],[f333]) ).
tcf(c_122,negated_conjecture,
! [X0: $i] :
( ( a_select2(s_center7_init,X0) = s_sworst7_init )
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_123,negated_conjecture,
( ( s_sworst7_init = pvar1400_init )
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_124,negated_conjecture,
( ( s_sworst7_init = pvar1401_init )
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f336]) ).
tcf(c_125,negated_conjecture,
( ( s_sworst7_init = pvar1402_init )
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i] :
( leq(X1,X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_134,plain,
! [X0: $i] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f246]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(X2,X1)
| ~ leq(X2,X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_155,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f267]) ).
tcf(c_183,plain,
~ gt(s_sworst7_init,s_sworst7_init),
inference(instantiation,[status(thm)],[c_134]) ).
tcf(c_190,plain,
( gt(s_sworst7_init,s_sworst7_init)
| ( s_sworst7_init = s_sworst7_init ) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_208,plain,
( sP10
| gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_110]) ).
tcf(c_212,plain,
( sP5
| sP4
| gt(loopcounter,n1)
| leq(sK13,n3)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_70]) ).
tcf(c_213,plain,
( sP5
| sP4
| ~ leq(n0,pv1388)
| ~ sP8
| leq(sK13,n3) ),
inference(global_subsumption_just,[status(thm)],[c_212,c_119,c_118,c_116,c_114,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_70,c_69]) ).
tcf(c_214,plain,
( sP5
| sP4
| leq(sK13,n3)
| ~ sP8
| ~ leq(n0,pv1388) ),
inference(renaming,[status(thm)],[c_213]) ).
tcf(c_215,plain,
( sP5
| sP4
| gt(loopcounter,n1)
| leq(n0,sK13)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_68]) ).
tcf(c_216,plain,
( sP5
| sP4
| ~ leq(n0,pv1388)
| ~ sP8
| leq(n0,sK13) ),
inference(global_subsumption_just,[status(thm)],[c_215,c_119,c_118,c_116,c_114,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_68,c_67]) ).
tcf(c_217,plain,
( sP5
| sP4
| leq(n0,sK13)
| ~ sP8
| ~ leq(n0,pv1388) ),
inference(renaming,[status(thm)],[c_216]) ).
tcf(c_218,plain,
( sP5
| sP4
| gt(loopcounter,n1)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_66]) ).
tcf(c_219,plain,
( sP5
| sP4
| ( a_select2(s_values7_init,sK13) != s_sworst7_init )
| ~ leq(n0,pv1388)
| ~ sP8 ),
inference(global_subsumption_just,[status(thm)],[c_218,c_119,c_118,c_116,c_114,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_66,c_65]) ).
tcf(c_220,plain,
( sP5
| sP4
| ~ sP8
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_219]) ).
tcf(c_221,plain,
( sP5
| sP4
| leq(sK13,n3)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_69]) ).
tcf(c_222,plain,
( sP5
| sP4
| leq(sK13,n3)
| ~ sP8
| ~ leq(n0,pv1388) ),
inference(global_subsumption_just,[status(thm)],[c_221,c_214]) ).
tcf(c_224,plain,
( sP5
| sP4
| leq(n0,sK13)
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_67]) ).
tcf(c_225,plain,
( sP5
| sP4
| leq(n0,sK13)
| ~ sP8
| ~ leq(n0,pv1388) ),
inference(global_subsumption_just,[status(thm)],[c_224,c_217]) ).
tcf(c_227,plain,
( sP0
| sP1
| sP10
| gt(loopcounter,n1)
| leq(sK26,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_109]) ).
tcf(c_228,plain,
( sP0
| sP1
| sP10
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ~ leq(n0,pv1388)
| leq(sK26,n3) ),
inference(global_subsumption_just,[status(thm)],[c_227,c_119,c_118,c_117,c_114,c_113,c_111,c_183,c_125,c_124,c_123,c_190,c_109,c_108]) ).
tcf(c_229,plain,
( sP0
| sP1
| sP10
| leq(sK26,n3)
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_228]) ).
tcf(c_230,plain,
( sP0
| sP1
| sP10
| gt(loopcounter,n1)
| leq(n0,sK26)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_107]) ).
tcf(c_231,plain,
( sP0
| sP1
| sP10
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ~ leq(n0,pv1388)
| leq(n0,sK26) ),
inference(global_subsumption_just,[status(thm)],[c_230,c_119,c_118,c_117,c_114,c_113,c_111,c_183,c_125,c_124,c_123,c_190,c_107,c_106]) ).
tcf(c_232,plain,
( sP0
| sP1
| sP10
| leq(n0,sK26)
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_231]) ).
tcf(c_233,plain,
( sP8
| sP7
| sP6
| gt(loopcounter,n1)
| leq(sK12,n3)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_62]) ).
tcf(c_234,plain,
( sP8
| sP7
| sP6
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ~ sP9
| leq(sK12,n3) ),
inference(global_subsumption_just,[status(thm)],[c_233,c_118,c_117,c_116,c_114,c_113,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_62,c_61]) ).
tcf(c_235,plain,
( sP8
| sP7
| sP6
| leq(sK12,n3)
| ~ sP9
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_234]) ).
tcf(c_236,plain,
( sP8
| sP7
| sP6
| gt(loopcounter,n1)
| leq(n0,sK12)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_60]) ).
tcf(c_237,plain,
( sP8
| sP7
| sP6
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ~ sP9
| leq(n0,sK12) ),
inference(global_subsumption_just,[status(thm)],[c_236,c_118,c_117,c_116,c_114,c_113,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_60,c_59]) ).
tcf(c_238,plain,
( sP8
| sP7
| sP6
| leq(n0,sK12)
| ~ sP9
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_237]) ).
tcf(c_239,plain,
( sP3
| sP2
| sP9
| gt(loopcounter,n1)
| leq(sK11,n3)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_54]) ).
tcf(c_240,plain,
( sP3
| sP2
| sP9
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ~ leq(n0,pv1388)
| ~ sP10
| leq(sK11,n3) ),
inference(global_subsumption_just,[status(thm)],[c_239,c_119,c_118,c_116,c_114,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_54,c_53]) ).
tcf(c_241,plain,
( sP3
| sP2
| sP9
| leq(sK11,n3)
| ~ sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_240]) ).
tcf(c_242,plain,
( sP3
| sP2
| sP9
| gt(loopcounter,n1)
| leq(n0,sK11)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_52]) ).
tcf(c_243,plain,
( sP3
| sP2
| sP9
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ~ leq(n0,pv1388)
| ~ sP10
| leq(n0,sK11) ),
inference(global_subsumption_just,[status(thm)],[c_242,c_119,c_118,c_116,c_114,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_52,c_51]) ).
tcf(c_244,plain,
( sP3
| sP2
| sP9
| leq(n0,sK11)
| ~ sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_243]) ).
tcf(c_245,plain,
( sP5
| sP4
| ~ sP8
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_65]) ).
tcf(c_246,plain,
( sP5
| sP4
| ~ sP8
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(global_subsumption_just,[status(thm)],[c_245,c_220]) ).
tcf(c_248,plain,
( sP0
| sP1
| sP10
| gt(loopcounter,n1)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,sK26) != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_105]) ).
tcf(c_249,plain,
( sP0
| sP1
| sP10
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,sK26) != s_sworst7_init )
| ~ leq(n0,pv1388) ),
inference(global_subsumption_just,[status(thm)],[c_248,c_119,c_118,c_117,c_114,c_113,c_111,c_183,c_125,c_124,c_123,c_190,c_105,c_104]) ).
tcf(c_250,plain,
( sP0
| sP1
| sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,sK26) != s_sworst7_init )
| ( a_select2(s_values7_init,s_best7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_249]) ).
tcf(c_251,plain,
( sP8
| sP7
| sP6
| gt(loopcounter,n1)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,sK12) != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_58]) ).
tcf(c_252,plain,
( sP8
| sP7
| sP6
| ( a_select2(s_values7_init,sK12) != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ~ sP9 ),
inference(global_subsumption_just,[status(thm)],[c_251,c_118,c_117,c_116,c_114,c_113,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_58,c_57]) ).
tcf(c_253,plain,
( sP8
| sP7
| sP6
| ~ sP9
| ( a_select2(s_values7_init,sK12) != s_sworst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_252]) ).
tcf(c_254,plain,
( sP3
| sP2
| sP9
| gt(loopcounter,n1)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,sK11) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_50]) ).
tcf(c_255,plain,
( sP3
| sP2
| sP9
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,sK11) != s_sworst7_init )
| ~ leq(n0,pv1388)
| ~ sP10 ),
inference(global_subsumption_just,[status(thm)],[c_254,c_119,c_118,c_116,c_114,c_112,c_111,c_183,c_125,c_124,c_123,c_190,c_50,c_49]) ).
tcf(c_256,plain,
( sP3
| sP2
| sP9
| ~ sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,sK11) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_255]) ).
tcf(c_263,plain,
( sP8
| sP7
| sP6
| leq(sK12,n3)
| ~ sP9
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_61]) ).
tcf(c_264,plain,
( sP8
| sP7
| sP6
| leq(sK12,n3)
| ~ sP9
| ( a_select2(s_values7_init,s_sworst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(global_subsumption_just,[status(thm)],[c_263,c_235]) ).
tcf(c_269,plain,
( sP3
| sP2
| sP9
| leq(sK11,n3)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_53]) ).
tcf(c_270,plain,
( sP3
| sP2
| sP9
| leq(sK11,n3)
| ~ sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(global_subsumption_just,[status(thm)],[c_269,c_241]) ).
tcf(c_271,plain,
( sP3
| sP2
| sP9
| leq(sK11,n3)
| ~ sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_270]) ).
tcf(c_272,plain,
( sP3
| sP2
| sP9
| leq(n0,sK11)
| ~ sP10
| ~ leq(s_best7,n3)
| ~ leq(n0,s_best7)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ( s_sworst7_init != pvar1402_init )
| ( s_sworst7_init != pvar1401_init )
| ( s_sworst7_init != pvar1400_init )
| ( s_sworst7_init != s_worst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(equality_resolution_simp,[status(thm)],[c_51]) ).
tcf(c_273,plain,
( sP3
| sP2
| sP9
| leq(n0,sK11)
| ~ sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init )
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init ) ),
inference(global_subsumption_just,[status(thm)],[c_272,c_244]) ).
tcf(c_274,plain,
( sP3
| sP2
| sP9
| leq(n0,sK11)
| ~ sP10
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,pv1388) != s_sworst7_init )
| ( a_select2(s_values7_init,s_worst7) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_273]) ).
tcf(c_14297,plain,
( ( a_select2(s_values7_init,s_best7) = s_sworst7_init )
| ~ leq(s_best7,n3) ),
inference(superposition,[status(thm)],[c_112,c_121]) ).
tcf(c_14298,plain,
( ( a_select2(s_values7_init,s_worst7) = s_sworst7_init )
| ~ leq(s_worst7,n3) ),
inference(superposition,[status(thm)],[c_114,c_121]) ).
tcf(c_14299,plain,
( ( a_select2(s_values7_init,s_sworst7) = s_sworst7_init )
| ~ leq(s_sworst7,n3) ),
inference(superposition,[status(thm)],[c_113,c_121]) ).
tcf(c_14303,plain,
a_select2(s_values7_init,s_sworst7) = s_sworst7_init,
inference(forward_subsumption_resolution,[status(thm)],[c_14299,c_117]) ).
tcf(c_14304,plain,
a_select2(s_values7_init,s_worst7) = s_sworst7_init,
inference(forward_subsumption_resolution,[status(thm)],[c_14298,c_118]) ).
tcf(c_14305,plain,
a_select2(s_values7_init,s_best7) = s_sworst7_init,
inference(forward_subsumption_resolution,[status(thm)],[c_14297,c_116]) ).
tcf(c_14373,plain,
( ( a_select2(s_center7_init,sK14) = s_sworst7_init )
| ~ sP7
| ~ leq(sK14,n2) ),
inference(superposition,[status(thm)],[c_73,c_122]) ).
tcf(c_14407,plain,
~ sP7,
inference(global_subsumption_just,[status(thm)],[c_74,c_74,c_72,c_14373]) ).
tcf(c_14413,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK16,X0) = s_sworst7_init )
| ~ sP6
| ~ leq(sK16,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(superposition,[status(thm)],[c_76,c_120]) ).
tcf(c_14460,plain,
( ( a_select2(s_center7_init,sK17) = s_sworst7_init )
| ~ sP5
| ~ leq(sK17,n2) ),
inference(superposition,[status(thm)],[c_81,c_122]) ).
tcf(c_14474,plain,
~ sP5,
inference(global_subsumption_just,[status(thm)],[c_82,c_82,c_80,c_14460]) ).
tcf(c_14480,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK19,X0) = s_sworst7_init )
| ~ sP4
| ~ leq(sK19,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(superposition,[status(thm)],[c_84,c_120]) ).
tcf(c_14495,plain,
( ~ leq(n0,pv1388)
| ~ sP8
| leq(sK13,n3)
| sP4 ),
inference(global_subsumption_just,[status(thm)],[c_222,c_214,c_14474]) ).
tcf(c_14496,plain,
( sP4
| leq(sK13,n3)
| ~ sP8
| ~ leq(n0,pv1388) ),
inference(renaming,[status(thm)],[c_14495]) ).
tcf(c_14576,plain,
( ( a_select2(s_center7_init,sK20) = s_sworst7_init )
| ~ sP3
| ~ leq(sK20,n2) ),
inference(superposition,[status(thm)],[c_89,c_122]) ).
tcf(c_14590,plain,
~ sP3,
inference(global_subsumption_just,[status(thm)],[c_90,c_90,c_88,c_14576]) ).
tcf(c_14596,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK22,X0) = s_sworst7_init )
| ~ sP2
| ~ leq(sK22,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(superposition,[status(thm)],[c_92,c_120]) ).
tcf(c_14677,plain,
( ( a_select2(s_center7_init,sK23) = s_sworst7_init )
| ~ sP1
| ~ leq(sK23,n2) ),
inference(superposition,[status(thm)],[c_97,c_122]) ).
tcf(c_14691,plain,
~ sP1,
inference(global_subsumption_just,[status(thm)],[c_98,c_98,c_96,c_14677]) ).
tcf(c_14797,plain,
leq(n0,n2),
inference(superposition,[status(thm)],[c_155,c_133]) ).
tcf(c_14840,plain,
( ( a_select2(s_values7_init,sK13) != s_sworst7_init )
| ~ leq(n0,pv1388)
| ~ sP8
| sP4 ),
inference(global_subsumption_just,[status(thm)],[c_246,c_82,c_80,c_220,c_14460]) ).
tcf(c_14841,plain,
( sP4
| ~ sP8
| ~ leq(n0,pv1388)
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(renaming,[status(thm)],[c_14840]) ).
tcf(c_14968,plain,
( ( a_select2(s_values7_init,pv1388) = s_sworst7_init )
| ~ leq(n0,pv1388)
| ~ leq(pv1388,n3) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_15516,plain,
! [X0: $i] :
( leq(n0,pv1388)
| ~ leq(n0,X0)
| ~ leq(X0,pv1388) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_15564,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK16,X0) = s_sworst7_init )
| ~ sP6
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_14413,c_77,c_14413]) ).
tcf(c_15565,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK16,X0) = s_sworst7_init )
| ~ sP6
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(renaming,[status(thm)],[c_15564]) ).
tcf(c_15579,plain,
( ( a_select3(simplex7_init,sK16,sK15) = s_sworst7_init )
| ~ sP6
| ~ leq(sK15,n2) ),
inference(superposition,[status(thm)],[c_78,c_15565]) ).
tcf(c_16388,plain,
( leq(n0,pv1388)
| ~ leq(n2,pv1388)
| ~ leq(n0,n2) ),
inference(instantiation,[status(thm)],[c_15516]) ).
tcf(c_16664,negated_conjecture,
~ sP6,
inference(global_subsumption_just,[status(thm)],[c_75,c_79,c_75,c_15579]) ).
tcf(c_16786,plain,
! [X0: $i] :
( leq(X0,pv1388)
| ~ leq(X0,n2) ),
inference(superposition,[status(thm)],[c_115,c_139]) ).
tcf(c_17002,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK19,X0) = s_sworst7_init )
| ~ sP4
| ~ leq(sK19,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(superposition,[status(thm)],[c_84,c_120]) ).
tcf(c_17092,plain,
( ~ sP8
| leq(n0,sK13)
| sP4 ),
inference(global_subsumption_just,[status(thm)],[c_225,c_115,c_82,c_80,c_217,c_14460,c_14797,c_16388]) ).
tcf(c_17093,plain,
( sP4
| leq(n0,sK13)
| ~ sP8 ),
inference(renaming,[status(thm)],[c_17092]) ).
tcf(c_17101,plain,
( sP4
| ( a_select2(s_center7_init,sK13) = s_sworst7_init )
| ~ sP8
| ~ leq(sK13,n2) ),
inference(superposition,[status(thm)],[c_17093,c_122]) ).
tcf(c_17102,plain,
( sP4
| ( a_select2(s_values7_init,sK13) = s_sworst7_init )
| ~ sP8
| ~ leq(sK13,n3) ),
inference(superposition,[status(thm)],[c_17093,c_121]) ).
tcf(c_17260,plain,
leq(n0,pv1388),
inference(superposition,[status(thm)],[c_14797,c_16786]) ).
tcf(c_17271,plain,
( sP4
| ~ sP8
| ( a_select2(s_values7_init,sK13) != s_sworst7_init ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_14841,c_17260]) ).
tcf(c_17273,plain,
( sP4
| leq(sK13,n3)
| ~ sP8 ),
inference(backward_subsumption_resolution,[status(thm)],[c_14496,c_17260]) ).
tcf(c_17292,plain,
( sP4
| ~ sP8 ),
inference(global_subsumption_just,[status(thm)],[c_17101,c_115,c_14496,c_14797,c_16388,c_17102,c_17271]) ).
tcf(c_19766,plain,
( ( a_select2(s_values7_init,sK26) = s_sworst7_init )
| ~ leq(sK26,n3)
| ~ leq(n0,sK26) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_21206,plain,
( ( a_select2(s_values7_init,sK12) = s_sworst7_init )
| ~ leq(sK12,n3)
| ~ leq(n0,sK12) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_21611,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK19,X0) = s_sworst7_init )
| ~ sP4
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_17002,c_85,c_14480]) ).
tcf(c_21612,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK19,X0) = s_sworst7_init )
| ~ sP4
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(renaming,[status(thm)],[c_21611]) ).
tcf(c_21626,plain,
( ( a_select3(simplex7_init,sK19,sK18) = s_sworst7_init )
| ~ sP4
| ~ leq(sK18,n2) ),
inference(superposition,[status(thm)],[c_86,c_21612]) ).
tcf(c_21805,plain,
~ sP8,
inference(global_subsumption_just,[status(thm)],[c_17273,c_87,c_83,c_17292,c_21626]) ).
tcf(c_21819,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK22,X0) = s_sworst7_init )
| ~ sP2
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_14596,c_93,c_14596]) ).
tcf(c_21820,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK22,X0) = s_sworst7_init )
| ~ sP2
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(renaming,[status(thm)],[c_21819]) ).
tcf(c_21830,plain,
( ( a_select3(simplex7_init,sK22,s_best7) = s_sworst7_init )
| ~ sP2
| ~ leq(s_best7,n2) ),
inference(superposition,[status(thm)],[c_112,c_21820]) ).
tcf(c_21835,plain,
( ( a_select3(simplex7_init,sK22,sK21) = s_sworst7_init )
| ~ sP2
| ~ leq(sK21,n2) ),
inference(superposition,[status(thm)],[c_94,c_21820]) ).
tcf(c_21910,plain,
~ sP2,
inference(global_subsumption_just,[status(thm)],[c_21830,c_95,c_91,c_21835]) ).
tcf(c_22232,plain,
~ sP9,
inference(global_subsumption_just,[status(thm)],[c_264,c_119,c_115,c_235,c_238,c_253,c_14303,c_14407,c_14797,c_14968,c_16388,c_16664,c_21206,c_21805]) ).
fof(f110,definition,
( ~ sP0
| ? [X16] :
( leq(X16,n2)
& leq(n0,X16)
& ? [X17] :
( leq(X17,n3)
& leq(n0,X17)
& init != a_select3(simplex7_init,X17,X16) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f111,definition,
( ~ sP1
| ? [X19] :
( leq(X19,n2)
& leq(n0,X19)
& init != a_select2(s_center7_init,X19) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f112,definition,
( ~ sP2
| ? [X12] :
( leq(X12,n2)
& leq(n0,X12)
& ? [X13] :
( leq(X13,n3)
& leq(n0,X13)
& init != a_select3(simplex7_init,X13,X12) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f113,definition,
( ~ sP3
| ? [X15] :
( leq(X15,n2)
& leq(n0,X15)
& init != a_select2(s_center7_init,X15) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f114,definition,
( ~ sP4
| ? [X8] :
( leq(X8,n2)
& leq(n0,X8)
& ? [X9] :
( leq(X9,n3)
& leq(n0,X9)
& init != a_select3(simplex7_init,X9,X8) ) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f115,definition,
( ~ sP5
| ? [X11] :
( leq(X11,n2)
& leq(n0,X11)
& init != a_select2(s_center7_init,X11) ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f116,definition,
( ~ sP6
| ? [X4] :
( leq(X4,n2)
& leq(n0,X4)
& ? [X5] :
( leq(X5,n3)
& leq(n0,X5)
& init != a_select3(simplex7_init,X5,X4) ) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f117,definition,
( ~ sP7
| ? [X7] :
( leq(X7,n2)
& leq(n0,X7)
& init != a_select2(s_center7_init,X7) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f118,definition,
( ~ sP8
| ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| sP5
| ? [X10] :
( leq(X10,n3)
& leq(n0,X10)
& init != a_select2(s_values7_init,X10) )
| sP4
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| s_best7_init != init
| init != init ) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f119,definition,
( ~ sP9
| ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
& ( sP8
| ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| sP7
| ? [X6] :
( leq(X6,n3)
& leq(n0,X6)
& init != a_select2(s_values7_init,X6) )
| sP6
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| init != s_sworst7_init
| s_best7_init != init ) )
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_sworst7)
| init != s_sworst7_init
| init != init ) ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f120,definition,
( ~ sP10
| ( ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| sP3
| ? [X14] :
( leq(X14,n3)
& leq(n0,X14)
& init != a_select2(s_values7_init,X14) )
| sP2
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_best7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_best7)
| init != s_worst7_init
| s_best7_init != init
| init != init ) )
| sP9
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_worst7)
| init != s_worst7_init
| init != init ) ) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f121,plain,
( ( ~ gt(loopcounter,n1)
| ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [X3] :
( ~ leq(X3,n2)
| ~ leq(n0,X3)
| a_select2(s_center7_init,X3) = init )
& ! [X2] :
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| a_select2(s_values7_init,X2) = init )
& ! [X0] :
( ~ leq(X0,n2)
| ~ leq(n0,X0)
| ! [X1] :
( ~ leq(X1,n3)
| ~ leq(n0,X1)
| a_select3(simplex7_init,X1,X0) = init ) )
& leq(pv1388,n3)
& leq(s_worst7,n3)
& leq(s_sworst7,n3)
& leq(s_best7,n3)
& leq(n2,pv1388)
& leq(n0,s_worst7)
& leq(n0,s_sworst7)
& leq(n0,s_best7)
& s_worst7_init = init
& s_sworst7_init = init
& s_best7_init = init
& ( ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
& ( ( gt(loopcounter,n1)
& ( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init ) )
| sP1
| ? [X18] :
( leq(X18,n3)
& leq(n0,X18)
& init != a_select2(s_values7_init,X18) )
| sP0
| ~ leq(pv1388,n3)
| ~ leq(s_worst7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(n0,pv1388)
| ~ leq(n0,s_worst7)
| ~ leq(n0,s_sworst7)
| init != s_worst7_init
| init != s_sworst7_init
| init != init ) )
| sP10
| init != a_select2(s_values7_init,pv1388)
| init != a_select2(s_values7_init,s_best7)
| s_best7_init != init
| init != init ) ),
inference(definition_folding,[],[f88,f120,f119,f118,f117,f116,f115,f114,f113,f112,f111,f110]) ).
fof(f152,plain,
( ~ sP0
| ? [X16] :
( leq(X16,n2)
& leq(n0,X16)
& ? [X17] :
( leq(X17,n3)
& leq(n0,X17)
& init != a_select3(simplex7_init,X17,X16) ) ) ),
inference(nnf_transformation,[],[f110]) ).
fof(f153,plain,
( ~ sP0
| ? [X0] :
( leq(X0,n2)
& leq(n0,X0)
& ? [X1] :
( leq(X1,n3)
& leq(n0,X1)
& init != a_select3(simplex7_init,X1,X0) ) ) ),
inference(rectify,[],[f152]) ).
fof(f154,plain,
( ~ sP0
| ( leq(sK24,n2)
& leq(n0,sK24)
& leq(sK25,n3)
& leq(n0,sK25)
& init != a_select3(simplex7_init,sK25,sK24) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25]),skolemize(X0,sK24),skolemize(X1,sK25)],[f153]) ).
fof(f209,plain,
( ~ sP0
| leq(sK24,n2) ),
inference(cnf_transformation,[],[f154]) ).
fof(f210,plain,
( ~ sP0
| leq(n0,sK24) ),
inference(cnf_transformation,[],[f154]) ).
fof(f211,plain,
( ~ sP0
| leq(sK25,n3) ),
inference(cnf_transformation,[],[f154]) ).
fof(f212,plain,
( ~ sP0
| leq(n0,sK25) ),
inference(cnf_transformation,[],[f154]) ).
fof(f213,plain,
( ~ sP0
| init != a_select3(simplex7_init,sK25,sK24) ),
inference(cnf_transformation,[],[f154]) ).
fof(f323,plain,
( ~ sP0
| s_sworst7_init != a_select3(simplex7_init,sK25,sK24) ),
inference(definition_unfolding,[],[f213,f229]) ).
tcf(c_99,negated_conjecture,
( ~ sP0
| ( a_select3(simplex7_init,sK25,sK24) != s_sworst7_init ) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_100,plain,
( leq(n0,sK25)
| ~ sP0 ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_101,plain,
( leq(sK25,n3)
| ~ sP0 ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_102,plain,
( leq(n0,sK24)
| ~ sP0 ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_103,plain,
( leq(sK24,n2)
| ~ sP0 ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_14697,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK25,X0) = s_sworst7_init )
| ~ sP0
| ~ leq(sK25,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(superposition,[status(thm)],[c_100,c_120]) ).
tcf(c_22030,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK25,X0) = s_sworst7_init )
| ~ sP0
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_14697,c_101,c_14697]) ).
tcf(c_22031,plain,
! [X0: $i] :
( ( a_select3(simplex7_init,sK25,X0) = s_sworst7_init )
| ~ sP0
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(renaming,[status(thm)],[c_22030]) ).
tcf(c_22041,plain,
( ( a_select3(simplex7_init,sK25,s_best7) = s_sworst7_init )
| ~ sP0
| ~ leq(s_best7,n2) ),
inference(superposition,[status(thm)],[c_112,c_22031]) ).
tcf(c_22046,plain,
( ( a_select3(simplex7_init,sK25,sK24) = s_sworst7_init )
| ~ sP0
| ~ leq(sK24,n2) ),
inference(superposition,[status(thm)],[c_102,c_22031]) ).
tcf(c_22108,plain,
~ sP0,
inference(global_subsumption_just,[status(thm)],[c_22041,c_103,c_99,c_22046]) ).
tcf(c_22226,plain,
sP10,
inference(global_subsumption_just,[status(thm)],[c_208,c_119,c_115,c_229,c_232,c_250,c_14305,c_14691,c_14797,c_14968,c_16388,c_19766,c_22108]) ).
tcf(c_22572,plain,
leq(sK11,n3),
inference(global_subsumption_just,[status(thm)],[c_271,c_119,c_115,c_103,c_98,c_95,c_90,c_87,c_79,c_74,c_96,c_88,c_72,c_99,c_91,c_83,c_75,c_229,c_232,c_235,c_238,c_241,c_250,c_253,c_14305,c_14304,c_14303,c_14373,c_14576,c_14677,c_14797,c_14968,c_15579,c_16388,c_17292,c_19766,c_21206,c_21626,c_21835,c_22046]) ).
tcf(c_22581,plain,
leq(n0,sK11),
inference(global_subsumption_just,[status(thm)],[c_274,c_119,c_115,c_244,c_14304,c_14590,c_14797,c_14968,c_16388,c_21910,c_22226,c_22232]) ).
tcf(c_22598,plain,
( ( a_select2(s_values7_init,sK11) = s_sworst7_init )
| ~ leq(sK11,n3) ),
inference(superposition,[status(thm)],[c_22581,c_121]) ).
tcf(c_22607,plain,
a_select2(s_values7_init,sK11) = s_sworst7_init,
inference(forward_subsumption_resolution,[status(thm)],[c_22598,c_22572]) ).
tcf(c_22639,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_22607,c_22232,c_22226,c_21910,c_16388,c_14968,c_14797,c_14590,c_14304,c_256,c_115,c_119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV036+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 18:21:32 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.40 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 8.60/1.74 % SZS status Started for theBenchmark.p
% 8.60/1.74 % SZS status Theorem for theBenchmark.p
% 8.60/1.74
% 8.60/1.74 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.60/1.74
% 8.60/1.74 % ------ iProver source info
% 8.60/1.74
% 8.60/1.74 % git: date: 2026-07-19 20:42:38 +0200
% 8.60/1.74 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.60/1.74 % git: non_committed_changes: false
% 8.60/1.74
% 8.60/1.74 % ------ Parsing...
% 8.60/1.74 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.60/1.74
% 8.60/1.74 % ------ Preprocessing... sup_sim: 11 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 8.60/1.74
% 8.60/1.74 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.60/1.74
% 8.60/1.74 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.60/1.74 % ------ Proving...
% 8.60/1.74 % ------ Problem Properties
% 8.60/1.74
% 8.60/1.74 %
% 8.60/1.74 % clauses 121
% 8.60/1.74 % conjectures 24
% 8.60/1.74 % EPR 72
% 8.60/1.74 % Horn 100
% 8.60/1.74 % unary 48
% 8.60/1.74 % binary 45
% 8.60/1.74 % lits 289
% 8.60/1.75 % lits eq 81
% 8.60/1.75 % fd_pure 0
% 8.60/1.75 % fd_pseudo 0
% 8.60/1.75 % fd_cond 6
% 8.60/1.75 % fd_pseudo_cond 2
% 8.60/1.75 % AC symbols 0
% 8.60/1.75
% 8.60/1.75 % ------ Schedule dynamic 5 is on
% 8.60/1.75
% 8.60/1.75 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 8.60/1.75
% 8.60/1.75
% 8.60/1.75 % ------
% 8.60/1.75 % Current options:
% 8.60/1.75 % ------
% 8.60/1.75
% 8.60/1.75
% 8.60/1.75 %
% 8.60/1.75
% 8.60/1.75 % ------ Proving...
% 8.60/1.75 %
% 8.60/1.75
% 8.60/1.75 % SZS status Theorem for theBenchmark.p
% 8.60/1.75
% 8.60/1.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.60/1.75
% 8.60/1.75
%------------------------------------------------------------------------------