%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV039+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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 : Tue Sep 29 01:20:03 PM UTC 2026
% Result : Theorem 1.21s 0.45s
% Output : Refutation 1.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 24
% Syntax : Number of formulae : 239 ( 45 unt; 18 def)
% Number of atoms : 1545 ( 319 equ)
% Maximal formula atoms : 51 ( 6 avg)
% Number of connectives : 2207 ( 901 ~;1132 |; 129 &)
% ( 19 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 19 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 23 con; 0-3 aty)
% Number of variables : 84 ( 0 sgn 74 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(f10,axiom,
! [X0,X1] :
( leq(X0,pred(X1))
<=> gt(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt_pred) ).
fof(f39,axiom,
! [X0] : minus(X0,n1) = pred(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',pred_minus_1) ).
fof(f53,conjecture,
( ( s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,n3) )
=> a_select2(s_values7_init,X2) = init )
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> a_select2(s_center7_init,X3) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,n2) )
=> ! [X5] :
( ( leq(n0,X5)
& leq(X5,n3) )
=> a_select3(simplex7_init,X5,X4) = init ) )
& ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select2(s_values7_init,X6) = init )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n2) )
=> a_select2(s_center7_init,X7) = init )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,minus(n0,n1)) )
=> a_select2(s_try7_init,X8) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gauss_init_0069) ).
fof(f54,negated_conjecture,
~ ( ( s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,n3) )
=> a_select2(s_values7_init,X2) = init )
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> a_select2(s_center7_init,X3) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,n2) )
=> ! [X5] :
( ( leq(n0,X5)
& leq(X5,n3) )
=> a_select3(simplex7_init,X5,X4) = init ) )
& ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select2(s_values7_init,X6) = init )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n2) )
=> a_select2(s_center7_init,X7) = init )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,minus(n0,n1)) )
=> a_select2(s_try7_init,X8) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f78,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n0) )
=> X0 = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_0) ).
fof(f100,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(X1,X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f136,plain,
( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ? [X4] :
( ? [X5] :
( init != a_select3(simplex7_init,X5,X4)
& leq(n0,X5)
& leq(X5,n3) )
& leq(n0,X4)
& leq(X4,n2) )
| ? [X6] :
( init != a_select2(s_values7_init,X6)
& leq(n0,X6)
& leq(X6,n3) )
| ? [X7] :
( init != a_select2(s_center7_init,X7)
& leq(n0,X7)
& leq(X7,n2) )
| ? [X8] :
( init != a_select2(s_try7_init,X8)
& leq(n0,X8)
& leq(X8,minus(n0,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f137,plain,
( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ? [X4] :
( ? [X5] :
( init != a_select3(simplex7_init,X5,X4)
& leq(n0,X5)
& leq(X5,n3) )
& leq(n0,X4)
& leq(X4,n2) )
| ? [X6] :
( init != a_select2(s_values7_init,X6)
& leq(n0,X6)
& leq(X6,n3) )
| ? [X7] :
( init != a_select2(s_center7_init,X7)
& leq(n0,X7)
& leq(X7,n2) )
| ? [X8] :
( init != a_select2(s_try7_init,X8)
& leq(n0,X8)
& leq(X8,minus(n0,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(flattening,[],[f136]) ).
fof(f142,plain,
! [X0] :
( X0 = n0
| ~ leq(n0,X0)
| ~ leq(X0,n0) ),
inference(ennf_transformation,[],[f78]) ).
fof(f143,plain,
! [X0] :
( X0 = n0
| ~ leq(n0,X0)
| ~ leq(X0,n0) ),
inference(flattening,[],[f142]) ).
fof(f152,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f155,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f158,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,pred(X1)) ),
inference(cnf_transformation,[],[f10]) ).
fof(f288,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[],[f39]) ).
fof(f308,plain,
! [X4] :
( leq(sK37(X4),n3)
| ~ sP36(X4) ),
inference(cnf_transformation,[],[f137]) ).
fof(f309,plain,
! [X4] :
( leq(n0,sK37(X4))
| ~ sP36(X4) ),
inference(cnf_transformation,[],[f137]) ).
fof(f310,plain,
! [X4] :
( init != a_select3(simplex7_init,sK37(X4),X4)
| ~ sP36(X4) ),
inference(cnf_transformation,[],[f137]) ).
fof(f311,plain,
! [X4] :
( leq(X4,n2)
| ~ sP36(X4) ),
inference(cnf_transformation,[],[f137]) ).
fof(f312,plain,
! [X4] :
( leq(n0,X4)
| ~ sP36(X4) ),
inference(cnf_transformation,[],[f137]) ).
fof(f313,plain,
! [X6] :
( leq(X6,n3)
| ~ sP35(X6) ),
inference(cnf_transformation,[],[f137]) ).
fof(f314,plain,
! [X6] :
( leq(n0,X6)
| ~ sP35(X6) ),
inference(cnf_transformation,[],[f137]) ).
fof(f315,plain,
! [X6] :
( init != a_select2(s_values7_init,X6)
| ~ sP35(X6) ),
inference(cnf_transformation,[],[f137]) ).
fof(f316,plain,
! [X0,X1] :
( ~ leq(X0,n2)
| ~ leq(n0,X0)
| ~ leq(X1,n3)
| ~ leq(n0,X1)
| init = a_select3(simplex7_init,X1,X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f320,plain,
( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f321,plain,
( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f322,plain,
( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init
| leq(n0,sK31)
| init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f323,plain,
( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f324,plain,
( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f325,plain,
( init != pvar1402_init
| init != pvar1401_init
| init != pvar1400_init
| leq(sK31,minus(n0,n1))
| init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f329,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f330,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f331,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f332,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f333,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f334,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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 ),
inference(cnf_transformation,[],[f137]) ).
fof(f335,plain,
! [X2] :
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| init = a_select2(s_values7_init,X2) ),
inference(cnf_transformation,[],[f137]) ).
fof(f336,plain,
! [X3] :
( ~ leq(X3,n2)
| ~ leq(n0,X3)
| init = a_select2(s_center7_init,X3) ),
inference(cnf_transformation,[],[f137]) ).
fof(f337,plain,
( ~ gt(loopcounter,n1)
| init = pvar1402_init ),
inference(cnf_transformation,[],[f137]) ).
fof(f338,plain,
( ~ gt(loopcounter,n1)
| init = pvar1401_init ),
inference(cnf_transformation,[],[f137]) ).
fof(f339,plain,
( ~ gt(loopcounter,n1)
| init = pvar1400_init ),
inference(cnf_transformation,[],[f137]) ).
fof(f340,plain,
leq(s_worst7,n3),
inference(cnf_transformation,[],[f137]) ).
fof(f341,plain,
leq(s_sworst7,n3),
inference(cnf_transformation,[],[f137]) ).
fof(f342,plain,
leq(s_best7,n3),
inference(cnf_transformation,[],[f137]) ).
fof(f343,plain,
leq(n0,s_worst7),
inference(cnf_transformation,[],[f137]) ).
fof(f344,plain,
leq(n0,s_sworst7),
inference(cnf_transformation,[],[f137]) ).
fof(f345,plain,
leq(n0,s_best7),
inference(cnf_transformation,[],[f137]) ).
fof(f346,plain,
init = s_worst7_init,
inference(cnf_transformation,[],[f137]) ).
fof(f347,plain,
init = s_sworst7_init,
inference(cnf_transformation,[],[f137]) ).
fof(f348,plain,
s_best7_init = init,
inference(cnf_transformation,[],[f137]) ).
fof(f372,plain,
! [X0] :
( ~ leq(X0,n0)
| ~ leq(n0,X0)
| n0 = X0 ),
inference(cnf_transformation,[],[f143]) ).
fof(f381,plain,
s_best7_init = s_sworst7_init,
inference(definition_unfolding,[],[f348,f347]) ).
fof(f382,plain,
! [X0,X1] :
( ~ leq(X0,minus(X1,n1))
| gt(X1,X0) ),
inference(definition_unfolding,[],[f158,f288]) ).
fof(f403,plain,
s_sworst7_init = s_worst7_init,
inference(definition_unfolding,[],[f346,f347]) ).
fof(f404,plain,
( ~ gt(loopcounter,n1)
| s_sworst7_init = pvar1400_init ),
inference(definition_unfolding,[],[f339,f347]) ).
fof(f405,plain,
( ~ gt(loopcounter,n1)
| s_sworst7_init = pvar1401_init ),
inference(definition_unfolding,[],[f338,f347]) ).
fof(f406,plain,
( ~ gt(loopcounter,n1)
| s_sworst7_init = pvar1402_init ),
inference(definition_unfolding,[],[f337,f347]) ).
fof(f407,plain,
! [X3] :
( ~ leq(n0,X3)
| ~ leq(X3,n2)
| s_sworst7_init = a_select2(s_center7_init,X3) ),
inference(definition_unfolding,[],[f336,f347]) ).
fof(f408,plain,
! [X2] :
( ~ leq(n0,X2)
| ~ leq(X2,n3)
| s_sworst7_init = a_select2(s_values7_init,X2) ),
inference(definition_unfolding,[],[f335,f347]) ).
fof(f409,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f334,f347,f347,f347,f381,f347]) ).
fof(f410,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f333,f347,f347,f381,f347]) ).
fof(f411,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f332,f347,f347,f381,f347]) ).
fof(f412,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f331,f347,f347,f347,f381,f347]) ).
fof(f413,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f330,f347,f347,f381,f347]) ).
fof(f414,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f329,f347,f347,f381,f347]) ).
fof(f418,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f325,f347,f347,f347,f347,f347,f347,f381,f347]) ).
fof(f419,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f324,f347,f347,f347,f347,f347,f381,f347]) ).
fof(f420,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f323,f347,f347,f347,f347,f347,f381,f347]) ).
fof(f421,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f322,f347,f347,f347,f347,f347,f347,f381,f347]) ).
fof(f422,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f321,f347,f347,f347,f347,f347,f381,f347]) ).
fof(f423,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init ),
inference(definition_unfolding,[],[f320,f347,f347,f347,f347,f347,f381,f347]) ).
fof(f427,plain,
! [X0,X1] :
( ~ leq(n0,X1)
| ~ leq(n0,X0)
| ~ leq(X1,n3)
| ~ leq(X0,n2)
| s_sworst7_init = a_select3(simplex7_init,X1,X0) ),
inference(definition_unfolding,[],[f316,f347]) ).
fof(f428,plain,
! [X6] :
( s_sworst7_init != a_select2(s_values7_init,X6)
| ~ sP35(X6) ),
inference(definition_unfolding,[],[f315,f347]) ).
fof(f429,plain,
! [X4] :
( s_sworst7_init != a_select3(simplex7_init,sK37(X4),X4)
| ~ sP36(X4) ),
inference(definition_unfolding,[],[f310,f347]) ).
fof(f444,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f423]) ).
fof(f445,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f444]) ).
fof(f446,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f422]) ).
fof(f447,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f446]) ).
fof(f448,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f421]) ).
fof(f449,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(n0,sK31)
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f448]) ).
fof(f450,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f420]) ).
fof(f451,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f450]) ).
fof(f452,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f419]) ).
fof(f453,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f452]) ).
fof(f454,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f418]) ).
fof(f455,plain,
( s_sworst7_init != pvar1402_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1400_init
| leq(sK31,minus(n0,n1))
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f454]) ).
fof(f462,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f414]) ).
fof(f463,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f462]) ).
fof(f464,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f413]) ).
fof(f465,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f464]) ).
fof(f466,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f412]) ).
fof(f467,plain,
( gt(loopcounter,n1)
| leq(n0,sK31)
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f466]) ).
fof(f468,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f411]) ).
fof(f469,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(sK32,n2)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f468]) ).
fof(f470,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f410]) ).
fof(f471,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| leq(n0,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f470]) ).
fof(f472,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init
| s_sworst7_init != s_sworst7_init ),
inference(duplicate_literal_removal,[],[f409]) ).
fof(f473,plain,
( gt(loopcounter,n1)
| leq(sK31,minus(n0,n1))
| s_sworst7_init != a_select2(s_center7_init,sK32)
| sP35(sK33)
| sP36(sK34)
| ~ 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_sworst7_init != s_worst7_init ),
inference(trivial_inequality_removal,[],[f472]) ).
fof(f475,definition,
( spl38_1
<=> s_sworst7_init = s_worst7_init ),
introduced(definition,[new_symbols(definition,[spl38_1])],[avatar_definition]) ).
fof(f477,plain,
( s_sworst7_init != s_worst7_init
| spl38_1 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f479,definition,
( spl38_2
<=> leq(n0,s_best7) ),
introduced(definition,[new_symbols(definition,[spl38_2])],[avatar_definition]) ).
fof(f481,plain,
( ~ leq(n0,s_best7)
| spl38_2 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f483,definition,
( spl38_3
<=> leq(n0,s_sworst7) ),
introduced(definition,[new_symbols(definition,[spl38_3])],[avatar_definition]) ).
fof(f485,plain,
( ~ leq(n0,s_sworst7)
| spl38_3 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f487,definition,
( spl38_4
<=> leq(n0,s_worst7) ),
introduced(definition,[new_symbols(definition,[spl38_4])],[avatar_definition]) ).
fof(f489,plain,
( ~ leq(n0,s_worst7)
| spl38_4 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f491,definition,
( spl38_5
<=> leq(s_best7,n3) ),
introduced(definition,[new_symbols(definition,[spl38_5])],[avatar_definition]) ).
fof(f493,plain,
( ~ leq(s_best7,n3)
| spl38_5 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f495,definition,
( spl38_6
<=> leq(s_sworst7,n3) ),
introduced(definition,[new_symbols(definition,[spl38_6])],[avatar_definition]) ).
fof(f497,plain,
( ~ leq(s_sworst7,n3)
| spl38_6 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f499,definition,
( spl38_7
<=> leq(s_worst7,n3) ),
introduced(definition,[new_symbols(definition,[spl38_7])],[avatar_definition]) ).
fof(f501,plain,
( ~ leq(s_worst7,n3)
| spl38_7 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f503,definition,
( spl38_8
<=> sP36(sK34) ),
introduced(definition,[new_symbols(definition,[spl38_8])],[avatar_definition]) ).
fof(f505,plain,
( sP36(sK34)
| ~ spl38_8 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f507,definition,
( spl38_9
<=> sP35(sK33) ),
introduced(definition,[new_symbols(definition,[spl38_9])],[avatar_definition]) ).
fof(f509,plain,
( sP35(sK33)
| ~ spl38_9 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f511,definition,
( spl38_10
<=> leq(sK32,n2) ),
introduced(definition,[new_symbols(definition,[spl38_10])],[avatar_definition]) ).
fof(f513,plain,
( leq(sK32,n2)
| ~ spl38_10 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f519,definition,
( spl38_12
<=> s_sworst7_init = pvar1400_init ),
introduced(definition,[new_symbols(definition,[spl38_12])],[avatar_definition]) ).
fof(f523,definition,
( spl38_13
<=> s_sworst7_init = pvar1401_init ),
introduced(definition,[new_symbols(definition,[spl38_13])],[avatar_definition]) ).
fof(f527,definition,
( spl38_14
<=> s_sworst7_init = pvar1402_init ),
introduced(definition,[new_symbols(definition,[spl38_14])],[avatar_definition]) ).
fof(f532,definition,
( spl38_15
<=> leq(n0,sK32) ),
introduced(definition,[new_symbols(definition,[spl38_15])],[avatar_definition]) ).
fof(f534,plain,
( leq(n0,sK32)
| ~ spl38_15 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f537,definition,
( spl38_16
<=> s_sworst7_init = a_select2(s_center7_init,sK32) ),
introduced(definition,[new_symbols(definition,[spl38_16])],[avatar_definition]) ).
fof(f539,plain,
( s_sworst7_init != a_select2(s_center7_init,sK32)
| spl38_16 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f542,definition,
( spl38_17
<=> leq(n0,sK31) ),
introduced(definition,[new_symbols(definition,[spl38_17])],[avatar_definition]) ).
fof(f544,plain,
( leq(n0,sK31)
| ~ spl38_17 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f545,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| spl38_17
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14 ),
inference(avatar_split_clause,[],[f445,f527,f523,f519,f542,f511,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f546,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_15
| spl38_17
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14 ),
inference(avatar_split_clause,[],[f447,f527,f523,f519,f542,f532,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f547,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_16
| spl38_17
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14 ),
inference(avatar_split_clause,[],[f449,f527,f523,f519,f542,f537,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f549,definition,
( spl38_18
<=> leq(sK31,minus(n0,n1)) ),
introduced(definition,[new_symbols(definition,[spl38_18])],[avatar_definition]) ).
fof(f551,plain,
( leq(sK31,minus(n0,n1))
| ~ spl38_18 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f552,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| spl38_18
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14 ),
inference(avatar_split_clause,[],[f451,f527,f523,f519,f549,f511,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f553,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_15
| spl38_18
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14 ),
inference(avatar_split_clause,[],[f453,f527,f523,f519,f549,f532,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f554,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_16
| spl38_18
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14 ),
inference(avatar_split_clause,[],[f455,f527,f523,f519,f549,f537,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f556,definition,
( spl38_19
<=> gt(loopcounter,n1) ),
introduced(definition,[new_symbols(definition,[spl38_19])],[avatar_definition]) ).
fof(f562,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| spl38_17
| spl38_19 ),
inference(avatar_split_clause,[],[f463,f556,f542,f511,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f563,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_15
| spl38_17
| spl38_19 ),
inference(avatar_split_clause,[],[f465,f556,f542,f532,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f564,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_16
| spl38_17
| spl38_19 ),
inference(avatar_split_clause,[],[f467,f556,f542,f537,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f565,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| spl38_18
| spl38_19 ),
inference(avatar_split_clause,[],[f469,f556,f549,f511,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f566,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_15
| spl38_18
| spl38_19 ),
inference(avatar_split_clause,[],[f471,f556,f549,f532,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f567,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_16
| spl38_18
| spl38_19 ),
inference(avatar_split_clause,[],[f473,f556,f549,f537,f507,f503,f499,f495,f491,f487,f483,f479,f475]) ).
fof(f568,plain,
( spl38_14
| ~ spl38_19 ),
inference(avatar_split_clause,[],[f406,f556,f527]) ).
fof(f569,plain,
( spl38_13
| ~ spl38_19 ),
inference(avatar_split_clause,[],[f405,f556,f523]) ).
fof(f570,plain,
( spl38_12
| ~ spl38_19 ),
inference(avatar_split_clause,[],[f404,f556,f519]) ).
fof(f571,plain,
( $false
| spl38_1 ),
inference(forward_subsumption_resolution,[],[f477,f403]) ).
fof(f572,plain,
spl38_1,
inference(avatar_contradiction_clause,[],[f571]) ).
fof(f573,plain,
( $false
| spl38_2 ),
inference(forward_subsumption_resolution,[],[f481,f345]) ).
fof(f574,plain,
spl38_2,
inference(avatar_contradiction_clause,[],[f573]) ).
fof(f575,plain,
( $false
| spl38_3 ),
inference(forward_subsumption_resolution,[],[f485,f344]) ).
fof(f576,plain,
spl38_3,
inference(avatar_contradiction_clause,[],[f575]) ).
fof(f577,plain,
( $false
| spl38_4 ),
inference(forward_subsumption_resolution,[],[f489,f343]) ).
fof(f578,plain,
spl38_4,
inference(avatar_contradiction_clause,[],[f577]) ).
fof(f579,plain,
( $false
| spl38_5 ),
inference(forward_subsumption_resolution,[],[f493,f342]) ).
fof(f580,plain,
spl38_5,
inference(avatar_contradiction_clause,[],[f579]) ).
fof(f581,plain,
( $false
| spl38_6 ),
inference(forward_subsumption_resolution,[],[f497,f341]) ).
fof(f582,plain,
spl38_6,
inference(avatar_contradiction_clause,[],[f581]) ).
fof(f583,plain,
( $false
| spl38_7 ),
inference(forward_subsumption_resolution,[],[f501,f340]) ).
fof(f584,plain,
spl38_7,
inference(avatar_contradiction_clause,[],[f583]) ).
fof(f665,plain,
! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select2(s_values7_init,X0)
| ~ sP35(X0) ),
inference(resolution,[],[f408,f314]) ).
fof(f695,plain,
! [X0] :
( s_sworst7_init = a_select2(s_values7_init,X0)
| ~ sP35(X0) ),
inference(forward_subsumption_resolution,[],[f665,f313]) ).
fof(f696,plain,
! [X0] : ~ sP35(X0),
inference(forward_subsumption_resolution,[],[f695,f428]) ).
fof(f702,plain,
! [X0,X1] :
( ~ leq(n0,X0)
| ~ leq(sK37(X1),n3)
| ~ leq(X0,n2)
| s_sworst7_init = a_select3(simplex7_init,sK37(X1),X0)
| ~ sP36(X1) ),
inference(resolution,[],[f427,f309]) ).
fof(f703,plain,
! [X0,X1] :
( ~ sP36(X1)
| ~ leq(X0,n2)
| s_sworst7_init = a_select3(simplex7_init,sK37(X1),X0)
| ~ leq(n0,X0) ),
inference(forward_subsumption_resolution,[],[f702,f308]) ).
fof(f1081,plain,
( ! [X0] :
( ~ leq(X0,n2)
| s_sworst7_init = a_select3(simplex7_init,sK37(sK34),X0)
| ~ leq(n0,X0) )
| ~ spl38_8 ),
inference(resolution,[],[f703,f505]) ).
fof(f1082,plain,
( ! [X0] :
( s_sworst7_init = a_select3(simplex7_init,sK37(sK34),X0)
| ~ leq(n0,X0)
| ~ sP36(X0) )
| ~ spl38_8 ),
inference(resolution,[],[f1081,f311]) ).
fof(f1099,plain,
( ! [X0] :
( ~ sP36(X0)
| s_sworst7_init = a_select3(simplex7_init,sK37(sK34),X0) )
| ~ spl38_8 ),
inference(forward_subsumption_resolution,[],[f1082,f312]) ).
fof(f1109,plain,
( s_sworst7_init = a_select3(simplex7_init,sK37(sK34),sK34)
| ~ spl38_8 ),
inference(resolution,[],[f1099,f505]) ).
fof(f1110,plain,
( s_sworst7_init != s_sworst7_init
| ~ sP36(sK34)
| ~ spl38_8 ),
inference(superposition,[],[f429,f1109]) ).
fof(f1111,plain,
( ~ sP36(sK34)
| ~ spl38_8 ),
inference(trivial_inequality_removal,[],[f1110]) ).
fof(f1112,plain,
( $false
| ~ spl38_8 ),
inference(forward_subsumption_resolution,[],[f1111,f505]) ).
fof(f1113,plain,
~ spl38_8,
inference(avatar_contradiction_clause,[],[f1112]) ).
fof(f1114,plain,
( $false
| ~ spl38_9 ),
inference(forward_subsumption_resolution,[],[f509,f696]) ).
fof(f1115,plain,
~ spl38_9,
inference(avatar_contradiction_clause,[],[f1114]) ).
fof(f1128,plain,
( ~ leq(sK32,n2)
| s_sworst7_init = a_select2(s_center7_init,sK32)
| ~ spl38_15 ),
inference(resolution,[],[f534,f407]) ).
fof(f1153,plain,
( s_sworst7_init = a_select2(s_center7_init,sK32)
| ~ spl38_10
| ~ spl38_15 ),
inference(forward_subsumption_resolution,[],[f1128,f513]) ).
fof(f1166,plain,
( $false
| ~ spl38_10
| ~ spl38_15
| spl38_16 ),
inference(forward_subsumption_resolution,[],[f1153,f539]) ).
fof(f1167,plain,
( ~ spl38_10
| ~ spl38_15
| spl38_16 ),
inference(avatar_contradiction_clause,[],[f1166]) ).
fof(f3861,plain,
( gt(n0,sK31)
| ~ spl38_18 ),
inference(resolution,[],[f382,f551]) ).
fof(f3868,plain,
( leq(sK31,n0)
| ~ spl38_18 ),
inference(resolution,[],[f3861,f155]) ).
fof(f5395,plain,
( ~ leq(n0,sK31)
| n0 = sK31
| ~ spl38_18 ),
inference(resolution,[],[f372,f3868]) ).
fof(f5417,plain,
( n0 = sK31
| ~ spl38_17
| ~ spl38_18 ),
inference(forward_subsumption_resolution,[],[f5395,f544]) ).
fof(f5426,plain,
( gt(n0,n0)
| ~ spl38_17
| ~ spl38_18 ),
inference(superposition,[],[f3861,f5417]) ).
fof(f5434,plain,
( $false
| ~ spl38_17
| ~ spl38_18 ),
inference(forward_subsumption_resolution,[],[f5426,f152]) ).
fof(f5435,plain,
( ~ spl38_17
| ~ spl38_18 ),
inference(avatar_contradiction_clause,[],[f5434]) ).
cnf(s4,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_17 ),
inference(sat_conversion,[],[f545]) ).
cnf(s5,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_15
| spl38_17 ),
inference(sat_conversion,[],[f546]) ).
cnf(s6,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| ~ spl38_16
| spl38_17 ),
inference(sat_conversion,[],[f547]) ).
cnf(s7,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_18 ),
inference(sat_conversion,[],[f552]) ).
cnf(s8,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_15
| spl38_18 ),
inference(sat_conversion,[],[f553]) ).
cnf(s9,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| ~ spl38_16
| spl38_18 ),
inference(sat_conversion,[],[f554]) ).
cnf(s13,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| spl38_17
| spl38_19 ),
inference(sat_conversion,[],[f562]) ).
cnf(s14,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_15
| spl38_17
| spl38_19 ),
inference(sat_conversion,[],[f563]) ).
cnf(s15,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_16
| spl38_17
| spl38_19 ),
inference(sat_conversion,[],[f564]) ).
cnf(s16,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_10
| spl38_18
| spl38_19 ),
inference(sat_conversion,[],[f565]) ).
cnf(s17,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| spl38_15
| spl38_18
| spl38_19 ),
inference(sat_conversion,[],[f566]) ).
cnf(s18,plain,
( ~ spl38_1
| ~ spl38_2
| ~ spl38_3
| ~ spl38_4
| ~ spl38_5
| ~ spl38_6
| ~ spl38_7
| spl38_8
| spl38_9
| ~ spl38_16
| spl38_18
| spl38_19 ),
inference(sat_conversion,[],[f567]) ).
cnf(s19,plain,
( spl38_14
| ~ spl38_19 ),
inference(sat_conversion,[],[f568]) ).
cnf(s20,plain,
( spl38_13
| ~ spl38_19 ),
inference(sat_conversion,[],[f569]) ).
cnf(s21,plain,
( spl38_12
| ~ spl38_19 ),
inference(sat_conversion,[],[f570]) ).
cnf(s22,plain,
spl38_1,
inference(sat_conversion,[],[f572]) ).
cnf(s23,plain,
spl38_2,
inference(sat_conversion,[],[f574]) ).
cnf(s24,plain,
spl38_3,
inference(sat_conversion,[],[f576]) ).
cnf(s25,plain,
spl38_4,
inference(sat_conversion,[],[f578]) ).
cnf(s26,plain,
spl38_5,
inference(sat_conversion,[],[f580]) ).
cnf(s27,plain,
spl38_6,
inference(sat_conversion,[],[f582]) ).
cnf(s28,plain,
spl38_7,
inference(sat_conversion,[],[f584]) ).
cnf(s79,plain,
~ spl38_8,
inference(sat_conversion,[],[f1113]) ).
cnf(s80,plain,
~ spl38_9,
inference(sat_conversion,[],[f1115]) ).
cnf(s85,plain,
( ~ spl38_10
| ~ spl38_15
| spl38_16 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s251,plain,
( ~ spl38_17
| ~ spl38_18 ),
inference(sat_conversion,[],[f5435]) ).
cnf(s329,plain,
( ~ spl38_16
| spl38_18
| spl38_19 ),
inference(rat,[],[s18,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s330,plain,
( spl38_15
| spl38_18
| spl38_19 ),
inference(rat,[],[s17,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s331,plain,
( spl38_10
| spl38_18
| spl38_19 ),
inference(rat,[],[s16,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s332,plain,
( ~ spl38_16
| spl38_17
| spl38_19 ),
inference(rat,[],[s15,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s333,plain,
( spl38_15
| spl38_17
| spl38_19 ),
inference(rat,[],[s14,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s334,plain,
( spl38_10
| spl38_17
| spl38_19 ),
inference(rat,[],[s13,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s338,plain,
( ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| ~ spl38_16
| spl38_18 ),
inference(rat,[],[s9,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s339,plain,
( ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_15
| spl38_18 ),
inference(rat,[],[s8,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s340,plain,
( spl38_10
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_18 ),
inference(rat,[],[s7,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s341,plain,
( ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| ~ spl38_16
| spl38_17 ),
inference(rat,[],[s6,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s342,plain,
( ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_15
| spl38_17 ),
inference(rat,[],[s5,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s343,plain,
( spl38_10
| ~ spl38_12
| ~ spl38_13
| ~ spl38_14
| spl38_17 ),
inference(rat,[],[s4,s80,s79,s28,s27,s26,s25,s24,s23,s22]) ).
cnf(s347,plain,
( spl38_19
| spl38_10 ),
inference(rat,[],[s251,s334,s331]) ).
cnf(s348,plain,
( ~ spl38_13
| spl38_10
| ~ spl38_12
| ~ spl38_14 ),
inference(rat,[],[s251,s340,s343]) ).
cnf(s349,plain,
spl38_10,
inference(rat,[],[s348,s19,s20,s21,s347]) ).
cnf(s350,plain,
( spl38_19
| spl38_18 ),
inference(rat,[],[s85,s330,s329,s349]) ).
cnf(s351,plain,
( ~ spl38_14
| spl38_18
| ~ spl38_12
| ~ spl38_13 ),
inference(rat,[],[s85,s339,s338,s349]) ).
cnf(s352,plain,
spl38_18,
inference(rat,[],[s351,s19,s20,s21,s350]) ).
cnf(s353,plain,
~ spl38_17,
inference(rat,[],[s251,s352]) ).
cnf(s354,plain,
~ spl38_16,
inference(rat,[],[s341,s19,s20,s21,s332,s353]) ).
cnf(s355,plain,
~ spl38_15,
inference(rat,[],[s85,s349,s354]) ).
cnf(s356,plain,
spl38_19,
inference(rat,[],[s333,s353,s355]) ).
cnf(s357,plain,
spl38_12,
inference(rat,[],[s21,s356]) ).
cnf(s358,plain,
spl38_13,
inference(rat,[],[s20,s356]) ).
cnf(s359,plain,
spl38_14,
inference(rat,[],[s19,s356]) ).
cnf(s360,plain,
$false,
inference(rat,[],[s342,s353,s358,s355,s357,s359]) ).
fof(f5441,plain,
$false,
inference(avatar_sat_refutation,[],[s360]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV039+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.15 % Computer : n018.cluster.edu
% 0.10/0.15 % Model : x86_64 x86_64
% 0.10/0.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.15 % Memory : 8046.5625MB
% 0.10/0.15 % OS : Linux 6.8.0-71-generic
% 0.10/0.15 % CPULimit : 300
% 0.10/0.15 % WCLimit : 300
% 0.10/0.15 % DateTime : Mon Sep 28 09:46:54 UTC 2026
% 0.10/0.16 % CPUTime :
% 0.10/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 Running first-order model finding
% 0.10/0.19 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.21/0.45 % (3268983)Will run a generic schedule for satisfiability detection.
% 1.21/0.45 % (3268988)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=14030426_2999 on theBenchmark for (2999ds/0Mi)
% 1.21/0.45 % (3268989)% WARNING: option uhcvi not known.
% 1.21/0.45 % (3268989)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3041019241:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.21/0.45 % (3268990)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2139273752:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.21/0.45 % (3268991)dis+10_1_sil=32000:sp=arity:random_seed=133839395:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.21/0.45 % (3268992)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4273961490:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.21/0.45 % (3268993)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3912271469:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.21/0.45 % (3268994)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2329184348:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.21/0.45 % TRYING [1]
% 1.21/0.45 % TRYING [2]
% 1.21/0.45 % TRYING [3]
% 1.21/0.45 % (3268991)Instruction limit reached!
% 1.21/0.45 % (3268991)------------------------------
% 1.21/0.45 % (3268991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.21/0.45 % (3268991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.21/0.45 % (3268991)CaDiCaL version: 2.1.3
% 1.21/0.45 % (3268991)Termination reason: Instruction limit
% 1.21/0.45 % (3268991)Termination phase: Saturation
% 1.21/0.45 % (3268991)Time elapsed: 0.058 s
% 1.21/0.45 % (3268991)Peak memory usage: 12 MB
% 1.21/0.45 % (3268991)Instructions burned: 103 (million)
% 1.21/0.45 % (3268992)Instruction limit reached!
% 1.21/0.45 % (3268992)------------------------------
% 1.21/0.45 % (3268992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.21/0.45 % (3268992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.21/0.45 % (3268992)CaDiCaL version: 2.1.3
% 1.21/0.45 % (3268992)Termination reason: Instruction limit
% 1.21/0.45 % (3268992)Termination phase: Saturation
% 1.21/0.45 % (3268992)Time elapsed: 0.066 s
% 1.21/0.45 % (3268992)Peak memory usage: 13 MB
% 1.21/0.45 % (3268992)Instructions burned: 117 (million)
% 1.21/0.45 % (3268993)Instruction limit reached!
% 1.21/0.45 % (3268993)------------------------------
% 1.21/0.45 % (3268993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.21/0.45 % (3268993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.21/0.45 % (3268993)CaDiCaL version: 2.1.3
% 1.21/0.45 % (3268993)Termination reason: Instruction limit
% 1.21/0.45 % (3268993)Termination phase: Saturation
% 1.21/0.45 % (3268993)Time elapsed: 0.070 s
% 1.21/0.45 % (3268993)Peak memory usage: 13 MB
% 1.21/0.45 % (3268993)Instructions burned: 131 (million)
% 1.21/0.45 % (3269002)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=794797225:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.21/0.45 % TRYING [4]
% 1.21/0.45 % (3269003)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=468210446:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.21/0.45 % (3269004)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3003037127:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.21/0.45 % (3268994)Instruction limit reached!
% 1.21/0.45 % (3268994)------------------------------
% 1.21/0.45 % (3268994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.21/0.45 % (3268994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.21/0.45 % (3268994)CaDiCaL version: 2.1.3
% 1.21/0.45 % (3268994)Termination reason: Instruction limit
% 1.21/0.45 % (3268994)Termination phase: Saturation
% 1.21/0.45 % (3268994)Time elapsed: 0.097 s
% 1.21/0.45 % (3268994)Peak memory usage: 14 MB
% 1.21/0.45 % (3268994)Instructions burned: 160 (million)
% 1.21/0.45 % TRYING [1]
% 1.21/0.45 % TRYING [2]
% 1.21/0.45 % TRYING [3]
% 1.21/0.45 % (3269008)ott-21_1_sil=16000:fs=off:random_seed=1321597875:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.21/0.45 % TRYING [4]
% 1.21/0.45 % (3269003)Instruction limit reached!
% 1.21/0.45 % (3269003)------------------------------
% 1.21/0.45 % (3269003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.21/0.45 % (3269003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.21/0.45 % (3269003)CaDiCaL version: 2.1.3
% 1.21/0.45 % (3269003)Termination reason: Instruction limit
% 1.21/0.45 % (3269003)Termination phase: Saturation
% 1.21/0.45 % (3269003)Time elapsed: 0.081 s
% 1.21/0.45 % (3269003)Peak memory usage: 13 MB
% 1.21/0.45 % (3269003)Instructions burned: 134 (million)
% 1.21/0.45 % (3269010)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=685230395:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.21/0.45 % (3269004) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3268983-3269004"...
% 1.21/0.45 % (3269008)Instruction limit reached!
% 1.21/0.45 % (3269008)------------------------------
% 1.21/0.45 % (3269008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.21/0.45 % (3269008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.21/0.45 % (3269008)CaDiCaL version: 2.1.3
% 1.21/0.45 % (3269008)Termination reason: Instruction limit
% 1.21/0.45 % (3269008)Termination phase: Saturation
% 1.21/0.45 % (3269008)Time elapsed: 0.094 s
% 1.21/0.45 % (3269008)Peak memory usage: 13 MB
% 1.21/0.45 % (3269008)Instructions burned: 182 (million)
% 1.21/0.45 % (3269004)...printing done.
% 1.21/0.45 % (3269004)Refutation found. Thanks to Tanya!
% 1.21/0.45 % SZS status Theorem for theBenchmark
% 1.21/0.45 % SZS output start Proof for theBenchmark
% See solution above
% 1.21/0.46 % (3269004)------------------------------
% 1.21/0.46 % (3269004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.21/0.46 % (3269004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.21/0.46 % (3269004)CaDiCaL version: 2.1.3
% 1.21/0.46 % (3269004)Termination reason: Refutation
% 1.21/0.46 % (3269004)Time elapsed: 0.122 s
% 1.21/0.46 % (3269004)Peak memory usage: 15 MB
% 1.21/0.46 % (3269004)Instructions burned: 187 (million)
% 1.21/0.46 % (3268983)Success in time 0.255 s
% 1.21/0.46 % Vampire exiting
%------------------------------------------------------------------------------