%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV033+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:02 PM UTC 2026
% Result : Theorem 0.38s 0.34s
% Output : Refutation 0.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 52
% Syntax : Number of formulae : 317 ( 65 unt; 28 def)
% Number of atoms : 946 ( 245 equ)
% Maximal formula atoms : 20 ( 2 avg)
% Number of connectives : 1020 ( 391 ~; 490 |; 90 &)
% ( 28 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 29 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 12 con; 0-3 aty)
% Number of variables : 140 ( 0 sgn 126 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(f9,axiom,
! [X0,X1] :
( ( leq(X0,X1)
& X0 != X1 )
=> gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt2) ).
fof(f10,axiom,
! [X0,X1] :
( leq(X0,pred(X1))
<=> gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt_pred) ).
fof(f29,axiom,
! [X0] : plus(X0,n1) = succ(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_plus_1_r) ).
fof(f30,axiom,
! [X0] : plus(n1,X0) = succ(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_plus_1_l) ).
fof(f31,axiom,
! [X0] : plus(X0,n2) = succ(succ(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_plus_2_r) ).
fof(f33,axiom,
! [X0] : plus(X0,n3) = succ(succ(succ(X0))),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_plus_3_r) ).
fof(f39,axiom,
! [X0] : minus(X0,n1) = pred(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',pred_minus_1) ).
fof(f40,axiom,
! [X0] : pred(succ(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',pred_succ) ).
fof(f48,axiom,
! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',sel2_update_1) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( X0 != X1
& a_select2(X2,X1) = X3 )
=> a_select2(tptp_update2(X2,X0,X4),X1) = X3 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',sel2_update_2) ).
fof(f53,conjecture,
( ( init = init
& leq(n0,pv1376)
& leq(pv1376,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,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X2) = init ) )
=> ( init = init
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> ! [X4] :
( ( leq(n0,X4)
& leq(X4,n3) )
=> a_select3(simplex7_init,X4,X3) = init ) )
& ! [X5] :
( ( leq(n0,X5)
& leq(X5,minus(plus(n1,pv1376),n1)) )
=> a_select2(tptp_update2(s_values7_init,pv1376,init),X5) = init ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gauss_init_0045) ).
fof(f54,negated_conjecture,
~ ( ( init = init
& leq(n0,pv1376)
& leq(pv1376,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,minus(pv1376,n1)) )
=> a_select2(s_values7_init,X2) = init ) )
=> ( init = init
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> ! [X4] :
( ( leq(n0,X4)
& leq(X4,n3) )
=> a_select3(simplex7_init,X4,X3) = init ) )
& ! [X5] :
( ( leq(n0,X5)
& leq(X5,minus(plus(n1,pv1376),n1)) )
=> a_select2(tptp_update2(s_values7_init,pv1376,init),X5) = init ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f69,axiom,
gt(n2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_1) ).
fof(f70,axiom,
gt(n3,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_1) ).
fof(f73,axiom,
gt(n3,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_2) ).
fof(f76,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n4) )
=> ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_4) ).
fof(f78,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n0) )
=> X0 = n0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_0) ).
fof(f79,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n1) )
=> ( X0 = n0
| X0 = n1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_1) ).
fof(f81,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n3) )
=> ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_3) ).
fof(f82,axiom,
succ(succ(succ(succ(n0)))) = n4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_4) ).
fof(f84,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_1) ).
fof(f85,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_2) ).
fof(f86,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_3) ).
fof(f100,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(X1,X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f101,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f9]) ).
fof(f102,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f101]) ).
fof(f132,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(ennf_transformation,[],[f49]) ).
fof(f133,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(flattening,[],[f132]) ).
fof(f136,plain,
( ( init != init
| ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ? [X5] :
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),X5)
& leq(n0,X5)
& leq(X5,minus(plus(n1,pv1376),n1)) ) )
& init = init
& leq(n0,pv1376)
& leq(pv1376,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,minus(pv1376,n1)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f137,plain,
( ( init != init
| ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ? [X5] :
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),X5)
& leq(n0,X5)
& leq(X5,minus(plus(n1,pv1376),n1)) ) )
& init = init
& leq(n0,pv1376)
& leq(pv1376,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,minus(pv1376,n1)) ) ),
inference(flattening,[],[f136]) ).
fof(f138,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| ~ leq(n0,X0)
| ~ leq(X0,n4) ),
inference(ennf_transformation,[],[f76]) ).
fof(f139,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| ~ leq(n0,X0)
| ~ leq(X0,n4) ),
inference(flattening,[],[f138]) ).
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(f144,plain,
! [X0] :
( X0 = n0
| X0 = n1
| ~ leq(n0,X0)
| ~ leq(X0,n1) ),
inference(ennf_transformation,[],[f79]) ).
fof(f145,plain,
! [X0] :
( X0 = n0
| X0 = n1
| ~ leq(n0,X0)
| ~ leq(X0,n1) ),
inference(flattening,[],[f144]) ).
fof(f148,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| ~ leq(n0,X0)
| ~ leq(X0,n3) ),
inference(ennf_transformation,[],[f81]) ).
fof(f149,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| ~ leq(n0,X0)
| ~ leq(X0,n3) ),
inference(flattening,[],[f148]) ).
fof(f157,definition,
( ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f158,plain,
( ( init != init
| sP4
| ? [X5] :
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),X5)
& leq(n0,X5)
& leq(X5,minus(plus(n1,pv1376),n1)) ) )
& init = init
& leq(n0,pv1376)
& leq(pv1376,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,minus(pv1376,n1)) ) ),
inference(definition_folding,[],[f137,f157]) ).
fof(f159,plain,
! [X0,X1] :
( ( leq(X0,pred(X1))
| ~ gt(X1,X0) )
& ( gt(X1,X0)
| ~ leq(X0,pred(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f192,plain,
( ? [X3] :
( ? [X4] :
( init != a_select3(simplex7_init,X4,X3)
& leq(n0,X4)
& leq(X4,n3) )
& leq(n0,X3)
& leq(X3,n2) )
| ~ sP4 ),
inference(nnf_transformation,[],[f157]) ).
fof(f193,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP4 ),
inference(rectify,[],[f192]) ).
fof(f194,plain,
( ( init != a_select3(simplex7_init,sK33,sK32)
& leq(n0,sK33)
& leq(sK33,n3)
& leq(n0,sK32)
& leq(sK32,n2) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33]),skolemize(X0,sK32),skolemize(X1,sK33)],[f193]) ).
fof(f195,plain,
( ( init != init
| sP4
| ? [X0] :
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),X0)
& leq(n0,X0)
& leq(X0,minus(plus(n1,pv1376),n1)) ) )
& init = init
& leq(n0,pv1376)
& leq(pv1376,n3)
& ! [X1] :
( ! [X2] :
( init = a_select3(simplex7_init,X2,X1)
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
| ~ leq(n0,X1)
| ~ leq(X1,n2) )
& ! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,minus(pv1376,n1)) ) ),
inference(rectify,[],[f158]) ).
fof(f196,plain,
( ( init != init
| sP4
| ( init != a_select2(tptp_update2(s_values7_init,pv1376,init),sK34)
& leq(n0,sK34)
& leq(sK34,minus(plus(n1,pv1376),n1)) ) )
& init = init
& leq(n0,pv1376)
& leq(pv1376,n3)
& ! [X1] :
( ! [X2] :
( init = a_select3(simplex7_init,X2,X1)
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
| ~ leq(n0,X1)
| ~ leq(X1,n2) )
& ! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,minus(pv1376,n1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X0,sK34)],[f195]) ).
fof(f199,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f202,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f203,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| gt(X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f102]) ).
fof(f204,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,pred(X1)) ),
inference(cnf_transformation,[],[f159]) ).
fof(f205,plain,
! [X0,X1] :
( leq(X0,pred(X1))
| ~ gt(X1,X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f277,plain,
! [X0] : succ(X0) = plus(X0,n1),
inference(cnf_transformation,[],[f29]) ).
fof(f278,plain,
! [X0] : succ(X0) = plus(n1,X0),
inference(cnf_transformation,[],[f30]) ).
fof(f279,plain,
! [X0] : plus(X0,n2) = succ(succ(X0)),
inference(cnf_transformation,[],[f31]) ).
fof(f281,plain,
! [X0] : plus(X0,n3) = succ(succ(succ(X0))),
inference(cnf_transformation,[],[f33]) ).
fof(f287,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[],[f39]) ).
fof(f288,plain,
! [X0] : pred(succ(X0)) = X0,
inference(cnf_transformation,[],[f40]) ).
fof(f301,plain,
! [X2,X0,X1] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f48]) ).
fof(f302,plain,
! [X2,X3,X0,X1,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(cnf_transformation,[],[f133]) ).
fof(f307,plain,
( leq(sK32,n2)
| ~ sP4 ),
inference(cnf_transformation,[],[f194]) ).
fof(f308,plain,
( leq(n0,sK32)
| ~ sP4 ),
inference(cnf_transformation,[],[f194]) ).
fof(f309,plain,
( leq(sK33,n3)
| ~ sP4 ),
inference(cnf_transformation,[],[f194]) ).
fof(f310,plain,
( leq(n0,sK33)
| ~ sP4 ),
inference(cnf_transformation,[],[f194]) ).
fof(f311,plain,
( init != a_select3(simplex7_init,sK33,sK32)
| ~ sP4 ),
inference(cnf_transformation,[],[f194]) ).
fof(f312,plain,
! [X3] :
( ~ leq(X3,minus(pv1376,n1))
| ~ leq(n0,X3)
| init = a_select2(s_values7_init,X3) ),
inference(cnf_transformation,[],[f196]) ).
fof(f313,plain,
! [X2,X1] :
( ~ leq(n0,X2)
| init = a_select3(simplex7_init,X2,X1)
| ~ leq(X2,n3)
| ~ leq(n0,X1)
| ~ leq(X1,n2) ),
inference(cnf_transformation,[],[f196]) ).
fof(f314,plain,
leq(pv1376,n3),
inference(cnf_transformation,[],[f196]) ).
fof(f315,plain,
leq(n0,pv1376),
inference(cnf_transformation,[],[f196]) ).
fof(f317,plain,
( init != init
| sP4
| leq(sK34,minus(plus(n1,pv1376),n1)) ),
inference(cnf_transformation,[],[f196]) ).
fof(f318,plain,
( init != init
| sP4
| leq(n0,sK34) ),
inference(cnf_transformation,[],[f196]) ).
fof(f319,plain,
( init != init
| sP4
| init != a_select2(tptp_update2(s_values7_init,pv1376,init),sK34) ),
inference(cnf_transformation,[],[f196]) ).
fof(f334,plain,
gt(n2,n1),
inference(cnf_transformation,[],[f69]) ).
fof(f335,plain,
gt(n3,n1),
inference(cnf_transformation,[],[f70]) ).
fof(f338,plain,
gt(n3,n2),
inference(cnf_transformation,[],[f73]) ).
fof(f341,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n2 = X0
| n3 = X0
| n4 = X0
| n0 = X0
| ~ leq(X0,n4) ),
inference(cnf_transformation,[],[f139]) ).
fof(f343,plain,
! [X0] :
( ~ leq(n0,X0)
| n0 = X0
| ~ leq(X0,n0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f344,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n0 = X0
| ~ leq(X0,n1) ),
inference(cnf_transformation,[],[f145]) ).
fof(f346,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n2 = X0
| n3 = X0
| n0 = X0
| ~ leq(X0,n3) ),
inference(cnf_transformation,[],[f149]) ).
fof(f347,plain,
n4 = succ(succ(succ(succ(n0)))),
inference(cnf_transformation,[],[f82]) ).
fof(f349,plain,
n1 = succ(n0),
inference(cnf_transformation,[],[f84]) ).
fof(f350,plain,
n2 = succ(succ(n0)),
inference(cnf_transformation,[],[f85]) ).
fof(f351,plain,
n3 = succ(succ(succ(n0))),
inference(cnf_transformation,[],[f86]) ).
fof(f352,plain,
! [X0,X1] :
( leq(X0,minus(X1,n1))
| ~ gt(X1,X0) ),
inference(definition_unfolding,[],[f205,f287]) ).
fof(f353,plain,
! [X0,X1] :
( ~ leq(X0,minus(X1,n1))
| gt(X1,X0) ),
inference(definition_unfolding,[],[f204,f287]) ).
fof(f359,plain,
! [X0] : plus(X0,n1) = plus(n1,X0),
inference(definition_unfolding,[],[f278,f277]) ).
fof(f360,plain,
! [X0] : plus(X0,n2) = plus(plus(X0,n1),n1),
inference(definition_unfolding,[],[f279,f277,f277]) ).
fof(f362,plain,
! [X0] : plus(X0,n3) = plus(plus(plus(X0,n1),n1),n1),
inference(definition_unfolding,[],[f281,f277,f277,f277]) ).
fof(f368,plain,
! [X0] : minus(plus(X0,n1),n1) = X0,
inference(definition_unfolding,[],[f288,f287,f277]) ).
fof(f373,plain,
n4 = plus(plus(plus(plus(n0,n1),n1),n1),n1),
inference(definition_unfolding,[],[f347,f277,f277,f277,f277]) ).
fof(f375,plain,
n1 = plus(n0,n1),
inference(definition_unfolding,[],[f349,f277]) ).
fof(f376,plain,
n2 = plus(plus(n0,n1),n1),
inference(definition_unfolding,[],[f350,f277,f277]) ).
fof(f377,plain,
n3 = plus(plus(plus(n0,n1),n1),n1),
inference(definition_unfolding,[],[f351,f277,f277,f277]) ).
fof(f380,plain,
! [X2,X0,X1,X4] :
( a_select2(X2,X1) = a_select2(tptp_update2(X2,X0,X4),X1)
| X0 = X1 ),
inference(equality_resolution,[],[f302]) ).
fof(f381,plain,
( sP4
| leq(sK34,minus(plus(n1,pv1376),n1)) ),
inference(trivial_inequality_removal,[],[f317]) ).
fof(f382,plain,
( sP4
| leq(n0,sK34) ),
inference(trivial_inequality_removal,[],[f318]) ).
fof(f383,plain,
( sP4
| init != a_select2(tptp_update2(s_values7_init,pv1376,init),sK34) ),
inference(trivial_inequality_removal,[],[f319]) ).
fof(f385,definition,
( spl35_1
<=> leq(sK34,minus(plus(n1,pv1376),n1)) ),
introduced(definition,[new_symbols(definition,[spl35_1])],[avatar_definition]) ).
fof(f387,plain,
( leq(sK34,minus(plus(n1,pv1376),n1))
| ~ spl35_1 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f389,definition,
( spl35_2
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl35_2])],[avatar_definition]) ).
fof(f392,plain,
( spl35_1
| spl35_2 ),
inference(avatar_split_clause,[],[f381,f389,f385]) ).
fof(f394,definition,
( spl35_3
<=> leq(n0,sK34) ),
introduced(definition,[new_symbols(definition,[spl35_3])],[avatar_definition]) ).
fof(f396,plain,
( leq(n0,sK34)
| ~ spl35_3 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,plain,
( spl35_3
| spl35_2 ),
inference(avatar_split_clause,[],[f382,f389,f394]) ).
fof(f399,definition,
( spl35_4
<=> init = a_select2(tptp_update2(s_values7_init,pv1376,init),sK34) ),
introduced(definition,[new_symbols(definition,[spl35_4])],[avatar_definition]) ).
fof(f401,plain,
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),sK34)
| spl35_4 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f402,plain,
( ~ spl35_4
| spl35_2 ),
inference(avatar_split_clause,[],[f383,f389,f399]) ).
fof(f404,definition,
( spl35_5
<=> leq(sK32,n2) ),
introduced(definition,[new_symbols(definition,[spl35_5])],[avatar_definition]) ).
fof(f406,plain,
( leq(sK32,n2)
| ~ spl35_5 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f407,plain,
( ~ spl35_2
| spl35_5 ),
inference(avatar_split_clause,[],[f307,f404,f389]) ).
fof(f409,definition,
( spl35_6
<=> leq(n0,sK32) ),
introduced(definition,[new_symbols(definition,[spl35_6])],[avatar_definition]) ).
fof(f411,plain,
( leq(n0,sK32)
| ~ spl35_6 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,plain,
( ~ spl35_2
| spl35_6 ),
inference(avatar_split_clause,[],[f308,f409,f389]) ).
fof(f414,definition,
( spl35_7
<=> leq(sK33,n3) ),
introduced(definition,[new_symbols(definition,[spl35_7])],[avatar_definition]) ).
fof(f416,plain,
( leq(sK33,n3)
| ~ spl35_7 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f417,plain,
( ~ spl35_2
| spl35_7 ),
inference(avatar_split_clause,[],[f309,f414,f389]) ).
fof(f419,definition,
( spl35_8
<=> leq(n0,sK33) ),
introduced(definition,[new_symbols(definition,[spl35_8])],[avatar_definition]) ).
fof(f421,plain,
( leq(n0,sK33)
| ~ spl35_8 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,plain,
( ~ spl35_2
| spl35_8 ),
inference(avatar_split_clause,[],[f310,f419,f389]) ).
fof(f424,definition,
( spl35_9
<=> init = a_select3(simplex7_init,sK33,sK32) ),
introduced(definition,[new_symbols(definition,[spl35_9])],[avatar_definition]) ).
fof(f427,plain,
( ~ spl35_2
| ~ spl35_9 ),
inference(avatar_split_clause,[],[f311,f424,f389]) ).
fof(f481,plain,
( ! [X0] :
( init = a_select3(simplex7_init,sK33,X0)
| ~ leq(sK33,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
| ~ spl35_8 ),
inference(resolution,[],[f421,f313]) ).
fof(f482,plain,
( ! [X0] :
( ~ leq(n0,X0)
| init = a_select3(simplex7_init,sK33,X0)
| ~ leq(X0,n2) )
| ~ spl35_7
| ~ spl35_8 ),
inference(forward_subsumption_resolution,[],[f481,f416]) ).
fof(f493,plain,
( init = a_select3(simplex7_init,sK33,sK32)
| ~ leq(sK32,n2)
| ~ spl35_6
| ~ spl35_7
| ~ spl35_8 ),
inference(resolution,[],[f482,f411]) ).
fof(f496,plain,
( init = a_select3(simplex7_init,sK33,sK32)
| ~ spl35_5
| ~ spl35_6
| ~ spl35_7
| ~ spl35_8 ),
inference(forward_subsumption_resolution,[],[f493,f406]) ).
fof(f497,plain,
( spl35_9
| ~ spl35_5
| ~ spl35_6
| ~ spl35_7
| ~ spl35_8 ),
inference(avatar_split_clause,[],[f496,f419,f414,f409,f404,f424]) ).
fof(f505,definition,
( spl35_23
<=> leq(sK34,n3) ),
introduced(definition,[new_symbols(definition,[spl35_23])],[avatar_definition]) ).
fof(f506,plain,
( leq(sK34,n3)
| ~ spl35_23 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f590,plain,
n2 = plus(n1,plus(n0,n1)),
inference(forward_demodulation,[],[f376,f359]) ).
fof(f591,plain,
n2 = plus(n1,n1),
inference(forward_demodulation,[],[f590,f375]) ).
fof(f677,plain,
! [X0] :
( ~ leq(n0,X0)
| ~ gt(pv1376,X0)
| init = a_select2(s_values7_init,X0) ),
inference(resolution,[],[f352,f312]) ).
fof(f696,plain,
( gt(plus(n1,pv1376),sK34)
| ~ spl35_1 ),
inference(resolution,[],[f353,f387]) ).
fof(f698,plain,
( leq(sK34,plus(n1,pv1376))
| ~ spl35_1 ),
inference(resolution,[],[f696,f202]) ).
fof(f727,plain,
( ~ gt(pv1376,sK34)
| init = a_select2(s_values7_init,sK34)
| ~ spl35_3 ),
inference(resolution,[],[f677,f396]) ).
fof(f732,definition,
( spl35_33
<=> init = a_select2(s_values7_init,sK34) ),
introduced(definition,[new_symbols(definition,[spl35_33])],[avatar_definition]) ).
fof(f736,definition,
( spl35_34
<=> gt(pv1376,sK34) ),
introduced(definition,[new_symbols(definition,[spl35_34])],[avatar_definition]) ).
fof(f738,plain,
( ~ gt(pv1376,sK34)
| spl35_34 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f739,plain,
( spl35_33
| ~ spl35_34
| ~ spl35_3 ),
inference(avatar_split_clause,[],[f727,f394,f736,f732]) ).
fof(f798,definition,
( spl35_43
<=> n0 = pv1376 ),
introduced(definition,[new_symbols(definition,[spl35_43])],[avatar_definition]) ).
fof(f799,plain,
( n0 != pv1376
| spl35_43 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f800,plain,
( n0 = pv1376
| ~ spl35_43 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f836,definition,
( spl35_45
<=> n3 = pv1376 ),
introduced(definition,[new_symbols(definition,[spl35_45])],[avatar_definition]) ).
fof(f838,plain,
( n3 = pv1376
| ~ spl35_45 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f879,definition,
( spl35_47
<=> n2 = pv1376 ),
introduced(definition,[new_symbols(definition,[spl35_47])],[avatar_definition]) ).
fof(f881,plain,
( n2 = pv1376
| ~ spl35_47 ),
inference(avatar_component_clause,[],[f879]) ).
fof(f894,plain,
( gt(pv1376,n0)
| n0 = pv1376 ),
inference(resolution,[],[f203,f315]) ).
fof(f939,definition,
( spl35_53
<=> n0 = sK34 ),
introduced(definition,[new_symbols(definition,[spl35_53])],[avatar_definition]) ).
fof(f940,plain,
( n0 != sK34
| spl35_53 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f941,plain,
( n0 = sK34
| ~ spl35_53 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f974,plain,
( ~ gt(pv1376,n0)
| spl35_34
| ~ spl35_53 ),
inference(superposition,[],[f738,f941]) ).
fof(f1001,plain,
( n0 = sK34
| ~ leq(sK34,n0)
| ~ spl35_3 ),
inference(resolution,[],[f343,f396]) ).
fof(f1038,plain,
! [X0] : plus(X0,n2) = plus(n1,plus(X0,n1)),
inference(forward_demodulation,[],[f360,f359]) ).
fof(f1043,plain,
( init != a_select2(tptp_update2(s_values7_init,n0,init),sK34)
| spl35_4
| ~ spl35_43 ),
inference(superposition,[],[f401,f800]) ).
fof(f1063,plain,
( init != a_select2(tptp_update2(s_values7_init,n0,init),n0)
| spl35_4
| ~ spl35_43
| ~ spl35_53 ),
inference(forward_demodulation,[],[f1043,f941]) ).
fof(f1067,plain,
( $false
| spl35_4
| ~ spl35_43
| ~ spl35_53 ),
inference(forward_subsumption_resolution,[],[f1063,f301]) ).
fof(f1068,plain,
( spl35_4
| ~ spl35_43
| ~ spl35_53 ),
inference(avatar_contradiction_clause,[],[f1067]) ).
fof(f1079,definition,
( spl35_67
<=> gt(pv1376,n0) ),
introduced(definition,[new_symbols(definition,[spl35_67])],[avatar_definition]) ).
fof(f1083,plain,
( spl35_43
| spl35_67 ),
inference(avatar_split_clause,[],[f894,f1079,f798]) ).
fof(f1084,plain,
( ~ spl35_67
| spl35_34
| ~ spl35_53 ),
inference(avatar_split_clause,[],[f974,f939,f736,f1079]) ).
fof(f1101,definition,
( spl35_71
<=> leq(sK34,n0) ),
introduced(definition,[new_symbols(definition,[spl35_71])],[avatar_definition]) ).
fof(f1103,plain,
( ~ leq(sK34,n0)
| spl35_71 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1104,plain,
( ~ spl35_71
| spl35_53
| ~ spl35_3 ),
inference(avatar_split_clause,[],[f1001,f394,f939,f1101]) ).
fof(f1120,definition,
( spl35_74
<=> n3 = sK34 ),
introduced(definition,[new_symbols(definition,[spl35_74])],[avatar_definition]) ).
fof(f1122,plain,
( n3 = sK34
| ~ spl35_74 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1124,definition,
( spl35_75
<=> gt(n3,sK34) ),
introduced(definition,[new_symbols(definition,[spl35_75])],[avatar_definition]) ).
fof(f1125,plain,
( ~ gt(n3,sK34)
| spl35_75 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1126,plain,
( gt(n3,sK34)
| ~ spl35_75 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1128,plain,
n3 = plus(n1,plus(plus(n0,n1),n1)),
inference(forward_demodulation,[],[f377,f359]) ).
fof(f1129,plain,
n3 = plus(n1,plus(n1,plus(n0,n1))),
inference(forward_demodulation,[],[f1128,f359]) ).
fof(f1130,plain,
n3 = plus(n1,plus(n1,n1)),
inference(forward_demodulation,[],[f1129,f375]) ).
fof(f1131,plain,
n3 = plus(n1,n2),
inference(forward_demodulation,[],[f1130,f591]) ).
fof(f1166,definition,
( spl35_76
<=> n2 = sK34 ),
introduced(definition,[new_symbols(definition,[spl35_76])],[avatar_definition]) ).
fof(f1168,plain,
( n2 = sK34
| ~ spl35_76 ),
inference(avatar_component_clause,[],[f1166]) ).
fof(f1189,plain,
! [X0] : plus(X0,n3) = plus(n1,plus(plus(X0,n1),n1)),
inference(forward_demodulation,[],[f362,f359]) ).
fof(f1190,plain,
! [X0] : plus(X0,n3) = plus(plus(X0,n1),n2),
inference(forward_demodulation,[],[f1189,f1038]) ).
fof(f1192,plain,
( leq(sK34,n3)
| ~ spl35_75 ),
inference(resolution,[],[f1126,f202]) ).
fof(f1201,plain,
( leq(sK34,minus(plus(n1,n0),n1))
| ~ spl35_1
| ~ spl35_43 ),
inference(superposition,[],[f387,f800]) ).
fof(f1221,plain,
( leq(sK34,minus(plus(n0,n1),n1))
| ~ spl35_1
| ~ spl35_43 ),
inference(forward_demodulation,[],[f1201,f359]) ).
fof(f1224,plain,
( leq(sK34,n0)
| ~ spl35_1
| ~ spl35_43 ),
inference(forward_demodulation,[],[f1221,f368]) ).
fof(f1225,plain,
( $false
| ~ spl35_1
| ~ spl35_43
| spl35_71 ),
inference(forward_subsumption_resolution,[],[f1224,f1103]) ).
fof(f1226,plain,
( ~ spl35_1
| ~ spl35_43
| spl35_71 ),
inference(avatar_contradiction_clause,[],[f1225]) ).
fof(f1239,plain,
n4 = plus(n1,plus(plus(plus(n0,n1),n1),n1)),
inference(forward_demodulation,[],[f373,f359]) ).
fof(f1240,plain,
n4 = plus(plus(plus(n0,n1),n1),n2),
inference(forward_demodulation,[],[f1239,f1038]) ).
fof(f1241,plain,
n4 = plus(plus(n0,n1),n3),
inference(forward_demodulation,[],[f1240,f1190]) ).
fof(f1242,plain,
n4 = plus(n1,n3),
inference(forward_demodulation,[],[f1241,f375]) ).
fof(f1259,plain,
( n1 = sK34
| n0 = sK34
| ~ leq(sK34,n1)
| ~ spl35_3 ),
inference(resolution,[],[f344,f396]) ).
fof(f1263,plain,
( n1 = sK34
| ~ leq(sK34,n1)
| ~ spl35_3
| spl35_53 ),
inference(forward_subsumption_resolution,[],[f1259,f940]) ).
fof(f1302,definition,
( spl35_86
<=> leq(sK34,n1) ),
introduced(definition,[new_symbols(definition,[spl35_86])],[avatar_definition]) ).
fof(f1306,definition,
( spl35_87
<=> n1 = sK34 ),
introduced(definition,[new_symbols(definition,[spl35_87])],[avatar_definition]) ).
fof(f1308,plain,
( n1 = sK34
| ~ spl35_87 ),
inference(avatar_component_clause,[],[f1306]) ).
fof(f1309,plain,
( ~ spl35_86
| spl35_87
| ~ spl35_3
| spl35_53 ),
inference(avatar_split_clause,[],[f1263,f939,f394,f1306,f1302]) ).
fof(f1315,definition,
( spl35_89
<=> n1 = pv1376 ),
introduced(definition,[new_symbols(definition,[spl35_89])],[avatar_definition]) ).
fof(f1317,plain,
( n1 = pv1376
| ~ spl35_89 ),
inference(avatar_component_clause,[],[f1315]) ).
fof(f1353,plain,
( spl35_23
| ~ spl35_75 ),
inference(avatar_split_clause,[],[f1192,f1124,f505]) ).
fof(f1369,plain,
( init != a_select2(s_values7_init,sK34)
| pv1376 = sK34
| spl35_4 ),
inference(superposition,[],[f401,f380]) ).
fof(f1371,definition,
( spl35_90
<=> pv1376 = sK34 ),
introduced(definition,[new_symbols(definition,[spl35_90])],[avatar_definition]) ).
fof(f1373,plain,
( pv1376 = sK34
| ~ spl35_90 ),
inference(avatar_component_clause,[],[f1371]) ).
fof(f1374,plain,
( spl35_90
| ~ spl35_33
| spl35_4 ),
inference(avatar_split_clause,[],[f1369,f399,f732,f1371]) ).
fof(f1451,plain,
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),n3)
| spl35_4
| ~ spl35_74 ),
inference(superposition,[],[f401,f1122]) ).
fof(f1484,plain,
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),n2)
| spl35_4
| ~ spl35_76 ),
inference(superposition,[],[f401,f1168]) ).
fof(f1494,plain,
( ~ gt(n3,n2)
| spl35_75
| ~ spl35_76 ),
inference(superposition,[],[f1125,f1168]) ).
fof(f1496,plain,
( $false
| spl35_75
| ~ spl35_76 ),
inference(forward_subsumption_resolution,[],[f1494,f338]) ).
fof(f1497,plain,
( spl35_75
| ~ spl35_76 ),
inference(avatar_contradiction_clause,[],[f1496]) ).
fof(f1501,plain,
( n1 = pv1376
| n2 = pv1376
| n3 = pv1376
| n0 = pv1376
| ~ leq(pv1376,n3) ),
inference(resolution,[],[f346,f315]) ).
fof(f1512,plain,
( n1 = sK34
| n2 = sK34
| n3 = sK34
| n0 = sK34
| ~ leq(sK34,n3)
| ~ spl35_3 ),
inference(resolution,[],[f346,f396]) ).
fof(f1516,plain,
( n1 = pv1376
| n2 = pv1376
| n3 = pv1376
| ~ leq(pv1376,n3)
| spl35_43 ),
inference(forward_subsumption_resolution,[],[f1501,f799]) ).
fof(f1517,plain,
( n1 = pv1376
| n2 = pv1376
| n3 = pv1376
| spl35_43 ),
inference(forward_subsumption_resolution,[],[f1516,f314]) ).
fof(f1518,plain,
( spl35_45
| spl35_47
| spl35_89
| spl35_43 ),
inference(avatar_split_clause,[],[f1517,f798,f1315,f879,f836]) ).
fof(f1526,plain,
( ~ gt(pv1376,n1)
| spl35_34
| ~ spl35_87 ),
inference(superposition,[],[f738,f1308]) ).
fof(f1531,plain,
( ~ gt(n3,n1)
| spl35_75
| ~ spl35_87 ),
inference(superposition,[],[f1125,f1308]) ).
fof(f1535,plain,
( $false
| spl35_75
| ~ spl35_87 ),
inference(forward_subsumption_resolution,[],[f1531,f335]) ).
fof(f1536,plain,
( spl35_75
| ~ spl35_87 ),
inference(avatar_contradiction_clause,[],[f1535]) ).
fof(f1594,plain,
( n1 = sK34
| n2 = sK34
| n3 = sK34
| n4 = sK34
| n0 = sK34
| ~ leq(sK34,n4)
| ~ spl35_3 ),
inference(resolution,[],[f341,f396]) ).
fof(f1643,definition,
( spl35_100
<=> leq(sK34,n4) ),
introduced(definition,[new_symbols(definition,[spl35_100])],[avatar_definition]) ).
fof(f1644,plain,
( leq(sK34,n4)
| ~ spl35_100 ),
inference(avatar_component_clause,[],[f1643]) ).
fof(f1647,definition,
( spl35_101
<=> n4 = sK34 ),
introduced(definition,[new_symbols(definition,[spl35_101])],[avatar_definition]) ).
fof(f1648,plain,
( n4 != sK34
| spl35_101 ),
inference(avatar_component_clause,[],[f1647]) ).
fof(f1649,plain,
( n4 = sK34
| ~ spl35_101 ),
inference(avatar_component_clause,[],[f1647]) ).
fof(f1662,plain,
( gt(plus(n1,n2),sK34)
| ~ spl35_1
| ~ spl35_47 ),
inference(superposition,[],[f696,f881]) ).
fof(f1663,plain,
( leq(sK34,plus(n1,n2))
| ~ spl35_1
| ~ spl35_47 ),
inference(superposition,[],[f698,f881]) ).
fof(f1675,plain,
( leq(sK34,n3)
| ~ spl35_1
| ~ spl35_47 ),
inference(forward_demodulation,[],[f1663,f1131]) ).
fof(f1676,plain,
( gt(n3,sK34)
| ~ spl35_1
| ~ spl35_47 ),
inference(forward_demodulation,[],[f1662,f1131]) ).
fof(f1684,plain,
( spl35_75
| ~ spl35_1
| ~ spl35_47 ),
inference(avatar_split_clause,[],[f1676,f879,f385,f1124]) ).
fof(f1687,plain,
( spl35_23
| ~ spl35_1
| ~ spl35_47 ),
inference(avatar_split_clause,[],[f1675,f879,f385,f505]) ).
fof(f1696,plain,
( ~ gt(n2,n1)
| spl35_34
| ~ spl35_47
| ~ spl35_87 ),
inference(forward_demodulation,[],[f1526,f881]) ).
fof(f1701,plain,
( $false
| spl35_34
| ~ spl35_47
| ~ spl35_87 ),
inference(forward_subsumption_resolution,[],[f1696,f334]) ).
fof(f1702,plain,
( spl35_34
| ~ spl35_47
| ~ spl35_87 ),
inference(avatar_contradiction_clause,[],[f1701]) ).
fof(f1712,plain,
( init != a_select2(tptp_update2(s_values7_init,n2,init),n2)
| spl35_4
| ~ spl35_47
| ~ spl35_76 ),
inference(forward_demodulation,[],[f1484,f881]) ).
fof(f1722,plain,
( $false
| spl35_4
| ~ spl35_47
| ~ spl35_76 ),
inference(forward_subsumption_resolution,[],[f1712,f301]) ).
fof(f1723,plain,
( spl35_4
| ~ spl35_47
| ~ spl35_76 ),
inference(avatar_contradiction_clause,[],[f1722]) ).
fof(f1860,plain,
( leq(sK34,minus(plus(n1,n1),n1))
| ~ spl35_1
| ~ spl35_89 ),
inference(superposition,[],[f387,f1317]) ).
fof(f1883,plain,
( leq(sK34,n1)
| ~ spl35_1
| ~ spl35_89 ),
inference(forward_demodulation,[],[f1860,f368]) ).
fof(f2039,plain,
( leq(sK34,plus(n1,n3))
| ~ spl35_1
| ~ spl35_45 ),
inference(superposition,[],[f698,f838]) ).
fof(f2040,plain,
( ~ gt(n3,sK34)
| spl35_34
| ~ spl35_45 ),
inference(superposition,[],[f738,f838]) ).
fof(f2056,plain,
( leq(sK34,n4)
| ~ spl35_1
| ~ spl35_45 ),
inference(forward_demodulation,[],[f2039,f1242]) ).
fof(f2064,plain,
( spl35_100
| ~ spl35_1
| ~ spl35_45 ),
inference(avatar_split_clause,[],[f2056,f836,f385,f1643]) ).
fof(f2122,plain,
( gt(plus(n1,pv1376),n4)
| ~ spl35_1
| ~ spl35_101 ),
inference(superposition,[],[f696,f1649]) ).
fof(f2137,plain,
( gt(plus(n1,n3),n4)
| ~ spl35_1
| ~ spl35_45
| ~ spl35_101 ),
inference(forward_demodulation,[],[f2122,f838]) ).
fof(f2141,plain,
( gt(n4,n4)
| ~ spl35_1
| ~ spl35_45
| ~ spl35_101 ),
inference(forward_demodulation,[],[f2137,f1242]) ).
fof(f2143,plain,
( $false
| ~ spl35_1
| ~ spl35_45
| ~ spl35_101 ),
inference(forward_subsumption_resolution,[],[f2141,f199]) ).
fof(f2144,plain,
( ~ spl35_1
| ~ spl35_45
| ~ spl35_101 ),
inference(avatar_contradiction_clause,[],[f2143]) ).
fof(f2146,plain,
( init != a_select2(tptp_update2(s_values7_init,n3,init),n3)
| spl35_4
| ~ spl35_45
| ~ spl35_74 ),
inference(forward_demodulation,[],[f1451,f838]) ).
fof(f2151,plain,
( $false
| spl35_4
| ~ spl35_45
| ~ spl35_74 ),
inference(forward_subsumption_resolution,[],[f2146,f301]) ).
fof(f2152,plain,
( spl35_4
| ~ spl35_45
| ~ spl35_74 ),
inference(avatar_contradiction_clause,[],[f2151]) ).
fof(f2180,plain,
( gt(n3,sK34)
| n3 = sK34
| ~ spl35_23 ),
inference(resolution,[],[f506,f203]) ).
fof(f2182,plain,
( spl35_74
| spl35_75
| ~ spl35_23 ),
inference(avatar_split_clause,[],[f2180,f505,f1124,f1120]) ).
fof(f2278,plain,
( gt(n3,n3)
| ~ spl35_74
| ~ spl35_75 ),
inference(forward_demodulation,[],[f1126,f1122]) ).
fof(f2279,plain,
( $false
| ~ spl35_74
| ~ spl35_75 ),
inference(forward_subsumption_resolution,[],[f2278,f199]) ).
fof(f2280,plain,
( ~ spl35_74
| ~ spl35_75 ),
inference(avatar_contradiction_clause,[],[f2279]) ).
fof(f2282,plain,
( ~ spl35_75
| spl35_34
| ~ spl35_45 ),
inference(avatar_split_clause,[],[f2040,f836,f736,f1124]) ).
fof(f2305,plain,
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),pv1376)
| spl35_4
| ~ spl35_90 ),
inference(superposition,[],[f401,f1373]) ).
fof(f2323,plain,
( $false
| spl35_4
| ~ spl35_90 ),
inference(forward_subsumption_resolution,[],[f2305,f301]) ).
fof(f2324,plain,
( spl35_4
| ~ spl35_90 ),
inference(avatar_contradiction_clause,[],[f2323]) ).
fof(f2328,plain,
( spl35_86
| ~ spl35_1
| ~ spl35_89 ),
inference(avatar_split_clause,[],[f1883,f1315,f385,f1302]) ).
fof(f2329,plain,
( n1 = sK34
| n2 = sK34
| n3 = sK34
| n0 = sK34
| ~ leq(sK34,n4)
| ~ spl35_3
| spl35_101 ),
inference(forward_subsumption_resolution,[],[f1594,f1648]) ).
fof(f2330,plain,
( n1 = sK34
| n2 = sK34
| n3 = sK34
| ~ leq(sK34,n3)
| ~ spl35_3
| spl35_53 ),
inference(forward_subsumption_resolution,[],[f1512,f940]) ).
fof(f2331,plain,
( n1 = sK34
| n2 = sK34
| n3 = sK34
| ~ leq(sK34,n4)
| ~ spl35_3
| spl35_53
| spl35_101 ),
inference(forward_subsumption_resolution,[],[f2329,f940]) ).
fof(f2332,plain,
( n1 = sK34
| n2 = sK34
| n3 = sK34
| ~ spl35_3
| ~ spl35_23
| spl35_53 ),
inference(forward_subsumption_resolution,[],[f2330,f506]) ).
fof(f2333,plain,
( n1 = sK34
| n2 = sK34
| n3 = sK34
| ~ spl35_3
| spl35_53
| ~ spl35_100
| spl35_101 ),
inference(forward_subsumption_resolution,[],[f2331,f1644]) ).
fof(f2334,plain,
( spl35_74
| spl35_76
| spl35_87
| ~ spl35_3
| ~ spl35_23
| spl35_53 ),
inference(avatar_split_clause,[],[f2332,f939,f505,f394,f1306,f1166,f1120]) ).
fof(f2335,plain,
( spl35_74
| spl35_76
| spl35_87
| ~ spl35_3
| spl35_53
| ~ spl35_100
| spl35_101 ),
inference(avatar_split_clause,[],[f2333,f1647,f1643,f939,f394,f1306,f1166,f1120]) ).
fof(f2451,plain,
( init != a_select2(tptp_update2(s_values7_init,n1,init),sK34)
| spl35_4
| ~ spl35_89 ),
inference(superposition,[],[f401,f1317]) ).
fof(f2468,plain,
( init != a_select2(tptp_update2(s_values7_init,n1,init),n1)
| spl35_4
| ~ spl35_87
| ~ spl35_89 ),
inference(forward_demodulation,[],[f2451,f1308]) ).
fof(f2471,plain,
( $false
| spl35_4
| ~ spl35_87
| ~ spl35_89 ),
inference(forward_subsumption_resolution,[],[f2468,f301]) ).
fof(f2472,plain,
( spl35_4
| ~ spl35_87
| ~ spl35_89 ),
inference(avatar_contradiction_clause,[],[f2471]) ).
cnf(s1,plain,
( spl35_1
| spl35_2 ),
inference(sat_conversion,[],[f392]) ).
cnf(s2,plain,
( spl35_2
| spl35_3 ),
inference(sat_conversion,[],[f397]) ).
cnf(s3,plain,
( spl35_2
| ~ spl35_4 ),
inference(sat_conversion,[],[f402]) ).
cnf(s4,plain,
( ~ spl35_2
| spl35_5 ),
inference(sat_conversion,[],[f407]) ).
cnf(s5,plain,
( ~ spl35_2
| spl35_6 ),
inference(sat_conversion,[],[f412]) ).
cnf(s6,plain,
( ~ spl35_2
| spl35_7 ),
inference(sat_conversion,[],[f417]) ).
cnf(s7,plain,
( ~ spl35_2
| spl35_8 ),
inference(sat_conversion,[],[f422]) ).
cnf(s8,plain,
( ~ spl35_2
| ~ spl35_9 ),
inference(sat_conversion,[],[f427]) ).
cnf(s15,plain,
( ~ spl35_5
| ~ spl35_6
| ~ spl35_7
| ~ spl35_8
| spl35_9 ),
inference(sat_conversion,[],[f497]) ).
cnf(s26,plain,
( ~ spl35_3
| spl35_33
| ~ spl35_34 ),
inference(sat_conversion,[],[f739]) ).
cnf(s52,plain,
( spl35_4
| ~ spl35_43
| ~ spl35_53 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s55,plain,
( spl35_43
| spl35_67 ),
inference(sat_conversion,[],[f1083]) ).
cnf(s56,plain,
( spl35_34
| ~ spl35_53
| ~ spl35_67 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s60,plain,
( ~ spl35_3
| spl35_53
| ~ spl35_71 ),
inference(sat_conversion,[],[f1104]) ).
cnf(s69,plain,
( ~ spl35_1
| ~ spl35_43
| spl35_71 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s74,plain,
( ~ spl35_3
| spl35_53
| ~ spl35_86
| spl35_87 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s82,plain,
( spl35_23
| ~ spl35_75 ),
inference(sat_conversion,[],[f1353]) ).
cnf(s83,plain,
( spl35_4
| ~ spl35_33
| spl35_90 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s94,plain,
( spl35_75
| ~ spl35_76 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s96,plain,
( spl35_43
| spl35_45
| spl35_47
| spl35_89 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s98,plain,
( spl35_75
| ~ spl35_87 ),
inference(sat_conversion,[],[f1536]) ).
cnf(s112,plain,
( ~ spl35_1
| ~ spl35_47
| spl35_75 ),
inference(sat_conversion,[],[f1684]) ).
cnf(s114,plain,
( ~ spl35_1
| spl35_23
| ~ spl35_47 ),
inference(sat_conversion,[],[f1687]) ).
cnf(s118,plain,
( spl35_34
| ~ spl35_47
| ~ spl35_87 ),
inference(sat_conversion,[],[f1702]) ).
cnf(s123,plain,
( spl35_4
| ~ spl35_47
| ~ spl35_76 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s142,plain,
( ~ spl35_1
| ~ spl35_45
| spl35_100 ),
inference(sat_conversion,[],[f2064]) ).
cnf(s145,plain,
( ~ spl35_1
| ~ spl35_45
| ~ spl35_101 ),
inference(sat_conversion,[],[f2144]) ).
cnf(s147,plain,
( spl35_4
| ~ spl35_45
| ~ spl35_74 ),
inference(sat_conversion,[],[f2152]) ).
cnf(s154,plain,
( ~ spl35_23
| spl35_74
| spl35_75 ),
inference(sat_conversion,[],[f2182]) ).
cnf(s155,plain,
( ~ spl35_74
| ~ spl35_75 ),
inference(sat_conversion,[],[f2280]) ).
cnf(s157,plain,
( spl35_34
| ~ spl35_45
| ~ spl35_75 ),
inference(sat_conversion,[],[f2282]) ).
cnf(s164,plain,
( spl35_4
| ~ spl35_90 ),
inference(sat_conversion,[],[f2324]) ).
cnf(s172,plain,
( ~ spl35_1
| spl35_86
| ~ spl35_89 ),
inference(sat_conversion,[],[f2328]) ).
cnf(s173,plain,
( ~ spl35_3
| ~ spl35_23
| spl35_53
| spl35_74
| spl35_76
| spl35_87 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s174,plain,
( ~ spl35_3
| spl35_53
| spl35_74
| spl35_76
| spl35_87
| ~ spl35_100
| spl35_101 ),
inference(sat_conversion,[],[f2335]) ).
cnf(s179,plain,
( spl35_4
| ~ spl35_87
| ~ spl35_89 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s182,plain,
~ spl35_2,
inference(rat,[],[s15,s4,s5,s6,s7,s8]) ).
cnf(s183,plain,
~ spl35_4,
inference(rat,[],[s3,s182]) ).
cnf(s184,plain,
spl35_3,
inference(rat,[],[s2,s182]) ).
cnf(s185,plain,
spl35_1,
inference(rat,[],[s1,s182]) ).
cnf(s186,plain,
~ spl35_90,
inference(rat,[],[s164,s183]) ).
cnf(s187,plain,
~ spl35_33,
inference(rat,[],[s83,s186,s183]) ).
cnf(s188,plain,
~ spl35_34,
inference(rat,[],[s26,s184,s187]) ).
cnf(s189,plain,
( spl35_23
| spl35_43 ),
inference(rat,[],[s174,s142,s145,s147,s96,s172,s74,s94,s98,s114,s82,s56,s55,s184,s185,s183,s188]) ).
cnf(s190,plain,
( ~ spl35_45
| ~ spl35_23 ),
inference(rat,[],[s154,s147,s157,s183,s188]) ).
cnf(s191,plain,
( ~ spl35_89
| spl35_53 ),
inference(rat,[],[s74,s179,s172,s184,s183,s185]) ).
cnf(s192,plain,
spl35_43,
inference(rat,[],[s155,s173,s112,s118,s123,s96,s191,s190,s189,s56,s55,s184,s185,s188,s183]) ).
cnf(s193,plain,
spl35_71,
inference(rat,[],[s69,s185,s192]) ).
cnf(s195,plain,
~ spl35_53,
inference(rat,[],[s52,s183,s192]) ).
cnf(s197,plain,
$false,
inference(rat,[],[s60,s184,s195,s193]) ).
fof(f2473,plain,
$false,
inference(avatar_sat_refutation,[],[s197]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV033+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n008.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 09:44:24 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.34 % (2139103)Will run a generic schedule for satisfiability detection.
% 0.38/0.34 % (2139108)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2116728658_2999 on theBenchmark for (2999ds/0Mi)
% 0.38/0.34 % (2139109)% WARNING: option uhcvi not known.
% 0.38/0.34 % (2139112)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=447955811:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.38/0.34 % (2139109)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1129478804:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.38/0.34 % (2139110)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3402701014:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.38/0.34 % (2139111)dis+10_1_sil=32000:sp=arity:random_seed=3167429479:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.38/0.34 % (2139114)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=297392500:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.38/0.34 % (2139113)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3309958961:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.38/0.34 % TRYING [1]
% 0.38/0.34 % TRYING [2]
% 0.38/0.34 % TRYING [3]
% 0.38/0.34 % (2139111) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2139103-2139111"...
% 0.38/0.34 % (2139111)...printing done.
% 0.38/0.34 % (2139111)Refutation found. Thanks to Tanya!
% 0.38/0.34 % SZS status Theorem for theBenchmark
% 0.38/0.34 % SZS output start Proof for theBenchmark
% See solution above
% 0.38/0.34 % (2139111)------------------------------
% 0.38/0.34 % (2139111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.38/0.34 % (2139111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.38/0.34 % (2139111)CaDiCaL version: 2.1.3
% 0.38/0.34 % (2139111)Termination reason: Refutation
% 0.38/0.34 % (2139111)Time elapsed: 0.062 s
% 0.38/0.34 % (2139111)Peak memory usage: 13 MB
% 0.38/0.34 % (2139111)Instructions burned: 102 (million)
% 0.38/0.34 % (2139103)Success in time 0.113 s
% 0.38/0.34 % Vampire exiting
%------------------------------------------------------------------------------