%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV115+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 : n009.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:16 PM UTC 2026
% Result : Theorem 0.18s 0.28s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 41
% Syntax : Number of formulae : 240 ( 20 unt; 40 def)
% Number of atoms : 1054 ( 115 equ)
% Maximal formula atoms : 54 ( 4 avg)
% Number of connectives : 1214 ( 400 ~; 521 |; 231 &)
% ( 36 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 41 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 20 con; 0-3 aty)
% Number of variables : 169 ( 0 sgn 121 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f53,conjecture,
( ( leq(n0,pv5)
& leq(pv5,minus(n999,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/sandbox2/benchmark/theBenchmark.p',quaternion_ds1_symm_0008) ).
fof(f54,negated_conjecture,
~ ( ( leq(n0,pv5)
& leq(pv5,minus(n999,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(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)) )
& ! [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(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)) )
& ! [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(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)) )
& ! [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(pv5,minus(n999,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(pv5,minus(n999,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(f363,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[],[f227]) ).
fof(f364,plain,
leq(n0,pv5),
inference(cnf_transformation,[],[f227]) ).
fof(f365,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(sK44,minus(n6,n1))
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f366,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(sK43,minus(n6,n1))
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f367,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(n0,sK44)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f368,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| leq(n0,sK43)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f369,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,
( a_select3(pminus_ds1_filter,sK37,sK38) != a_select3(pminus_ds1_filter,sK38,sK37)
| sP6 ),
inference(consistent_polarity_flipping,[],[f347]) ).
fof(f540,plain,
( ~ leq(n0,sK37)
| sP6 ),
inference(consistent_polarity_flipping,[],[f346]) ).
fof(f541,plain,
( ~ leq(n0,sK38)
| sP6 ),
inference(consistent_polarity_flipping,[],[f345]) ).
fof(f542,plain,
( ~ leq(sK37,minus(n6,n1))
| sP6 ),
inference(consistent_polarity_flipping,[],[f344]) ).
fof(f543,plain,
( ~ leq(sK38,minus(n6,n1))
| sP6 ),
inference(consistent_polarity_flipping,[],[f343]) ).
fof(f544,plain,
( a_select3(pminus_ds1_filter,sK39,sK40) != a_select3(pminus_ds1_filter,sK40,sK39)
| sP5 ),
inference(consistent_polarity_flipping,[],[f352]) ).
fof(f545,plain,
( ~ leq(n0,sK39)
| sP5 ),
inference(consistent_polarity_flipping,[],[f351]) ).
fof(f546,plain,
( ~ leq(n0,sK40)
| sP5 ),
inference(consistent_polarity_flipping,[],[f350]) ).
fof(f547,plain,
( ~ leq(sK39,minus(n6,n1))
| sP5 ),
inference(consistent_polarity_flipping,[],[f349]) ).
fof(f548,plain,
( ~ leq(sK40,minus(n6,n1))
| sP5 ),
inference(consistent_polarity_flipping,[],[f348]) ).
fof(f549,plain,
( ~ leq(n0,sK42)
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f356]) ).
fof(f550,plain,
( ~ leq(sK42,minus(n6,n1))
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f355]) ).
fof(f551,plain,
( ~ leq(n0,sK41)
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f354]) ).
fof(f552,plain,
( ~ leq(sK41,minus(n6,n1))
| ~ sP4 ),
inference(consistent_polarity_flipping,[],[f353]) ).
fof(f553,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,[],[f369]) ).
fof(f554,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(n0,sK43)
| sP7
| ~ sP6
| ~ sP5
| sP4 ),
inference(consistent_polarity_flipping,[],[f368]) ).
fof(f555,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(n0,sK44)
| sP7
| ~ sP6
| ~ sP5
| sP4 ),
inference(consistent_polarity_flipping,[],[f367]) ).
fof(f556,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(sK43,minus(n6,n1))
| sP7
| ~ sP6
| ~ sP5
| sP4 ),
inference(consistent_polarity_flipping,[],[f366]) ).
fof(f557,plain,
( leq(n0,pv5)
| leq(pv5,minus(n999,n1))
| ~ leq(sK44,minus(n6,n1))
| sP7
| ~ sP6
| ~ sP5
| sP4 ),
inference(consistent_polarity_flipping,[],[f365]) ).
fof(f558,plain,
~ leq(n0,pv5),
inference(consistent_polarity_flipping,[],[f364]) ).
fof(f559,plain,
~ leq(pv5,minus(n999,n1)),
inference(consistent_polarity_flipping,[],[f363]) ).
fof(f560,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(f561,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(f563,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(f564,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(f609,definition,
( spl45_1
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl45_1])],[avatar_definition]) ).
fof(f613,definition,
( spl45_2
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl45_2])],[avatar_definition]) ).
fof(f617,definition,
( spl45_3
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl45_3])],[avatar_definition]) ).
fof(f621,definition,
( spl45_4
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl45_4])],[avatar_definition]) ).
fof(f625,definition,
( spl45_5
<=> leq(sK44,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_5])],[avatar_definition]) ).
fof(f629,definition,
( spl45_6
<=> leq(pv5,minus(n999,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_6])],[avatar_definition]) ).
fof(f631,plain,
( leq(pv5,minus(n999,n1))
| ~ spl45_6 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f633,definition,
( spl45_7
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[spl45_7])],[avatar_definition]) ).
fof(f635,plain,
( leq(n0,pv5)
| ~ spl45_7 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_5
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f557,f633,f629,f625,f621,f617,f613,f609]) ).
fof(f638,definition,
( spl45_8
<=> leq(sK43,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_8])],[avatar_definition]) ).
fof(f641,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_8
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f556,f633,f629,f638,f621,f617,f613,f609]) ).
fof(f643,definition,
( spl45_9
<=> leq(n0,sK44) ),
introduced(definition,[new_symbols(definition,[spl45_9])],[avatar_definition]) ).
fof(f645,plain,
( ~ leq(n0,sK44)
| spl45_9 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_9
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f555,f633,f629,f643,f621,f617,f613,f609]) ).
fof(f648,definition,
( spl45_10
<=> leq(n0,sK43) ),
introduced(definition,[new_symbols(definition,[spl45_10])],[avatar_definition]) ).
fof(f650,plain,
( ~ leq(n0,sK43)
| spl45_10 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f651,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_10
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f554,f633,f629,f648,f621,f617,f613,f609]) ).
fof(f653,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(f656,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_11
| spl45_6
| spl45_7 ),
inference(avatar_split_clause,[],[f553,f633,f629,f653,f621,f617,f613,f609]) ).
fof(f658,definition,
( spl45_12
<=> leq(sK41,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_12])],[avatar_definition]) ).
fof(f661,plain,
( ~ spl45_1
| ~ spl45_12 ),
inference(avatar_split_clause,[],[f552,f658,f609]) ).
fof(f663,definition,
( spl45_13
<=> leq(n0,sK41) ),
introduced(definition,[new_symbols(definition,[spl45_13])],[avatar_definition]) ).
fof(f665,plain,
( ~ leq(n0,sK41)
| spl45_13 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f666,plain,
( ~ spl45_1
| ~ spl45_13 ),
inference(avatar_split_clause,[],[f551,f663,f609]) ).
fof(f668,definition,
( spl45_14
<=> leq(sK42,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_14])],[avatar_definition]) ).
fof(f671,plain,
( ~ spl45_1
| ~ spl45_14 ),
inference(avatar_split_clause,[],[f550,f668,f609]) ).
fof(f673,definition,
( spl45_15
<=> leq(n0,sK42) ),
introduced(definition,[new_symbols(definition,[spl45_15])],[avatar_definition]) ).
fof(f675,plain,
( ~ leq(n0,sK42)
| spl45_15 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f676,plain,
( ~ spl45_1
| ~ spl45_15 ),
inference(avatar_split_clause,[],[f549,f673,f609]) ).
fof(f678,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(f681,plain,
( ~ spl45_1
| ~ spl45_16 ),
inference(avatar_split_clause,[],[f357,f678,f609]) ).
fof(f683,definition,
( spl45_17
<=> leq(sK40,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_17])],[avatar_definition]) ).
fof(f686,plain,
( spl45_2
| ~ spl45_17 ),
inference(avatar_split_clause,[],[f548,f683,f613]) ).
fof(f688,definition,
( spl45_18
<=> leq(sK39,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_18])],[avatar_definition]) ).
fof(f691,plain,
( spl45_2
| ~ spl45_18 ),
inference(avatar_split_clause,[],[f547,f688,f613]) ).
fof(f693,definition,
( spl45_19
<=> leq(n0,sK40) ),
introduced(definition,[new_symbols(definition,[spl45_19])],[avatar_definition]) ).
fof(f695,plain,
( ~ leq(n0,sK40)
| spl45_19 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f696,plain,
( spl45_2
| ~ spl45_19 ),
inference(avatar_split_clause,[],[f546,f693,f613]) ).
fof(f698,definition,
( spl45_20
<=> leq(n0,sK39) ),
introduced(definition,[new_symbols(definition,[spl45_20])],[avatar_definition]) ).
fof(f700,plain,
( ~ leq(n0,sK39)
| spl45_20 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f701,plain,
( spl45_2
| ~ spl45_20 ),
inference(avatar_split_clause,[],[f545,f698,f613]) ).
fof(f703,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(f706,plain,
( spl45_2
| ~ spl45_21 ),
inference(avatar_split_clause,[],[f544,f703,f613]) ).
fof(f708,definition,
( spl45_22
<=> leq(sK38,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_22])],[avatar_definition]) ).
fof(f711,plain,
( spl45_3
| ~ spl45_22 ),
inference(avatar_split_clause,[],[f543,f708,f617]) ).
fof(f713,definition,
( spl45_23
<=> leq(sK37,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_23])],[avatar_definition]) ).
fof(f716,plain,
( spl45_3
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f542,f713,f617]) ).
fof(f718,definition,
( spl45_24
<=> leq(n0,sK38) ),
introduced(definition,[new_symbols(definition,[spl45_24])],[avatar_definition]) ).
fof(f720,plain,
( ~ leq(n0,sK38)
| spl45_24 ),
inference(avatar_component_clause,[],[f718]) ).
fof(f721,plain,
( spl45_3
| ~ spl45_24 ),
inference(avatar_split_clause,[],[f541,f718,f617]) ).
fof(f723,definition,
( spl45_25
<=> leq(n0,sK37) ),
introduced(definition,[new_symbols(definition,[spl45_25])],[avatar_definition]) ).
fof(f725,plain,
( ~ leq(n0,sK37)
| spl45_25 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,plain,
( spl45_3
| ~ spl45_25 ),
inference(avatar_split_clause,[],[f540,f723,f617]) ).
fof(f728,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(f731,plain,
( spl45_3
| ~ spl45_26 ),
inference(avatar_split_clause,[],[f539,f728,f617]) ).
fof(f733,definition,
( spl45_27
<=> leq(sK36,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_27])],[avatar_definition]) ).
fof(f736,plain,
( ~ spl45_4
| ~ spl45_27 ),
inference(avatar_split_clause,[],[f538,f733,f621]) ).
fof(f738,definition,
( spl45_28
<=> leq(sK35,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_28])],[avatar_definition]) ).
fof(f741,plain,
( ~ spl45_4
| ~ spl45_28 ),
inference(avatar_split_clause,[],[f537,f738,f621]) ).
fof(f743,definition,
( spl45_29
<=> leq(n0,sK36) ),
introduced(definition,[new_symbols(definition,[spl45_29])],[avatar_definition]) ).
fof(f745,plain,
( ~ leq(n0,sK36)
| spl45_29 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f746,plain,
( ~ spl45_4
| ~ spl45_29 ),
inference(avatar_split_clause,[],[f536,f743,f621]) ).
fof(f748,definition,
( spl45_30
<=> leq(n0,sK35) ),
introduced(definition,[new_symbols(definition,[spl45_30])],[avatar_definition]) ).
fof(f750,plain,
( ~ leq(n0,sK35)
| spl45_30 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f751,plain,
( ~ spl45_4
| ~ spl45_30 ),
inference(avatar_split_clause,[],[f535,f748,f621]) ).
fof(f753,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(f756,plain,
( ~ spl45_4
| ~ spl45_31 ),
inference(avatar_split_clause,[],[f342,f753,f621]) ).
fof(f759,plain,
( ! [X0] :
( leq(n0,X0)
| a_select3(q_ds1_filter,X0,sK43) = a_select3(q_ds1_filter,sK43,X0)
| leq(X0,minus(n6,n1))
| leq(sK43,minus(n6,n1)) )
| spl45_10 ),
inference(resolution,[],[f560,f650]) ).
fof(f761,definition,
( spl45_32
<=> ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(q_ds1_filter,X0,sK43) = a_select3(q_ds1_filter,sK43,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_32])],[avatar_definition]) ).
fof(f762,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(q_ds1_filter,X0,sK43) = a_select3(q_ds1_filter,sK43,X0) )
| ~ spl45_32 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f763,plain,
( spl45_8
| spl45_32
| spl45_10 ),
inference(avatar_split_clause,[],[f759,f648,f761,f638]) ).
fof(f833,plain,
( ! [X0] :
( a_select3(id_ds1_filter,X0,sK41) = a_select3(id_ds1_filter,sK41,X0)
| leq(sK41,minus(n6,n1))
| leq(n0,X0)
| leq(X0,minus(n6,n1)) )
| spl45_13 ),
inference(resolution,[],[f665,f564]) ).
fof(f854,definition,
( spl45_52
<=> ! [X0] :
( a_select3(id_ds1_filter,X0,sK41) = a_select3(id_ds1_filter,sK41,X0)
| leq(X0,minus(n6,n1))
| leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_52])],[avatar_definition]) ).
fof(f855,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(id_ds1_filter,X0,sK41) = a_select3(id_ds1_filter,sK41,X0) )
| ~ spl45_52 ),
inference(avatar_component_clause,[],[f854]) ).
fof(f856,plain,
( spl45_12
| spl45_52
| spl45_13 ),
inference(avatar_split_clause,[],[f833,f663,f854,f658]) ).
fof(f906,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,[],[f700,f563]) ).
fof(f922,definition,
( spl45_66
<=> ! [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_66])],[avatar_definition]) ).
fof(f923,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_66 ),
inference(avatar_component_clause,[],[f922]) ).
fof(f924,plain,
( spl45_18
| spl45_66
| spl45_20 ),
inference(avatar_split_clause,[],[f906,f698,f922,f688]) ).
fof(f930,plain,
( ! [X0] :
( leq(n0,X0)
| a_select3(pminus_ds1_filter,X0,sK38) = a_select3(pminus_ds1_filter,sK38,X0)
| leq(X0,minus(n6,n1))
| leq(sK38,minus(n6,n1)) )
| spl45_24 ),
inference(resolution,[],[f720,f563]) ).
fof(f946,definition,
( spl45_71
<=> ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK38) = a_select3(pminus_ds1_filter,sK38,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_71])],[avatar_definition]) ).
fof(f947,plain,
( ! [X0] :
( leq(n0,X0)
| leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK38) = a_select3(pminus_ds1_filter,sK38,X0) )
| ~ spl45_71 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f948,plain,
( spl45_22
| spl45_71
| spl45_24 ),
inference(avatar_split_clause,[],[f930,f718,f946,f708]) ).
fof(f979,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,[],[f745,f561]) ).
fof(f990,definition,
( spl45_80
<=> ! [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_80])],[avatar_definition]) ).
fof(f991,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_80 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f992,plain,
( spl45_27
| spl45_80
| spl45_29 ),
inference(avatar_split_clause,[],[f979,f743,f990,f733]) ).
fof(f1001,plain,
( $false
| ~ spl45_6 ),
inference(resolution,[],[f631,f559]) ).
fof(f1002,plain,
~ spl45_6,
inference(avatar_contradiction_clause,[],[f1001]) ).
fof(f1003,plain,
( $false
| ~ spl45_7 ),
inference(resolution,[],[f635,f558]) ).
fof(f1004,plain,
~ spl45_7,
inference(avatar_contradiction_clause,[],[f1003]) ).
fof(f1025,plain,
( leq(sK40,minus(n6,n1))
| a_select3(pminus_ds1_filter,sK39,sK40) = a_select3(pminus_ds1_filter,sK40,sK39)
| spl45_19
| ~ spl45_66 ),
inference(resolution,[],[f695,f923]) ).
fof(f1032,plain,
( spl45_21
| spl45_17
| spl45_19
| ~ spl45_66 ),
inference(avatar_split_clause,[],[f1025,f922,f693,f683,f703]) ).
fof(f1118,plain,
( leq(sK42,minus(n6,n1))
| a_select3(id_ds1_filter,sK41,sK42) = a_select3(id_ds1_filter,sK42,sK41)
| spl45_15
| ~ spl45_52 ),
inference(resolution,[],[f675,f855]) ).
fof(f1129,plain,
( spl45_16
| spl45_14
| spl45_15
| ~ spl45_52 ),
inference(avatar_split_clause,[],[f1118,f854,f673,f668,f678]) ).
fof(f1183,plain,
( leq(sK35,minus(n3,n1))
| a_select3(r_ds1_filter,sK35,sK36) = a_select3(r_ds1_filter,sK36,sK35)
| spl45_30
| ~ spl45_80 ),
inference(resolution,[],[f750,f991]) ).
fof(f1184,plain,
( spl45_31
| spl45_28
| spl45_30
| ~ spl45_80 ),
inference(avatar_split_clause,[],[f1183,f990,f748,f738,f753]) ).
fof(f1377,plain,
( leq(sK44,minus(n6,n1))
| a_select3(q_ds1_filter,sK43,sK44) = a_select3(q_ds1_filter,sK44,sK43)
| spl45_9
| ~ spl45_32 ),
inference(resolution,[],[f762,f645]) ).
fof(f1379,plain,
( spl45_11
| spl45_5
| spl45_9
| ~ spl45_32 ),
inference(avatar_split_clause,[],[f1377,f761,f643,f625,f653]) ).
fof(f1506,plain,
( leq(sK37,minus(n6,n1))
| a_select3(pminus_ds1_filter,sK37,sK38) = a_select3(pminus_ds1_filter,sK38,sK37)
| spl45_25
| ~ spl45_71 ),
inference(resolution,[],[f725,f947]) ).
fof(f1508,plain,
( spl45_26
| spl45_23
| spl45_25
| ~ spl45_71 ),
inference(avatar_split_clause,[],[f1506,f946,f723,f713,f728]) ).
cnf(s1,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_5
| spl45_6
| spl45_7 ),
inference(sat_conversion,[],[f636]) ).
cnf(s2,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_8 ),
inference(sat_conversion,[],[f641]) ).
cnf(s3,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_9 ),
inference(sat_conversion,[],[f646]) ).
cnf(s4,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_10 ),
inference(sat_conversion,[],[f651]) ).
cnf(s5,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| spl45_6
| spl45_7
| ~ spl45_11 ),
inference(sat_conversion,[],[f656]) ).
cnf(s6,plain,
( ~ spl45_1
| ~ spl45_12 ),
inference(sat_conversion,[],[f661]) ).
cnf(s7,plain,
( ~ spl45_1
| ~ spl45_13 ),
inference(sat_conversion,[],[f666]) ).
cnf(s8,plain,
( ~ spl45_1
| ~ spl45_14 ),
inference(sat_conversion,[],[f671]) ).
cnf(s9,plain,
( ~ spl45_1
| ~ spl45_15 ),
inference(sat_conversion,[],[f676]) ).
cnf(s10,plain,
( ~ spl45_1
| ~ spl45_16 ),
inference(sat_conversion,[],[f681]) ).
cnf(s11,plain,
( spl45_2
| ~ spl45_17 ),
inference(sat_conversion,[],[f686]) ).
cnf(s12,plain,
( spl45_2
| ~ spl45_18 ),
inference(sat_conversion,[],[f691]) ).
cnf(s13,plain,
( spl45_2
| ~ spl45_19 ),
inference(sat_conversion,[],[f696]) ).
cnf(s14,plain,
( spl45_2
| ~ spl45_20 ),
inference(sat_conversion,[],[f701]) ).
cnf(s15,plain,
( spl45_2
| ~ spl45_21 ),
inference(sat_conversion,[],[f706]) ).
cnf(s16,plain,
( spl45_3
| ~ spl45_22 ),
inference(sat_conversion,[],[f711]) ).
cnf(s17,plain,
( spl45_3
| ~ spl45_23 ),
inference(sat_conversion,[],[f716]) ).
cnf(s18,plain,
( spl45_3
| ~ spl45_24 ),
inference(sat_conversion,[],[f721]) ).
cnf(s19,plain,
( spl45_3
| ~ spl45_25 ),
inference(sat_conversion,[],[f726]) ).
cnf(s20,plain,
( spl45_3
| ~ spl45_26 ),
inference(sat_conversion,[],[f731]) ).
cnf(s21,plain,
( ~ spl45_4
| ~ spl45_27 ),
inference(sat_conversion,[],[f736]) ).
cnf(s22,plain,
( ~ spl45_4
| ~ spl45_28 ),
inference(sat_conversion,[],[f741]) ).
cnf(s23,plain,
( ~ spl45_4
| ~ spl45_29 ),
inference(sat_conversion,[],[f746]) ).
cnf(s24,plain,
( ~ spl45_4
| ~ spl45_30 ),
inference(sat_conversion,[],[f751]) ).
cnf(s25,plain,
( ~ spl45_4
| ~ spl45_31 ),
inference(sat_conversion,[],[f756]) ).
cnf(s26,plain,
( spl45_8
| spl45_10
| spl45_32 ),
inference(sat_conversion,[],[f763]) ).
cnf(s39,plain,
( spl45_12
| spl45_13
| spl45_52 ),
inference(sat_conversion,[],[f856]) ).
cnf(s50,plain,
( spl45_18
| spl45_20
| spl45_66 ),
inference(sat_conversion,[],[f924]) ).
cnf(s54,plain,
( spl45_22
| spl45_24
| spl45_71 ),
inference(sat_conversion,[],[f948]) ).
cnf(s61,plain,
( spl45_27
| spl45_29
| spl45_80 ),
inference(sat_conversion,[],[f992]) ).
cnf(s64,plain,
~ spl45_6,
inference(sat_conversion,[],[f1002]) ).
cnf(s65,plain,
~ spl45_7,
inference(sat_conversion,[],[f1004]) ).
cnf(s67,plain,
( spl45_17
| spl45_19
| spl45_21
| ~ spl45_66 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s77,plain,
( spl45_14
| spl45_15
| spl45_16
| ~ spl45_52 ),
inference(sat_conversion,[],[f1129]) ).
cnf(s78,plain,
( spl45_28
| spl45_30
| spl45_31
| ~ spl45_80 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s114,plain,
( spl45_5
| spl45_9
| spl45_11
| ~ spl45_32 ),
inference(sat_conversion,[],[f1379]) ).
cnf(s128,plain,
( spl45_23
| spl45_25
| spl45_26
| ~ spl45_71 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s141,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_11 ),
inference(rat,[],[s5,s65,s64]) ).
cnf(s142,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_10 ),
inference(rat,[],[s4,s65,s64]) ).
cnf(s143,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_9 ),
inference(rat,[],[s3,s65,s64]) ).
cnf(s144,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_8 ),
inference(rat,[],[s2,s65,s64]) ).
cnf(s145,plain,
( spl45_1
| ~ spl45_2
| ~ spl45_3
| spl45_4
| ~ spl45_5 ),
inference(rat,[],[s1,s65,s64]) ).
cnf(s146,plain,
spl45_2,
inference(rat,[],[s67,s50,s11,s12,s13,s14,s15]) ).
cnf(s147,plain,
spl45_3,
inference(rat,[],[s54,s128,s16,s17,s18,s19,s20]) ).
cnf(s148,plain,
( spl45_4
| spl45_1 ),
inference(rat,[],[s114,s26,s143,s142,s141,s145,s144,s147,s146]) ).
cnf(s149,plain,
~ spl45_4,
inference(rat,[],[s61,s78,s21,s22,s23,s24,s25]) ).
cnf(s150,plain,
spl45_1,
inference(rat,[],[s148,s149]) ).
cnf(s151,plain,
~ spl45_16,
inference(rat,[],[s10,s150]) ).
cnf(s152,plain,
~ spl45_15,
inference(rat,[],[s9,s150]) ).
cnf(s153,plain,
~ spl45_14,
inference(rat,[],[s8,s150]) ).
cnf(s154,plain,
~ spl45_13,
inference(rat,[],[s7,s150]) ).
cnf(s155,plain,
~ spl45_12,
inference(rat,[],[s6,s150]) ).
cnf(s156,plain,
~ spl45_52,
inference(rat,[],[s77,s152,s151,s153]) ).
cnf(s160,plain,
$false,
inference(rat,[],[s39,s156,s154,s155]) ).
fof(f1569,plain,
$false,
inference(avatar_sat_refutation,[],[s160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV115+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n009.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 09:57:27 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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.18/0.28 % (2930567)Will run a generic schedule for satisfiability detection.
% 0.18/0.28 % (2930572)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1585444079_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.28 % (2930573)% WARNING: option uhcvi not known.
% 0.18/0.28 % (2930573)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3146356323:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.28 % (2930574)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2533061973:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.28 % (2930575)dis+10_1_sil=32000:sp=arity:random_seed=3015583055:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.28 % (2930576)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=772914625:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.28 % (2930578)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2803060277:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.28 % (2930577)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1950742974:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.28 % TRYING [1]
% 0.18/0.28 % TRYING [2]
% 0.18/0.28 % (2930578) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2930567-2930578"...
% 0.18/0.28 % (2930576) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2930567-2930576"...
% 0.18/0.28 % TRYING [3]
% 0.18/0.28 % (2930574) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2930567-2930574"...
% 0.18/0.28 % (2930578)...printing done.
% 0.18/0.28 % (2930576)...printing done.
% 0.18/0.28 % (2930578)Refutation found. Thanks to Tanya!
% 0.18/0.28 % SZS status Theorem for theBenchmark
% 0.18/0.28 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.28 % (2930578)------------------------------
% 0.18/0.28 % (2930578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.28 % (2930578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.28 % (2930578)CaDiCaL version: 2.1.3
% 0.18/0.28 % (2930578)Termination reason: Refutation
% 0.18/0.28 % (2930578)Time elapsed: 0.025 s
% 0.18/0.28 % (2930578)Peak memory usage: 13 MB
% 0.18/0.28 % (2930578)Instructions burned: 41 (million)
% 0.18/0.28 % (2930567)Success in time 0.061 s
% 0.18/0.28 % Vampire exiting
%------------------------------------------------------------------------------