%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV109+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 : n013.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:15 PM UTC 2026
% Result : Theorem 0.19s 0.33s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 41
% Syntax : Number of formulae : 239 ( 20 unt; 40 def)
% Number of atoms : 1067 ( 114 equ)
% Maximal formula atoms : 56 ( 4 avg)
% Number of connectives : 1221 ( 393 ~; 521 |; 245 &)
% ( 36 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 41 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 21 con; 0-3 aty)
% Number of variables : 169 ( 0 sgn 121 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f53,conjecture,
( ( leq(n0,pv5)
& leq(n0,pv47)
& leq(pv5,minus(n999,n1))
& leq(pv47,minus(n6,n1))
& ! [X0,X1] :
( ( leq(n0,X0)
& leq(n0,X1)
& leq(X0,minus(n6,n1))
& leq(X1,minus(n6,n1)) )
=> a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0) )
& ! [X2,X3] :
( ( leq(n0,X2)
& leq(n0,X3)
& leq(X2,minus(n3,n1))
& leq(X3,minus(n3,n1)) )
=> a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2) )
& ! [X4,X5] :
( ( leq(n0,X4)
& leq(n0,X5)
& leq(X4,minus(n6,n1))
& leq(X5,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4) )
& ! [X6,X7] :
( ( leq(n0,X6)
& leq(n0,X7)
& leq(X6,minus(n6,n1))
& leq(X7,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6) )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,minus(n6,n1)) )
=> ! [X9] :
( ( leq(n0,X9)
& leq(X9,minus(n6,n1)) )
=> a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8) ) ) )
=> ( leq(n0,pv5)
& leq(pv5,minus(n999,n1))
& ! [X10,X11] :
( ( leq(n0,X10)
& leq(n0,X11)
& leq(X10,minus(n6,n1))
& leq(X11,minus(n6,n1)) )
=> a_select3(q_ds1_filter,X10,X11) = a_select3(q_ds1_filter,X11,X10) )
& ! [X12,X13] :
( ( leq(n0,X12)
& leq(n0,X13)
& leq(X12,minus(n3,n1))
& leq(X13,minus(n3,n1)) )
=> a_select3(r_ds1_filter,X12,X13) = a_select3(r_ds1_filter,X13,X12) )
& ! [X14,X15] :
( ( leq(n0,X14)
& leq(n0,X15)
& leq(X14,minus(n6,n1))
& leq(X15,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X14,X15) = a_select3(pminus_ds1_filter,X15,X14) )
& ! [X16,X17] :
( ( leq(n0,X16)
& leq(n0,X17)
& leq(X16,minus(n6,n1))
& leq(X17,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X16,X17) = a_select3(pminus_ds1_filter,X17,X16) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,minus(n6,n1)) )
=> ! [X19] :
( ( leq(n0,X19)
& leq(X19,minus(n6,n1)) )
=> a_select3(id_ds1_filter,X18,X19) = a_select3(id_ds1_filter,X19,X18) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_symm_0002) ).
fof(f54,negated_conjecture,
~ ( ( leq(n0,pv5)
& leq(n0,pv47)
& leq(pv5,minus(n999,n1))
& leq(pv47,minus(n6,n1))
& ! [X0,X1] :
( ( leq(n0,X0)
& leq(n0,X1)
& leq(X0,minus(n6,n1))
& leq(X1,minus(n6,n1)) )
=> a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0) )
& ! [X2,X3] :
( ( leq(n0,X2)
& leq(n0,X3)
& leq(X2,minus(n3,n1))
& leq(X3,minus(n3,n1)) )
=> a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2) )
& ! [X4,X5] :
( ( leq(n0,X4)
& leq(n0,X5)
& leq(X4,minus(n6,n1))
& leq(X5,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4) )
& ! [X6,X7] :
( ( leq(n0,X6)
& leq(n0,X7)
& leq(X6,minus(n6,n1))
& leq(X7,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6) )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,minus(n6,n1)) )
=> ! [X9] :
( ( leq(n0,X9)
& leq(X9,minus(n6,n1)) )
=> a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8) ) ) )
=> ( leq(n0,pv5)
& leq(pv5,minus(n999,n1))
& ! [X10,X11] :
( ( leq(n0,X10)
& leq(n0,X11)
& leq(X10,minus(n6,n1))
& leq(X11,minus(n6,n1)) )
=> a_select3(q_ds1_filter,X10,X11) = a_select3(q_ds1_filter,X11,X10) )
& ! [X12,X13] :
( ( leq(n0,X12)
& leq(n0,X13)
& leq(X12,minus(n3,n1))
& leq(X13,minus(n3,n1)) )
=> a_select3(r_ds1_filter,X12,X13) = a_select3(r_ds1_filter,X13,X12) )
& ! [X14,X15] :
( ( leq(n0,X14)
& leq(n0,X15)
& leq(X14,minus(n6,n1))
& leq(X15,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X14,X15) = a_select3(pminus_ds1_filter,X15,X14) )
& ! [X16,X17] :
( ( leq(n0,X16)
& leq(n0,X17)
& leq(X16,minus(n6,n1))
& leq(X17,minus(n6,n1)) )
=> a_select3(pminus_ds1_filter,X16,X17) = a_select3(pminus_ds1_filter,X17,X16) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,minus(n6,n1)) )
=> ! [X19] :
( ( leq(n0,X19)
& leq(X19,minus(n6,n1)) )
=> a_select3(id_ds1_filter,X18,X19) = a_select3(id_ds1_filter,X19,X18) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f153,plain,
( ( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| ? [X10,X11] :
( a_select3(q_ds1_filter,X10,X11) != a_select3(q_ds1_filter,X11,X10)
& leq(n0,X10)
& leq(n0,X11)
& leq(X10,minus(n6,n1))
& leq(X11,minus(n6,n1)) )
| ? [X12,X13] :
( a_select3(r_ds1_filter,X12,X13) != a_select3(r_ds1_filter,X13,X12)
& leq(n0,X12)
& leq(n0,X13)
& leq(X12,minus(n3,n1))
& leq(X13,minus(n3,n1)) )
| ? [X14,X15] :
( a_select3(pminus_ds1_filter,X14,X15) != a_select3(pminus_ds1_filter,X15,X14)
& leq(n0,X14)
& leq(n0,X15)
& leq(X14,minus(n6,n1))
& leq(X15,minus(n6,n1)) )
| ? [X16,X17] :
( a_select3(pminus_ds1_filter,X16,X17) != a_select3(pminus_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,minus(n6,n1))
& leq(X17,minus(n6,n1)) )
| ? [X18] :
( ? [X19] :
( a_select3(id_ds1_filter,X18,X19) != a_select3(id_ds1_filter,X19,X18)
& leq(n0,X19)
& leq(X19,minus(n6,n1)) )
& leq(n0,X18)
& leq(X18,minus(n6,n1)) ) )
& leq(n0,pv5)
& leq(n0,pv47)
& leq(pv5,minus(n999,n1))
& leq(pv47,minus(n6,n1))
& ! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(n0,X0)
| ~ leq(n0,X1)
| ~ leq(X0,minus(n6,n1))
| ~ leq(X1,minus(n6,n1)) )
& ! [X2,X3] :
( a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2)
| ~ leq(n0,X2)
| ~ leq(n0,X3)
| ~ leq(X2,minus(n3,n1))
| ~ leq(X3,minus(n3,n1)) )
& ! [X4,X5] :
( a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4)
| ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,minus(n6,n1))
| ~ leq(X5,minus(n6,n1)) )
& ! [X6,X7] :
( a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6)
| ~ leq(n0,X6)
| ~ leq(n0,X7)
| ~ leq(X6,minus(n6,n1))
| ~ leq(X7,minus(n6,n1)) )
& ! [X8] :
( ! [X9] :
( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ leq(n0,X9)
| ~ leq(X9,minus(n6,n1)) )
| ~ leq(n0,X8)
| ~ leq(X8,minus(n6,n1)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f154,plain,
( ( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| ? [X10,X11] :
( a_select3(q_ds1_filter,X10,X11) != a_select3(q_ds1_filter,X11,X10)
& leq(n0,X10)
& leq(n0,X11)
& leq(X10,minus(n6,n1))
& leq(X11,minus(n6,n1)) )
| ? [X12,X13] :
( a_select3(r_ds1_filter,X12,X13) != a_select3(r_ds1_filter,X13,X12)
& leq(n0,X12)
& leq(n0,X13)
& leq(X12,minus(n3,n1))
& leq(X13,minus(n3,n1)) )
| ? [X14,X15] :
( a_select3(pminus_ds1_filter,X14,X15) != a_select3(pminus_ds1_filter,X15,X14)
& leq(n0,X14)
& leq(n0,X15)
& leq(X14,minus(n6,n1))
& leq(X15,minus(n6,n1)) )
| ? [X16,X17] :
( a_select3(pminus_ds1_filter,X16,X17) != a_select3(pminus_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,minus(n6,n1))
& leq(X17,minus(n6,n1)) )
| ? [X18] :
( ? [X19] :
( a_select3(id_ds1_filter,X18,X19) != a_select3(id_ds1_filter,X19,X18)
& leq(n0,X19)
& leq(X19,minus(n6,n1)) )
& leq(n0,X18)
& leq(X18,minus(n6,n1)) ) )
& leq(n0,pv5)
& leq(n0,pv47)
& leq(pv5,minus(n999,n1))
& leq(pv47,minus(n6,n1))
& ! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(n0,X0)
| ~ leq(n0,X1)
| ~ leq(X0,minus(n6,n1))
| ~ leq(X1,minus(n6,n1)) )
& ! [X2,X3] :
( a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2)
| ~ leq(n0,X2)
| ~ leq(n0,X3)
| ~ leq(X2,minus(n3,n1))
| ~ leq(X3,minus(n3,n1)) )
& ! [X4,X5] :
( a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4)
| ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,minus(n6,n1))
| ~ leq(X5,minus(n6,n1)) )
& ! [X6,X7] :
( a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6)
| ~ leq(n0,X6)
| ~ leq(n0,X7)
| ~ leq(X6,minus(n6,n1))
| ~ leq(X7,minus(n6,n1)) )
& ! [X8] :
( ! [X9] :
( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ leq(n0,X9)
| ~ leq(X9,minus(n6,n1)) )
| ~ leq(n0,X8)
| ~ leq(X8,minus(n6,n1)) ) ),
inference(flattening,[],[f153]) ).
fof(f176,definition,
( ? [X18] :
( ? [X19] :
( a_select3(id_ds1_filter,X18,X19) != a_select3(id_ds1_filter,X19,X18)
& leq(n0,X19)
& leq(X19,minus(n6,n1)) )
& leq(n0,X18)
& leq(X18,minus(n6,n1)) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f177,definition,
( ? [X16,X17] :
( a_select3(pminus_ds1_filter,X16,X17) != a_select3(pminus_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,minus(n6,n1))
& leq(X17,minus(n6,n1)) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f178,definition,
( ? [X14,X15] :
( a_select3(pminus_ds1_filter,X14,X15) != a_select3(pminus_ds1_filter,X15,X14)
& leq(n0,X14)
& leq(n0,X15)
& leq(X14,minus(n6,n1))
& leq(X15,minus(n6,n1)) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f179,definition,
( ? [X12,X13] :
( a_select3(r_ds1_filter,X12,X13) != a_select3(r_ds1_filter,X13,X12)
& leq(n0,X12)
& leq(n0,X13)
& leq(X12,minus(n3,n1))
& leq(X13,minus(n3,n1)) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f180,plain,
( ( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| ? [X10,X11] :
( a_select3(q_ds1_filter,X10,X11) != a_select3(q_ds1_filter,X11,X10)
& leq(n0,X10)
& leq(n0,X11)
& leq(X10,minus(n6,n1))
& leq(X11,minus(n6,n1)) )
| sP7
| sP6
| sP5
| sP4 )
& leq(n0,pv5)
& leq(n0,pv47)
& leq(pv5,minus(n999,n1))
& leq(pv47,minus(n6,n1))
& ! [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) = a_select3(q_ds1_filter,X1,X0)
| ~ leq(n0,X0)
| ~ leq(n0,X1)
| ~ leq(X0,minus(n6,n1))
| ~ leq(X1,minus(n6,n1)) )
& ! [X2,X3] :
( a_select3(r_ds1_filter,X2,X3) = a_select3(r_ds1_filter,X3,X2)
| ~ leq(n0,X2)
| ~ leq(n0,X3)
| ~ leq(X2,minus(n3,n1))
| ~ leq(X3,minus(n3,n1)) )
& ! [X4,X5] :
( a_select3(pminus_ds1_filter,X4,X5) = a_select3(pminus_ds1_filter,X5,X4)
| ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,minus(n6,n1))
| ~ leq(X5,minus(n6,n1)) )
& ! [X6,X7] :
( a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6)
| ~ leq(n0,X6)
| ~ leq(n0,X7)
| ~ leq(X6,minus(n6,n1))
| ~ leq(X7,minus(n6,n1)) )
& ! [X8] :
( ! [X9] :
( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ leq(n0,X9)
| ~ leq(X9,minus(n6,n1)) )
| ~ leq(n0,X8)
| ~ leq(X8,minus(n6,n1)) ) ),
inference(definition_folding,[],[f154,f179,f178,f177,f176]) ).
fof(f214,plain,
( ? [X12,X13] :
( a_select3(r_ds1_filter,X12,X13) != a_select3(r_ds1_filter,X13,X12)
& leq(n0,X12)
& leq(n0,X13)
& leq(X12,minus(n3,n1))
& leq(X13,minus(n3,n1)) )
| ~ sP7 ),
inference(nnf_transformation,[],[f179]) ).
fof(f215,plain,
( ? [X0,X1] :
( a_select3(r_ds1_filter,X0,X1) != a_select3(r_ds1_filter,X1,X0)
& leq(n0,X0)
& leq(n0,X1)
& leq(X0,minus(n3,n1))
& leq(X1,minus(n3,n1)) )
| ~ sP7 ),
inference(rectify,[],[f214]) ).
fof(f216,plain,
( ( a_select3(r_ds1_filter,sK35,sK36) != a_select3(r_ds1_filter,sK36,sK35)
& leq(n0,sK35)
& leq(n0,sK36)
& leq(sK35,minus(n3,n1))
& leq(sK36,minus(n3,n1)) )
| ~ sP7 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36]),skolemize(X0,sK35),skolemize(X1,sK36)],[f215]) ).
fof(f217,plain,
( ? [X14,X15] :
( a_select3(pminus_ds1_filter,X14,X15) != a_select3(pminus_ds1_filter,X15,X14)
& leq(n0,X14)
& leq(n0,X15)
& leq(X14,minus(n6,n1))
& leq(X15,minus(n6,n1)) )
| ~ sP6 ),
inference(nnf_transformation,[],[f178]) ).
fof(f218,plain,
( ? [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) != a_select3(pminus_ds1_filter,X1,X0)
& leq(n0,X0)
& leq(n0,X1)
& leq(X0,minus(n6,n1))
& leq(X1,minus(n6,n1)) )
| ~ sP6 ),
inference(rectify,[],[f217]) ).
fof(f219,plain,
( ( a_select3(pminus_ds1_filter,sK37,sK38) != a_select3(pminus_ds1_filter,sK38,sK37)
& leq(n0,sK37)
& leq(n0,sK38)
& leq(sK37,minus(n6,n1))
& leq(sK38,minus(n6,n1)) )
| ~ sP6 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37,sK38]),skolemize(X0,sK37),skolemize(X1,sK38)],[f218]) ).
fof(f220,plain,
( ? [X16,X17] :
( a_select3(pminus_ds1_filter,X16,X17) != a_select3(pminus_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,minus(n6,n1))
& leq(X17,minus(n6,n1)) )
| ~ sP5 ),
inference(nnf_transformation,[],[f177]) ).
fof(f221,plain,
( ? [X0,X1] :
( a_select3(pminus_ds1_filter,X0,X1) != a_select3(pminus_ds1_filter,X1,X0)
& leq(n0,X0)
& leq(n0,X1)
& leq(X0,minus(n6,n1))
& leq(X1,minus(n6,n1)) )
| ~ sP5 ),
inference(rectify,[],[f220]) ).
fof(f222,plain,
( ( a_select3(pminus_ds1_filter,sK39,sK40) != a_select3(pminus_ds1_filter,sK40,sK39)
& leq(n0,sK39)
& leq(n0,sK40)
& leq(sK39,minus(n6,n1))
& leq(sK40,minus(n6,n1)) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39,sK40]),skolemize(X0,sK39),skolemize(X1,sK40)],[f221]) ).
fof(f223,plain,
( ? [X18] :
( ? [X19] :
( a_select3(id_ds1_filter,X18,X19) != a_select3(id_ds1_filter,X19,X18)
& leq(n0,X19)
& leq(X19,minus(n6,n1)) )
& leq(n0,X18)
& leq(X18,minus(n6,n1)) )
| ~ sP4 ),
inference(nnf_transformation,[],[f176]) ).
fof(f224,plain,
( ? [X0] :
( ? [X1] :
( a_select3(id_ds1_filter,X0,X1) != a_select3(id_ds1_filter,X1,X0)
& leq(n0,X1)
& leq(X1,minus(n6,n1)) )
& leq(n0,X0)
& leq(X0,minus(n6,n1)) )
| ~ sP4 ),
inference(rectify,[],[f223]) ).
fof(f225,plain,
( ( a_select3(id_ds1_filter,sK41,sK42) != a_select3(id_ds1_filter,sK42,sK41)
& leq(n0,sK42)
& leq(sK42,minus(n6,n1))
& leq(n0,sK41)
& leq(sK41,minus(n6,n1)) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41,sK42]),skolemize(X0,sK41),skolemize(X1,sK42)],[f224]) ).
fof(f226,plain,
( ( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| ? [X0,X1] :
( a_select3(q_ds1_filter,X0,X1) != a_select3(q_ds1_filter,X1,X0)
& leq(n0,X0)
& leq(n0,X1)
& leq(X0,minus(n6,n1))
& leq(X1,minus(n6,n1)) )
| sP7
| sP6
| sP5
| sP4 )
& leq(n0,pv5)
& leq(n0,pv47)
& leq(pv5,minus(n999,n1))
& leq(pv47,minus(n6,n1))
& ! [X2,X3] :
( a_select3(q_ds1_filter,X2,X3) = a_select3(q_ds1_filter,X3,X2)
| ~ leq(n0,X2)
| ~ leq(n0,X3)
| ~ leq(X2,minus(n6,n1))
| ~ leq(X3,minus(n6,n1)) )
& ! [X4,X5] :
( a_select3(r_ds1_filter,X4,X5) = a_select3(r_ds1_filter,X5,X4)
| ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,minus(n3,n1))
| ~ leq(X5,minus(n3,n1)) )
& ! [X6,X7] :
( a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6)
| ~ leq(n0,X6)
| ~ leq(n0,X7)
| ~ leq(X6,minus(n6,n1))
| ~ leq(X7,minus(n6,n1)) )
& ! [X8,X9] :
( a_select3(pminus_ds1_filter,X8,X9) = a_select3(pminus_ds1_filter,X9,X8)
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,minus(n6,n1))
| ~ leq(X9,minus(n6,n1)) )
& ! [X10] :
( ! [X11] :
( a_select3(id_ds1_filter,X10,X11) = a_select3(id_ds1_filter,X11,X10)
| ~ leq(n0,X11)
| ~ leq(X11,minus(n6,n1)) )
| ~ leq(n0,X10)
| ~ leq(X10,minus(n6,n1)) ) ),
inference(rectify,[],[f180]) ).
fof(f227,plain,
( ( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| ( a_select3(q_ds1_filter,sK43,sK44) != a_select3(q_ds1_filter,sK44,sK43)
& leq(n0,sK43)
& leq(n0,sK44)
& leq(sK43,minus(n6,n1))
& leq(sK44,minus(n6,n1)) )
| sP7
| sP6
| sP5
| sP4 )
& leq(n0,pv5)
& leq(n0,pv47)
& leq(pv5,minus(n999,n1))
& leq(pv47,minus(n6,n1))
& ! [X2,X3] :
( a_select3(q_ds1_filter,X2,X3) = a_select3(q_ds1_filter,X3,X2)
| ~ leq(n0,X2)
| ~ leq(n0,X3)
| ~ leq(X2,minus(n6,n1))
| ~ leq(X3,minus(n6,n1)) )
& ! [X4,X5] :
( a_select3(r_ds1_filter,X4,X5) = a_select3(r_ds1_filter,X5,X4)
| ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,minus(n3,n1))
| ~ leq(X5,minus(n3,n1)) )
& ! [X6,X7] :
( a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6)
| ~ leq(n0,X6)
| ~ leq(n0,X7)
| ~ leq(X6,minus(n6,n1))
| ~ leq(X7,minus(n6,n1)) )
& ! [X8,X9] :
( a_select3(pminus_ds1_filter,X8,X9) = a_select3(pminus_ds1_filter,X9,X8)
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,minus(n6,n1))
| ~ leq(X9,minus(n6,n1)) )
& ! [X10] :
( ! [X11] :
( a_select3(id_ds1_filter,X10,X11) = a_select3(id_ds1_filter,X11,X10)
| ~ leq(n0,X11)
| ~ leq(X11,minus(n6,n1)) )
| ~ leq(n0,X10)
| ~ leq(X10,minus(n6,n1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43,sK44]),skolemize(X0,sK43),skolemize(X1,sK44)],[f226]) ).
fof(f338,plain,
( leq(sK36,minus(n3,n1))
| ~ sP7 ),
inference(cnf_transformation,[],[f216]) ).
fof(f339,plain,
( leq(sK35,minus(n3,n1))
| ~ sP7 ),
inference(cnf_transformation,[],[f216]) ).
fof(f340,plain,
( leq(n0,sK36)
| ~ sP7 ),
inference(cnf_transformation,[],[f216]) ).
fof(f341,plain,
( leq(n0,sK35)
| ~ sP7 ),
inference(cnf_transformation,[],[f216]) ).
fof(f342,plain,
( a_select3(r_ds1_filter,sK35,sK36) != a_select3(r_ds1_filter,sK36,sK35)
| ~ sP7 ),
inference(cnf_transformation,[],[f216]) ).
fof(f343,plain,
( leq(sK38,minus(n6,n1))
| ~ sP6 ),
inference(cnf_transformation,[],[f219]) ).
fof(f344,plain,
( leq(sK37,minus(n6,n1))
| ~ sP6 ),
inference(cnf_transformation,[],[f219]) ).
fof(f345,plain,
( leq(n0,sK38)
| ~ sP6 ),
inference(cnf_transformation,[],[f219]) ).
fof(f346,plain,
( leq(n0,sK37)
| ~ sP6 ),
inference(cnf_transformation,[],[f219]) ).
fof(f347,plain,
( a_select3(pminus_ds1_filter,sK37,sK38) != a_select3(pminus_ds1_filter,sK38,sK37)
| ~ sP6 ),
inference(cnf_transformation,[],[f219]) ).
fof(f348,plain,
( leq(sK40,minus(n6,n1))
| ~ sP5 ),
inference(cnf_transformation,[],[f222]) ).
fof(f349,plain,
( leq(sK39,minus(n6,n1))
| ~ sP5 ),
inference(cnf_transformation,[],[f222]) ).
fof(f350,plain,
( leq(n0,sK40)
| ~ sP5 ),
inference(cnf_transformation,[],[f222]) ).
fof(f351,plain,
( leq(n0,sK39)
| ~ sP5 ),
inference(cnf_transformation,[],[f222]) ).
fof(f352,plain,
( a_select3(pminus_ds1_filter,sK39,sK40) != a_select3(pminus_ds1_filter,sK40,sK39)
| ~ sP5 ),
inference(cnf_transformation,[],[f222]) ).
fof(f353,plain,
( leq(sK41,minus(n6,n1))
| ~ sP4 ),
inference(cnf_transformation,[],[f225]) ).
fof(f354,plain,
( leq(n0,sK41)
| ~ sP4 ),
inference(cnf_transformation,[],[f225]) ).
fof(f355,plain,
( leq(sK42,minus(n6,n1))
| ~ sP4 ),
inference(cnf_transformation,[],[f225]) ).
fof(f356,plain,
( leq(n0,sK42)
| ~ sP4 ),
inference(cnf_transformation,[],[f225]) ).
fof(f357,plain,
( a_select3(id_ds1_filter,sK41,sK42) != a_select3(id_ds1_filter,sK42,sK41)
| ~ sP4 ),
inference(cnf_transformation,[],[f225]) ).
fof(f358,plain,
! [X10,X11] :
( a_select3(id_ds1_filter,X10,X11) = a_select3(id_ds1_filter,X11,X10)
| ~ leq(n0,X11)
| ~ leq(X11,minus(n6,n1))
| ~ leq(n0,X10)
| ~ leq(X10,minus(n6,n1)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f359,plain,
! [X8,X9] :
( a_select3(pminus_ds1_filter,X8,X9) = a_select3(pminus_ds1_filter,X9,X8)
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,minus(n6,n1))
| ~ leq(X9,minus(n6,n1)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f361,plain,
! [X4,X5] :
( a_select3(r_ds1_filter,X4,X5) = a_select3(r_ds1_filter,X5,X4)
| ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,minus(n3,n1))
| ~ leq(X5,minus(n3,n1)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f362,plain,
! [X2,X3] :
( a_select3(q_ds1_filter,X2,X3) = a_select3(q_ds1_filter,X3,X2)
| ~ leq(n0,X2)
| ~ leq(n0,X3)
| ~ leq(X2,minus(n6,n1))
| ~ leq(X3,minus(n6,n1)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f364,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[],[f227]) ).
fof(f366,plain,
leq(n0,pv5),
inference(cnf_transformation,[],[f227]) ).
fof(f367,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(sK44,minus(n6,n1))
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f368,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(sK43,minus(n6,n1))
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f369,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(n0,sK44)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f370,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(n0,sK43)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f371,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select3(q_ds1_filter,sK43,sK44) != a_select3(q_ds1_filter,sK44,sK43)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f535,plain,
( ~ leq(n0,sK35)
| ~ sP7 ),
inference(consistent_polarity_flipping,[],[f341]) ).
fof(f536,plain,
( ~ leq(n0,sK36)
| ~ sP7 ),
inference(consistent_polarity_flipping,[],[f340]) ).
fof(f537,plain,
( ~ leq(sK35,minus(n3,n1))
| ~ sP7 ),
inference(consistent_polarity_flipping,[],[f339]) ).
fof(f538,plain,
( ~ leq(sK36,minus(n3,n1))
| ~ sP7 ),
inference(consistent_polarity_flipping,[],[f338]) ).
fof(f539,plain,
( ~ leq(n0,sK37)
| ~ sP6 ),
inference(consistent_polarity_flipping,[],[f346]) ).
fof(f540,plain,
( ~ leq(n0,sK38)
| ~ sP6 ),
inference(consistent_polarity_flipping,[],[f345]) ).
fof(f541,plain,
( ~ leq(sK37,minus(n6,n1))
| ~ sP6 ),
inference(consistent_polarity_flipping,[],[f344]) ).
fof(f542,plain,
( ~ leq(sK38,minus(n6,n1))
| ~ sP6 ),
inference(consistent_polarity_flipping,[],[f343]) ).
fof(f543,plain,
( ~ leq(n0,sK39)
| ~ sP5 ),
inference(consistent_polarity_flipping,[],[f351]) ).
fof(f544,plain,
( ~ leq(n0,sK40)
| ~ sP5 ),
inference(consistent_polarity_flipping,[],[f350]) ).
fof(f545,plain,
( ~ leq(sK39,minus(n6,n1))
| ~ sP5 ),
inference(consistent_polarity_flipping,[],[f349]) ).
fof(f546,plain,
( ~ leq(sK40,minus(n6,n1))
| ~ sP5 ),
inference(consistent_polarity_flipping,[],[f348]) ).
fof(f547,plain,
( a_select3(id_ds1_filter,sK41,sK42) != a_select3(id_ds1_filter,sK42,sK41)
| sP4 ),
inference(consistent_polarity_flipping,[],[f357]) ).
fof(f548,plain,
( ~ leq(n0,sK42)
| sP4 ),
inference(consistent_polarity_flipping,[],[f356]) ).
fof(f549,plain,
( ~ leq(sK42,minus(n6,n1))
| sP4 ),
inference(consistent_polarity_flipping,[],[f355]) ).
fof(f550,plain,
( ~ leq(n0,sK41)
| sP4 ),
inference(consistent_polarity_flipping,[],[f354]) ).
fof(f551,plain,
( ~ leq(sK41,minus(n6,n1))
| sP4 ),
inference(consistent_polarity_flipping,[],[f353]) ).
fof(f552,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| a_select3(q_ds1_filter,sK43,sK44) != a_select3(q_ds1_filter,sK44,sK43)
| sP7
| sP6
| sP5
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f371]) ).
fof(f553,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(n0,sK43)
| sP7
| sP6
| sP5
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f370]) ).
fof(f554,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(n0,sK44)
| sP7
| sP6
| sP5
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f369]) ).
fof(f555,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(sK43,minus(n6,n1))
| sP7
| sP6
| sP5
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f368]) ).
fof(f556,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(sK44,minus(n6,n1))
| sP7
| sP6
| sP5
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f367]) ).
fof(f557,plain,
~ leq(n0,pv5),
inference(consistent_polarity_flipping,[],[f366]) ).
fof(f559,plain,
~ leq(pv5,minus(n999,n1)),
inference(consistent_polarity_flipping,[],[f364]) ).
fof(f561,plain,
! [X2,X3] :
( leq(n0,X3)
| leq(n0,X2)
| a_select3(q_ds1_filter,X2,X3) = a_select3(q_ds1_filter,X3,X2)
| leq(X2,minus(n6,n1))
| leq(X3,minus(n6,n1)) ),
inference(consistent_polarity_flipping,[],[f362]) ).
fof(f562,plain,
! [X4,X5] :
( leq(n0,X5)
| leq(n0,X4)
| a_select3(r_ds1_filter,X4,X5) = a_select3(r_ds1_filter,X5,X4)
| leq(X4,minus(n3,n1))
| leq(X5,minus(n3,n1)) ),
inference(consistent_polarity_flipping,[],[f361]) ).
fof(f564,plain,
! [X8,X9] :
( leq(n0,X9)
| leq(n0,X8)
| a_select3(pminus_ds1_filter,X8,X9) = a_select3(pminus_ds1_filter,X9,X8)
| leq(X8,minus(n6,n1))
| leq(X9,minus(n6,n1)) ),
inference(consistent_polarity_flipping,[],[f359]) ).
fof(f565,plain,
! [X10,X11] :
( leq(n0,X11)
| a_select3(id_ds1_filter,X10,X11) = a_select3(id_ds1_filter,X11,X10)
| leq(X11,minus(n6,n1))
| leq(n0,X10)
| leq(X10,minus(n6,n1)) ),
inference(consistent_polarity_flipping,[],[f358]) ).
fof(f574,definition,
( spl45_1
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl45_1])],[avatar_definition]) ).
fof(f578,definition,
( spl45_2
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl45_2])],[avatar_definition]) ).
fof(f582,definition,
( spl45_3
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl45_3])],[avatar_definition]) ).
fof(f586,definition,
( spl45_4
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl45_4])],[avatar_definition]) ).
fof(f590,definition,
( spl45_5
<=> leq(sK44,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_5])],[avatar_definition]) ).
fof(f594,definition,
( spl45_6
<=> leq(pv5,minus(n999,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_6])],[avatar_definition]) ).
fof(f596,plain,
( leq(pv5,minus(n999,n1))
| ~ spl45_6 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f598,definition,
( spl45_7
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[spl45_7])],[avatar_definition]) ).
fof(f600,plain,
( leq(n0,pv5)
| ~ spl45_7 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f601,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_5
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f556,f598,f594,f590,f586,f582,f578,f574]) ).
fof(f603,definition,
( spl45_8
<=> leq(sK43,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_8])],[avatar_definition]) ).
fof(f606,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_8
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f555,f598,f594,f603,f586,f582,f578,f574]) ).
fof(f608,definition,
( spl45_9
<=> leq(n0,sK44) ),
introduced(definition,[new_symbols(definition,[spl45_9])],[avatar_definition]) ).
fof(f610,plain,
( ~ leq(n0,sK44)
| spl45_9 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f611,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_9
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f554,f598,f594,f608,f586,f582,f578,f574]) ).
fof(f613,definition,
( spl45_10
<=> leq(n0,sK43) ),
introduced(definition,[new_symbols(definition,[spl45_10])],[avatar_definition]) ).
fof(f615,plain,
( ~ leq(n0,sK43)
| spl45_10 ),
inference(avatar_component_clause,[],[f613]) ).
fof(f616,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_10
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f553,f598,f594,f613,f586,f582,f578,f574]) ).
fof(f618,definition,
( spl45_11
<=> a_select3(q_ds1_filter,sK43,sK44) = a_select3(q_ds1_filter,sK44,sK43) ),
introduced(definition,[new_symbols(definition,[spl45_11])],[avatar_definition]) ).
fof(f621,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_11
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f552,f598,f594,f618,f586,f582,f578,f574]) ).
fof(f623,definition,
( spl45_12
<=> leq(sK41,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_12])],[avatar_definition]) ).
fof(f626,plain,
( spl45_1
| ~ spl45_12 ),
inference(avatar_split_clause,[],[f551,f623,f574]) ).
fof(f628,definition,
( spl45_13
<=> leq(n0,sK41) ),
introduced(definition,[new_symbols(definition,[spl45_13])],[avatar_definition]) ).
fof(f630,plain,
( ~ leq(n0,sK41)
| spl45_13 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f631,plain,
( spl45_1
| ~ spl45_13 ),
inference(avatar_split_clause,[],[f550,f628,f574]) ).
fof(f633,definition,
( spl45_14
<=> leq(sK42,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_14])],[avatar_definition]) ).
fof(f636,plain,
( spl45_1
| ~ spl45_14 ),
inference(avatar_split_clause,[],[f549,f633,f574]) ).
fof(f638,definition,
( spl45_15
<=> leq(n0,sK42) ),
introduced(definition,[new_symbols(definition,[spl45_15])],[avatar_definition]) ).
fof(f640,plain,
( ~ leq(n0,sK42)
| spl45_15 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f641,plain,
( spl45_1
| ~ spl45_15 ),
inference(avatar_split_clause,[],[f548,f638,f574]) ).
fof(f643,definition,
( spl45_16
<=> a_select3(id_ds1_filter,sK41,sK42) = a_select3(id_ds1_filter,sK42,sK41) ),
introduced(definition,[new_symbols(definition,[spl45_16])],[avatar_definition]) ).
fof(f646,plain,
( spl45_1
| ~ spl45_16 ),
inference(avatar_split_clause,[],[f547,f643,f574]) ).
fof(f648,definition,
( spl45_17
<=> leq(sK40,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_17])],[avatar_definition]) ).
fof(f651,plain,
( ~ spl45_2
| ~ spl45_17 ),
inference(avatar_split_clause,[],[f546,f648,f578]) ).
fof(f653,definition,
( spl45_18
<=> leq(sK39,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_18])],[avatar_definition]) ).
fof(f656,plain,
( ~ spl45_2
| ~ spl45_18 ),
inference(avatar_split_clause,[],[f545,f653,f578]) ).
fof(f658,definition,
( spl45_19
<=> leq(n0,sK40) ),
introduced(definition,[new_symbols(definition,[spl45_19])],[avatar_definition]) ).
fof(f660,plain,
( ~ leq(n0,sK40)
| spl45_19 ),
inference(avatar_component_clause,[],[f658]) ).
fof(f661,plain,
( ~ spl45_2
| ~ spl45_19 ),
inference(avatar_split_clause,[],[f544,f658,f578]) ).
fof(f663,definition,
( spl45_20
<=> leq(n0,sK39) ),
introduced(definition,[new_symbols(definition,[spl45_20])],[avatar_definition]) ).
fof(f665,plain,
( ~ leq(n0,sK39)
| spl45_20 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f666,plain,
( ~ spl45_2
| ~ spl45_20 ),
inference(avatar_split_clause,[],[f543,f663,f578]) ).
fof(f668,definition,
( spl45_21
<=> a_select3(pminus_ds1_filter,sK39,sK40) = a_select3(pminus_ds1_filter,sK40,sK39) ),
introduced(definition,[new_symbols(definition,[spl45_21])],[avatar_definition]) ).
fof(f671,plain,
( ~ spl45_2
| ~ spl45_21 ),
inference(avatar_split_clause,[],[f352,f668,f578]) ).
fof(f673,definition,
( spl45_22
<=> leq(sK38,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_22])],[avatar_definition]) ).
fof(f676,plain,
( ~ spl45_3
| ~ spl45_22 ),
inference(avatar_split_clause,[],[f542,f673,f582]) ).
fof(f678,definition,
( spl45_23
<=> leq(sK37,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_23])],[avatar_definition]) ).
fof(f681,plain,
( ~ spl45_3
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f541,f678,f582]) ).
fof(f683,definition,
( spl45_24
<=> leq(n0,sK38) ),
introduced(definition,[new_symbols(definition,[spl45_24])],[avatar_definition]) ).
fof(f685,plain,
( ~ leq(n0,sK38)
| spl45_24 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f686,plain,
( ~ spl45_3
| ~ spl45_24 ),
inference(avatar_split_clause,[],[f540,f683,f582]) ).
fof(f688,definition,
( spl45_25
<=> leq(n0,sK37) ),
introduced(definition,[new_symbols(definition,[spl45_25])],[avatar_definition]) ).
fof(f690,plain,
( ~ leq(n0,sK37)
| spl45_25 ),
inference(avatar_component_clause,[],[f688]) ).
fof(f691,plain,
( ~ spl45_3
| ~ spl45_25 ),
inference(avatar_split_clause,[],[f539,f688,f582]) ).
fof(f693,definition,
( spl45_26
<=> a_select3(pminus_ds1_filter,sK37,sK38) = a_select3(pminus_ds1_filter,sK38,sK37) ),
introduced(definition,[new_symbols(definition,[spl45_26])],[avatar_definition]) ).
fof(f696,plain,
( ~ spl45_3
| ~ spl45_26 ),
inference(avatar_split_clause,[],[f347,f693,f582]) ).
fof(f698,definition,
( spl45_27
<=> leq(sK36,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_27])],[avatar_definition]) ).
fof(f701,plain,
( ~ spl45_4
| ~ spl45_27 ),
inference(avatar_split_clause,[],[f538,f698,f586]) ).
fof(f703,definition,
( spl45_28
<=> leq(sK35,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_28])],[avatar_definition]) ).
fof(f706,plain,
( ~ spl45_4
| ~ spl45_28 ),
inference(avatar_split_clause,[],[f537,f703,f586]) ).
fof(f708,definition,
( spl45_29
<=> leq(n0,sK36) ),
introduced(definition,[new_symbols(definition,[spl45_29])],[avatar_definition]) ).
fof(f710,plain,
( ~ leq(n0,sK36)
| spl45_29 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f711,plain,
( ~ spl45_4
| ~ spl45_29 ),
inference(avatar_split_clause,[],[f536,f708,f586]) ).
fof(f713,definition,
( spl45_30
<=> leq(n0,sK35) ),
introduced(definition,[new_symbols(definition,[spl45_30])],[avatar_definition]) ).
fof(f715,plain,
( ~ leq(n0,sK35)
| spl45_30 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f716,plain,
( ~ spl45_4
| ~ spl45_30 ),
inference(avatar_split_clause,[],[f535,f713,f586]) ).
fof(f718,definition,
( spl45_31
<=> a_select3(r_ds1_filter,sK35,sK36) = a_select3(r_ds1_filter,sK36,sK35) ),
introduced(definition,[new_symbols(definition,[spl45_31])],[avatar_definition]) ).
fof(f721,plain,
( ~ spl45_4
| ~ spl45_31 ),
inference(avatar_split_clause,[],[f342,f718,f586]) ).
fof(f725,plain,
( ! [X0] :
( leq(n0,X0)
| a_select3(q_ds1_filter,X0,sK44) = a_select3(q_ds1_filter,sK44,X0)
| leq(X0,minus(n6,n1))
| leq(sK44,minus(n6,n1)) )
| spl45_9 ),
inference(resolution,[],[f561,f610]) ).
fof(f727,definition,
( spl45_32
<=> ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(q_ds1_filter,X0,sK44) = a_select3(q_ds1_filter,sK44,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_32])],[avatar_definition]) ).
fof(f728,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(q_ds1_filter,X0,sK44) = a_select3(q_ds1_filter,sK44,X0) )
| ~ spl45_32 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f729,plain,
( spl45_5
| spl45_32
| spl45_9 ),
inference(avatar_split_clause,[],[f725,f608,f727,f590]) ).
fof(f897,plain,
( ! [X0] :
( a_select3(id_ds1_filter,X0,sK42) = a_select3(id_ds1_filter,sK42,X0)
| leq(sK42,minus(n6,n1))
| leq(n0,X0)
| leq(X0,minus(n6,n1)) )
| spl45_15 ),
inference(resolution,[],[f640,f565]) ).
fof(f917,definition,
( spl45_68
<=> ! [X0] :
( a_select3(id_ds1_filter,X0,sK42) = a_select3(id_ds1_filter,sK42,X0)
| leq(X0,minus(n6,n1))
| leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_68])],[avatar_definition]) ).
fof(f918,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(id_ds1_filter,X0,sK42) = a_select3(id_ds1_filter,sK42,X0) )
| ~ spl45_68 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f919,plain,
( spl45_14
| spl45_68
| spl45_15 ),
inference(avatar_split_clause,[],[f897,f638,f917,f633]) ).
fof(f980,plain,
( ! [X0] :
( leq(n0,X0)
| a_select3(pminus_ds1_filter,X0,sK39) = a_select3(pminus_ds1_filter,sK39,X0)
| leq(X0,minus(n6,n1))
| leq(sK39,minus(n6,n1)) )
| spl45_20 ),
inference(resolution,[],[f665,f564]) ).
fof(f1005,definition,
( spl45_85
<=> ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK39) = a_select3(pminus_ds1_filter,sK39,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_85])],[avatar_definition]) ).
fof(f1006,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK39) = a_select3(pminus_ds1_filter,sK39,X0) )
| ~ spl45_85 ),
inference(avatar_component_clause,[],[f1005]) ).
fof(f1007,plain,
( spl45_18
| spl45_85
| spl45_20 ),
inference(avatar_split_clause,[],[f980,f663,f1005,f653]) ).
fof(f1062,plain,
( $false
| ~ spl45_7 ),
inference(resolution,[],[f600,f557]) ).
fof(f1063,plain,
~ spl45_7,
inference(avatar_contradiction_clause,[],[f1062]) ).
fof(f1066,plain,
( ! [X0] :
( leq(n0,X0)
| a_select3(pminus_ds1_filter,X0,sK37) = a_select3(pminus_ds1_filter,sK37,X0)
| leq(X0,minus(n6,n1))
| leq(sK37,minus(n6,n1)) )
| spl45_25 ),
inference(resolution,[],[f690,f564]) ).
fof(f1091,definition,
( spl45_101
<=> ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK37) = a_select3(pminus_ds1_filter,sK37,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_101])],[avatar_definition]) ).
fof(f1092,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK37) = a_select3(pminus_ds1_filter,sK37,X0) )
| ~ spl45_101 ),
inference(avatar_component_clause,[],[f1091]) ).
fof(f1093,plain,
( spl45_23
| spl45_101
| spl45_25 ),
inference(avatar_split_clause,[],[f1066,f688,f1091,f678]) ).
fof(f1107,plain,
( ! [X0] :
( leq(n0,X0)
| a_select3(r_ds1_filter,X0,sK36) = a_select3(r_ds1_filter,sK36,X0)
| leq(X0,minus(n3,n1))
| leq(sK36,minus(n3,n1)) )
| spl45_29 ),
inference(resolution,[],[f710,f562]) ).
fof(f1141,definition,
( spl45_111
<=> ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n3,n1))
| a_select3(r_ds1_filter,X0,sK36) = a_select3(r_ds1_filter,sK36,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_111])],[avatar_definition]) ).
fof(f1142,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n3,n1))
| a_select3(r_ds1_filter,X0,sK36) = a_select3(r_ds1_filter,sK36,X0) )
| ~ spl45_111 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1143,plain,
( spl45_27
| spl45_111
| spl45_29 ),
inference(avatar_split_clause,[],[f1107,f708,f1141,f698]) ).
fof(f1228,plain,
( $false
| ~ spl45_6 ),
inference(resolution,[],[f596,f559]) ).
fof(f1229,plain,
~ spl45_6,
inference(avatar_contradiction_clause,[],[f1228]) ).
fof(f1373,plain,
( leq(sK43,minus(n6,n1))
| a_select3(q_ds1_filter,sK43,sK44) = a_select3(q_ds1_filter,sK44,sK43)
| spl45_10
| ~ spl45_32 ),
inference(resolution,[],[f728,f615]) ).
fof(f1402,plain,
( leq(sK40,minus(n6,n1))
| a_select3(pminus_ds1_filter,sK39,sK40) = a_select3(pminus_ds1_filter,sK40,sK39)
| spl45_19
| ~ spl45_85 ),
inference(resolution,[],[f1006,f660]) ).
fof(f1405,plain,
( spl45_21
| spl45_17
| spl45_19
| ~ spl45_85 ),
inference(avatar_split_clause,[],[f1402,f1005,f658,f648,f668]) ).
fof(f1522,plain,
( leq(sK38,minus(n6,n1))
| a_select3(pminus_ds1_filter,sK37,sK38) = a_select3(pminus_ds1_filter,sK38,sK37)
| spl45_24
| ~ spl45_101 ),
inference(resolution,[],[f1092,f685]) ).
fof(f1528,plain,
( spl45_26
| spl45_22
| spl45_24
| ~ spl45_101 ),
inference(avatar_split_clause,[],[f1522,f1091,f683,f673,f693]) ).
fof(f1563,plain,
( leq(sK35,minus(n3,n1))
| a_select3(r_ds1_filter,sK35,sK36) = a_select3(r_ds1_filter,sK36,sK35)
| spl45_30
| ~ spl45_111 ),
inference(resolution,[],[f1142,f715]) ).
fof(f1571,plain,
( spl45_31
| spl45_28
| spl45_30
| ~ spl45_111 ),
inference(avatar_split_clause,[],[f1563,f1141,f713,f703,f718]) ).
fof(f1687,plain,
( leq(sK41,minus(n6,n1))
| a_select3(id_ds1_filter,sK41,sK42) = a_select3(id_ds1_filter,sK42,sK41)
| spl45_13
| ~ spl45_68 ),
inference(resolution,[],[f918,f630]) ).
fof(f1690,plain,
( spl45_16
| spl45_12
| spl45_13
| ~ spl45_68 ),
inference(avatar_split_clause,[],[f1687,f917,f628,f623,f643]) ).
fof(f1705,plain,
( spl45_11
| spl45_8
| spl45_10
| ~ spl45_32 ),
inference(avatar_split_clause,[],[f1373,f727,f613,f603,f618]) ).
cnf(s1,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_5
| spl45_6
| spl45_7 ),
inference(sat_conversion,[],[f601]) ).
cnf(s2,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_8 ),
inference(sat_conversion,[],[f606]) ).
cnf(s3,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_9 ),
inference(sat_conversion,[],[f611]) ).
cnf(s4,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_10 ),
inference(sat_conversion,[],[f616]) ).
cnf(s5,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_11 ),
inference(sat_conversion,[],[f621]) ).
cnf(s6,plain,
( spl45_1
| ~ spl45_12 ),
inference(sat_conversion,[],[f626]) ).
cnf(s7,plain,
( spl45_1
| ~ spl45_13 ),
inference(sat_conversion,[],[f631]) ).
cnf(s8,plain,
( spl45_1
| ~ spl45_14 ),
inference(sat_conversion,[],[f636]) ).
cnf(s9,plain,
( spl45_1
| ~ spl45_15 ),
inference(sat_conversion,[],[f641]) ).
cnf(s10,plain,
( spl45_1
| ~ spl45_16 ),
inference(sat_conversion,[],[f646]) ).
cnf(s11,plain,
( ~ spl45_2
| ~ spl45_17 ),
inference(sat_conversion,[],[f651]) ).
cnf(s12,plain,
( ~ spl45_2
| ~ spl45_18 ),
inference(sat_conversion,[],[f656]) ).
cnf(s13,plain,
( ~ spl45_2
| ~ spl45_19 ),
inference(sat_conversion,[],[f661]) ).
cnf(s14,plain,
( ~ spl45_2
| ~ spl45_20 ),
inference(sat_conversion,[],[f666]) ).
cnf(s15,plain,
( ~ spl45_2
| ~ spl45_21 ),
inference(sat_conversion,[],[f671]) ).
cnf(s16,plain,
( ~ spl45_3
| ~ spl45_22 ),
inference(sat_conversion,[],[f676]) ).
cnf(s17,plain,
( ~ spl45_3
| ~ spl45_23 ),
inference(sat_conversion,[],[f681]) ).
cnf(s18,plain,
( ~ spl45_3
| ~ spl45_24 ),
inference(sat_conversion,[],[f686]) ).
cnf(s19,plain,
( ~ spl45_3
| ~ spl45_25 ),
inference(sat_conversion,[],[f691]) ).
cnf(s20,plain,
( ~ spl45_3
| ~ spl45_26 ),
inference(sat_conversion,[],[f696]) ).
cnf(s21,plain,
( ~ spl45_4
| ~ spl45_27 ),
inference(sat_conversion,[],[f701]) ).
cnf(s22,plain,
( ~ spl45_4
| ~ spl45_28 ),
inference(sat_conversion,[],[f706]) ).
cnf(s23,plain,
( ~ spl45_4
| ~ spl45_29 ),
inference(sat_conversion,[],[f711]) ).
cnf(s24,plain,
( ~ spl45_4
| ~ spl45_30 ),
inference(sat_conversion,[],[f716]) ).
cnf(s25,plain,
( ~ spl45_4
| ~ spl45_31 ),
inference(sat_conversion,[],[f721]) ).
cnf(s26,plain,
( spl45_5
| spl45_9
| spl45_32 ),
inference(sat_conversion,[],[f729]) ).
cnf(s54,plain,
( spl45_14
| spl45_15
| spl45_68 ),
inference(sat_conversion,[],[f919]) ).
cnf(s69,plain,
( spl45_18
| spl45_20
| spl45_85 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s79,plain,
~ spl45_7,
inference(sat_conversion,[],[f1063]) ).
cnf(s84,plain,
( spl45_23
| spl45_25
| spl45_101 ),
inference(sat_conversion,[],[f1093]) ).
cnf(s92,plain,
( spl45_27
| spl45_29
| spl45_111 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s108,plain,
~ spl45_6,
inference(sat_conversion,[],[f1229]) ).
cnf(s140,plain,
( spl45_17
| spl45_19
| spl45_21
| ~ spl45_85 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s157,plain,
( spl45_22
| spl45_24
| spl45_26
| ~ spl45_101 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s160,plain,
( spl45_28
| spl45_30
| spl45_31
| ~ spl45_111 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s177,plain,
( spl45_12
| spl45_13
| spl45_16
| ~ spl45_68 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s184,plain,
( spl45_8
| spl45_10
| spl45_11
| ~ spl45_32 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s201,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_11 ),
inference(rat,[],[s5,s79,s108]) ).
cnf(s202,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_10 ),
inference(rat,[],[s4,s79,s108]) ).
cnf(s203,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_9 ),
inference(rat,[],[s3,s79,s108]) ).
cnf(s204,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_8 ),
inference(rat,[],[s2,s79,s108]) ).
cnf(s205,plain,
( ~ spl45_1
| spl45_2
| spl45_3
| spl45_4
| ~ spl45_5 ),
inference(rat,[],[s1,s79,s108]) ).
cnf(s206,plain,
spl45_1,
inference(rat,[],[s177,s54,s6,s7,s8,s9,s10]) ).
cnf(s207,plain,
( spl45_4
| spl45_3
| spl45_2 ),
inference(rat,[],[s26,s184,s203,s202,s201,s205,s204,s206]) ).
cnf(s208,plain,
~ spl45_4,
inference(rat,[],[s92,s160,s21,s22,s23,s24,s25]) ).
cnf(s209,plain,
~ spl45_3,
inference(rat,[],[s157,s84,s16,s17,s18,s19,s20]) ).
cnf(s210,plain,
spl45_2,
inference(rat,[],[s207,s208,s209]) ).
cnf(s211,plain,
~ spl45_21,
inference(rat,[],[s15,s210]) ).
cnf(s212,plain,
~ spl45_20,
inference(rat,[],[s14,s210]) ).
cnf(s213,plain,
~ spl45_19,
inference(rat,[],[s13,s210]) ).
cnf(s214,plain,
~ spl45_18,
inference(rat,[],[s12,s210]) ).
cnf(s215,plain,
~ spl45_17,
inference(rat,[],[s11,s210]) ).
cnf(s220,plain,
spl45_85,
inference(rat,[],[s69,s212,s214]) ).
cnf(s222,plain,
$false,
inference(rat,[],[s140,s213,s211,s220,s215]) ).
fof(f1755,plain,
$false,
inference(avatar_sat_refutation,[],[s222]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV109+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.08/0.20 % Computer : n013.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 09:54:22 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 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
% 0.19/0.33 % (1065373)Will run a generic schedule for satisfiability detection.
% 0.19/0.33 % (1065378)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1804524602_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.33 % (1065379)% WARNING: option uhcvi not known.
% 0.19/0.33 % (1065379)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1429350309:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.33 % (1065384)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=762087644:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.33 % (1065380)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3535358198:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.33 % (1065381)dis+10_1_sil=32000:sp=arity:random_seed=3443280482:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.33 % (1065382)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1869628861:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.33 % (1065383)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3891895134:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.33 % TRYING [1]
% 0.19/0.33 % TRYING [2]
% 0.19/0.33 % (1065384) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1065373-1065384"...
% 0.19/0.33 % (1065382) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1065373-1065382"...
% 0.19/0.33 % TRYING [3]
% 0.19/0.33 % (1065384)...printing done.
% 0.19/0.33 % (1065382)...printing done.
% 0.19/0.33 % (1065380) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1065373-1065380"...
% 0.19/0.33 % (1065384)Refutation found. Thanks to Tanya!
% 0.19/0.33 % SZS status Theorem for theBenchmark
% 0.19/0.33 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.33 % (1065384)------------------------------
% 0.19/0.33 % (1065384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.33 % (1065384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.33 % (1065384)CaDiCaL version: 2.1.3
% 0.19/0.33 % (1065384)Termination reason: Refutation
% 0.19/0.33 % (1065384)Time elapsed: 0.030 s
% 0.19/0.33 % (1065384)Peak memory usage: 13 MB
% 0.19/0.33 % (1065384)Instructions burned: 49 (million)
% 0.19/0.33 % (1065373)Success in time 0.079 s
% 0.19/0.33 % Vampire exiting
%------------------------------------------------------------------------------