%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV111+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 : n007.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 177.16s 27.61s
% Output : Refutation 177.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 136
% Syntax : Number of formulae : 660 ( 107 unt; 97 def)
% Number of atoms : 2245 ( 364 equ)
% Maximal formula atoms : 62 ( 3 avg)
% Number of connectives : 2549 ( 964 ~;1176 |; 270 &)
% ( 97 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 102 ( 100 usr; 98 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 25 con; 0-3 aty)
% Number of variables : 301 ( 0 sgn 253 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( gt(X0,X1)
| gt(X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',totality) ).
fof(f3,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
fof(f4,axiom,
! [X0] : leq(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',reflexivity_leq) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( leq(X0,X1)
& leq(X1,X2) )
=> leq(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',transitivity_leq) ).
fof(f6,axiom,
! [X0,X1] :
( lt(X0,X1)
<=> gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',lt_gt) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(f9,axiom,
! [X0,X1] :
( ( leq(X0,X1)
& X0 != X1 )
=> gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt2) ).
fof(f10,axiom,
! [X0,X1] :
( leq(X0,pred(X1))
<=> gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt_pred) ).
fof(f13,axiom,
! [X0,X1] :
( leq(X0,X1)
<=> gt(succ(X1),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_succ_gt_equiv) ).
fof(f28,axiom,
succ(tptp_minus_1) = n0,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_tptp_minus_1) ).
fof(f29,axiom,
! [X0] : plus(X0,n1) = succ(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_plus_1_r) ).
fof(f30,axiom,
! [X0] : plus(n1,X0) = succ(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_plus_1_l) ).
fof(f39,axiom,
! [X0] : minus(X0,n1) = pred(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',pred_minus_1) ).
fof(f40,axiom,
! [X0] : pred(succ(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',pred_succ) ).
fof(f41,axiom,
! [X0] : succ(pred(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',succ_pred) ).
fof(f42,axiom,
! [X0,X1] :
( leq(succ(X0),succ(X1))
<=> leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_succ_succ) ).
fof(f43,axiom,
! [X0,X1] :
( leq(succ(X0),X1)
=> gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_succ_gt) ).
fof(f53,conjecture,
( ( leq(n0,pv5)
& leq(n0,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,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)) )
=> ( ( ( lt(X7,plus(n1,minus(n6,n1)))
& X6 = pv57 )
=> a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6) )
& ( lt(X6,pv57)
=> a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6) ) ) )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,minus(pv57,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(n0,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,minus(n6,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,pv57)
& leq(X17,minus(n6,n1)) )
=> a_select3(id_ds1_filter,X16,X17) = a_select3(id_ds1_filter,X17,X16) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,minus(pv57,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_0004) ).
fof(f54,negated_conjecture,
~ ( ( leq(n0,pv5)
& leq(n0,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,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)) )
=> ( ( ( lt(X7,plus(n1,minus(n6,n1)))
& X6 = pv57 )
=> a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6) )
& ( lt(X6,pv57)
=> a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6) ) ) )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,minus(pv57,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(n0,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,minus(n6,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,pv57)
& leq(X17,minus(n6,n1)) )
=> a_select3(id_ds1_filter,X16,X17) = a_select3(id_ds1_filter,X17,X16) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,minus(pv57,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(f55,axiom,
gt(n5,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_4) ).
fof(f69,axiom,
gt(n4,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_0) ).
fof(f71,axiom,
gt(n6,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_6_0) ).
fof(f73,axiom,
gt(n1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_1_0) ).
fof(f74,axiom,
gt(n2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_0) ).
fof(f75,axiom,
gt(n3,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_0) ).
fof(f76,axiom,
gt(n4,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_1) ).
fof(f77,axiom,
gt(n5,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_1) ).
fof(f80,axiom,
gt(n2,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_1) ).
fof(f86,axiom,
gt(n3,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_2) ).
fof(f87,axiom,
gt(n4,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_3) ).
fof(f88,axiom,
gt(n5,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_3) ).
fof(f91,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n4) )
=> ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_4) ).
fof(f92,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n5) )
=> ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_5) ).
fof(f93,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n6) )
=> ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_6) ).
fof(f94,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n0) )
=> X0 = n0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_0) ).
fof(f95,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n1) )
=> ( X0 = n0
| X0 = n1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_1) ).
fof(f96,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ( X0 = n0
| X0 = n1
| X0 = n2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_2) ).
fof(f97,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n3) )
=> ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_domain_3) ).
fof(f101,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_1) ).
fof(f102,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_2) ).
fof(f112,plain,
! [X0,X1] :
( gt(X1,X0)
=> lt(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f6]) ).
fof(f116,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f117,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(flattening,[],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( lt(X0,X1)
| ~ gt(X1,X0) ),
inference(ennf_transformation,[],[f112]) ).
fof(f119,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(X1,X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f120,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f9]) ).
fof(f121,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f120]) ).
fof(f145,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(succ(X0),X1) ),
inference(ennf_transformation,[],[f43]) ).
fof(f155,plain,
( ( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,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(id_ds1_filter,X16,X17) != a_select3(id_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,pv57)
& 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(pv57,n1)) ) )
& leq(n0,pv5)
& leq(n0,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,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(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| ~ lt(X7,plus(n1,minus(n6,n1)))
| pv57 != X6 )
& ( a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| ~ lt(X6,pv57) ) )
| ~ 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(pv57,n1)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f156,plain,
( ( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,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(id_ds1_filter,X16,X17) != a_select3(id_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,pv57)
& 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(pv57,n1)) ) )
& leq(n0,pv5)
& leq(n0,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,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(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| ~ lt(X7,plus(n1,minus(n6,n1)))
| pv57 != X6 )
& ( a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| ~ lt(X6,pv57) ) )
| ~ 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(pv57,n1)) ) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| ~ leq(n0,X0)
| ~ leq(X0,n4) ),
inference(ennf_transformation,[],[f91]) ).
fof(f158,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| ~ leq(n0,X0)
| ~ leq(X0,n4) ),
inference(flattening,[],[f157]) ).
fof(f159,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| ~ leq(n0,X0)
| ~ leq(X0,n5) ),
inference(ennf_transformation,[],[f92]) ).
fof(f160,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| ~ leq(n0,X0)
| ~ leq(X0,n5) ),
inference(flattening,[],[f159]) ).
fof(f161,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6
| ~ leq(n0,X0)
| ~ leq(X0,n6) ),
inference(ennf_transformation,[],[f93]) ).
fof(f162,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6
| ~ leq(n0,X0)
| ~ leq(X0,n6) ),
inference(flattening,[],[f161]) ).
fof(f163,plain,
! [X0] :
( X0 = n0
| ~ leq(n0,X0)
| ~ leq(X0,n0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f164,plain,
! [X0] :
( X0 = n0
| ~ leq(n0,X0)
| ~ leq(X0,n0) ),
inference(flattening,[],[f163]) ).
fof(f165,plain,
! [X0] :
( X0 = n0
| X0 = n1
| ~ leq(n0,X0)
| ~ leq(X0,n1) ),
inference(ennf_transformation,[],[f95]) ).
fof(f166,plain,
! [X0] :
( X0 = n0
| X0 = n1
| ~ leq(n0,X0)
| ~ leq(X0,n1) ),
inference(flattening,[],[f165]) ).
fof(f167,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(ennf_transformation,[],[f96]) ).
fof(f168,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(flattening,[],[f167]) ).
fof(f169,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| ~ leq(n0,X0)
| ~ leq(X0,n3) ),
inference(ennf_transformation,[],[f97]) ).
fof(f170,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| ~ leq(n0,X0)
| ~ leq(X0,n3) ),
inference(flattening,[],[f169]) ).
fof(f178,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(pv57,n1)) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f179,definition,
( ? [X16,X17] :
( a_select3(id_ds1_filter,X16,X17) != a_select3(id_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,pv57)
& leq(X17,minus(n6,n1)) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f180,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(f181,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(f182,plain,
( ( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,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,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,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(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| ~ lt(X7,plus(n1,minus(n6,n1)))
| pv57 != X6 )
& ( a_select3(id_ds1_filter,X6,X7) = a_select3(id_ds1_filter,X7,X6)
| ~ lt(X6,pv57) ) )
| ~ 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(pv57,n1)) ) ),
inference(definition_folding,[],[f156,f181,f180,f179,f178]) ).
fof(f183,plain,
! [X0,X1] :
( ( leq(X0,pred(X1))
| ~ gt(X1,X0) )
& ( gt(X1,X0)
| ~ leq(X0,pred(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f184,plain,
! [X0,X1] :
( ( leq(X0,X1)
| ~ gt(succ(X1),X0) )
& ( gt(succ(X1),X0)
| ~ leq(X0,X1) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f213,plain,
! [X0,X1] :
( ( leq(succ(X0),succ(X1))
| ~ leq(X0,X1) )
& ( leq(X0,X1)
| ~ leq(succ(X0),succ(X1)) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f216,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,[],[f181]) ).
fof(f217,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,[],[f216]) ).
fof(f218,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)],[f217]) ).
fof(f219,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,[],[f180]) ).
fof(f220,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,[],[f219]) ).
fof(f221,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)],[f220]) ).
fof(f222,plain,
( ? [X16,X17] :
( a_select3(id_ds1_filter,X16,X17) != a_select3(id_ds1_filter,X17,X16)
& leq(n0,X16)
& leq(n0,X17)
& leq(X16,pv57)
& leq(X17,minus(n6,n1)) )
| ~ sP5 ),
inference(nnf_transformation,[],[f179]) ).
fof(f223,plain,
( ? [X0,X1] :
( a_select3(id_ds1_filter,X0,X1) != a_select3(id_ds1_filter,X1,X0)
& leq(n0,X0)
& leq(n0,X1)
& leq(X0,pv57)
& leq(X1,minus(n6,n1)) )
| ~ sP5 ),
inference(rectify,[],[f222]) ).
fof(f224,plain,
( ( a_select3(id_ds1_filter,sK39,sK40) != a_select3(id_ds1_filter,sK40,sK39)
& leq(n0,sK39)
& leq(n0,sK40)
& leq(sK39,pv57)
& leq(sK40,minus(n6,n1)) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39,sK40]),skolemize(X0,sK39),skolemize(X1,sK40)],[f223]) ).
fof(f225,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(pv57,n1)) )
| ~ sP4 ),
inference(nnf_transformation,[],[f178]) ).
fof(f226,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(pv57,n1)) )
| ~ sP4 ),
inference(rectify,[],[f225]) ).
fof(f227,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(pv57,n1)) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41,sK42]),skolemize(X0,sK41),skolemize(X1,sK42)],[f226]) ).
fof(f228,plain,
( ( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,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)) )
| sP7
| sP6
| sP5
| sP4 )
& leq(n0,pv5)
& leq(n0,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,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(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ lt(X9,plus(n1,minus(n6,n1)))
| pv57 != X8 )
& ( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ lt(X8,pv57) ) )
| ~ 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(pv57,n1)) ) ),
inference(rectify,[],[f182]) ).
fof(f229,plain,
( ( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,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,pv57)
& leq(pv5,minus(n999,n1))
& leq(pv57,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(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ lt(X9,plus(n1,minus(n6,n1)))
| pv57 != X8 )
& ( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ lt(X8,pv57) ) )
| ~ 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(pv57,n1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43,sK44]),skolemize(X0,sK43),skolemize(X1,sK44)],[f228]) ).
fof(f230,plain,
! [X0,X1] :
( gt(X1,X0)
| gt(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f1]) ).
fof(f232,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f233,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f234,plain,
! [X2,X0,X1] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f235,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| lt(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f236,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f237,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| gt(X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f121]) ).
fof(f238,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,pred(X1)) ),
inference(cnf_transformation,[],[f183]) ).
fof(f239,plain,
! [X0,X1] :
( leq(X0,pred(X1))
| ~ gt(X1,X0) ),
inference(cnf_transformation,[],[f183]) ).
fof(f242,plain,
! [X0,X1] :
( gt(succ(X1),X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f184]) ).
fof(f243,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(succ(X1),X0) ),
inference(cnf_transformation,[],[f184]) ).
fof(f310,plain,
n0 = succ(tptp_minus_1),
inference(cnf_transformation,[],[f28]) ).
fof(f311,plain,
! [X0] : succ(X0) = plus(X0,n1),
inference(cnf_transformation,[],[f29]) ).
fof(f312,plain,
! [X0] : succ(X0) = plus(n1,X0),
inference(cnf_transformation,[],[f30]) ).
fof(f321,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[],[f39]) ).
fof(f322,plain,
! [X0] : pred(succ(X0)) = X0,
inference(cnf_transformation,[],[f40]) ).
fof(f323,plain,
! [X0] : succ(pred(X0)) = X0,
inference(cnf_transformation,[],[f41]) ).
fof(f325,plain,
! [X0,X1] :
( leq(succ(X0),succ(X1))
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f213]) ).
fof(f326,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(succ(X0),X1) ),
inference(cnf_transformation,[],[f145]) ).
fof(f341,plain,
( leq(sK36,minus(n3,n1))
| ~ sP7 ),
inference(cnf_transformation,[],[f218]) ).
fof(f342,plain,
( leq(sK35,minus(n3,n1))
| ~ sP7 ),
inference(cnf_transformation,[],[f218]) ).
fof(f343,plain,
( leq(n0,sK36)
| ~ sP7 ),
inference(cnf_transformation,[],[f218]) ).
fof(f344,plain,
( leq(n0,sK35)
| ~ sP7 ),
inference(cnf_transformation,[],[f218]) ).
fof(f345,plain,
( a_select3(r_ds1_filter,sK35,sK36) != a_select3(r_ds1_filter,sK36,sK35)
| ~ sP7 ),
inference(cnf_transformation,[],[f218]) ).
fof(f346,plain,
( leq(sK38,minus(n6,n1))
| ~ sP6 ),
inference(cnf_transformation,[],[f221]) ).
fof(f347,plain,
( leq(sK37,minus(n6,n1))
| ~ sP6 ),
inference(cnf_transformation,[],[f221]) ).
fof(f348,plain,
( leq(n0,sK38)
| ~ sP6 ),
inference(cnf_transformation,[],[f221]) ).
fof(f349,plain,
( leq(n0,sK37)
| ~ sP6 ),
inference(cnf_transformation,[],[f221]) ).
fof(f350,plain,
( a_select3(pminus_ds1_filter,sK37,sK38) != a_select3(pminus_ds1_filter,sK38,sK37)
| ~ sP6 ),
inference(cnf_transformation,[],[f221]) ).
fof(f351,plain,
( leq(sK40,minus(n6,n1))
| ~ sP5 ),
inference(cnf_transformation,[],[f224]) ).
fof(f352,plain,
( leq(sK39,pv57)
| ~ sP5 ),
inference(cnf_transformation,[],[f224]) ).
fof(f353,plain,
( leq(n0,sK40)
| ~ sP5 ),
inference(cnf_transformation,[],[f224]) ).
fof(f354,plain,
( leq(n0,sK39)
| ~ sP5 ),
inference(cnf_transformation,[],[f224]) ).
fof(f355,plain,
( a_select3(id_ds1_filter,sK39,sK40) != a_select3(id_ds1_filter,sK40,sK39)
| ~ sP5 ),
inference(cnf_transformation,[],[f224]) ).
fof(f356,plain,
( leq(sK41,minus(pv57,n1))
| ~ sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f357,plain,
( leq(n0,sK41)
| ~ sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f358,plain,
( leq(sK42,minus(n6,n1))
| ~ sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f359,plain,
( leq(n0,sK42)
| ~ sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f360,plain,
( a_select3(id_ds1_filter,sK41,sK42) != a_select3(id_ds1_filter,sK42,sK41)
| ~ sP4 ),
inference(cnf_transformation,[],[f227]) ).
fof(f361,plain,
! [X10,X11] :
( ~ leq(X11,minus(n6,n1))
| ~ leq(n0,X11)
| a_select3(id_ds1_filter,X10,X11) = a_select3(id_ds1_filter,X11,X10)
| ~ leq(n0,X10)
| ~ leq(X10,minus(pv57,n1)) ),
inference(cnf_transformation,[],[f229]) ).
fof(f362,plain,
! [X8,X9] :
( ~ leq(X9,minus(n6,n1))
| ~ lt(X8,pv57)
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,minus(n6,n1))
| a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8) ),
inference(cnf_transformation,[],[f229]) ).
fof(f363,plain,
! [X8,X9] :
( a_select3(id_ds1_filter,X8,X9) = a_select3(id_ds1_filter,X9,X8)
| ~ lt(X9,plus(n1,minus(n6,n1)))
| pv57 != X8
| ~ leq(n0,X8)
| ~ leq(n0,X9)
| ~ leq(X8,minus(n6,n1))
| ~ leq(X9,minus(n6,n1)) ),
inference(cnf_transformation,[],[f229]) ).
fof(f364,plain,
! [X6,X7] :
( ~ leq(X7,minus(n6,n1))
| ~ leq(n0,X6)
| ~ leq(n0,X7)
| ~ leq(X6,minus(n6,n1))
| a_select3(pminus_ds1_filter,X6,X7) = a_select3(pminus_ds1_filter,X7,X6) ),
inference(cnf_transformation,[],[f229]) ).
fof(f365,plain,
! [X4,X5] :
( ~ leq(X5,minus(n3,n1))
| ~ leq(n0,X4)
| ~ leq(n0,X5)
| ~ leq(X4,minus(n3,n1))
| a_select3(r_ds1_filter,X4,X5) = a_select3(r_ds1_filter,X5,X4) ),
inference(cnf_transformation,[],[f229]) ).
fof(f366,plain,
! [X2,X3] :
( ~ leq(X3,minus(n6,n1))
| ~ leq(n0,X2)
| ~ leq(n0,X3)
| ~ leq(X2,minus(n6,n1))
| a_select3(q_ds1_filter,X2,X3) = a_select3(q_ds1_filter,X3,X2) ),
inference(cnf_transformation,[],[f229]) ).
fof(f367,plain,
leq(pv57,minus(n6,n1)),
inference(cnf_transformation,[],[f229]) ).
fof(f368,plain,
leq(pv5,minus(n999,n1)),
inference(cnf_transformation,[],[f229]) ).
fof(f369,plain,
leq(n0,pv57),
inference(cnf_transformation,[],[f229]) ).
fof(f370,plain,
leq(n0,pv5),
inference(cnf_transformation,[],[f229]) ).
fof(f371,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,n1))
| leq(sK44,minus(n6,n1))
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f229]) ).
fof(f372,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,n1))
| leq(sK43,minus(n6,n1))
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f229]) ).
fof(f373,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,n1))
| leq(n0,sK44)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f229]) ).
fof(f374,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,n1))
| leq(n0,sK43)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f229]) ).
fof(f375,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv57)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv57,minus(n6,n1))
| a_select3(q_ds1_filter,sK43,sK44) != a_select3(q_ds1_filter,sK44,sK43)
| sP7
| sP6
| sP5
| sP4 ),
inference(cnf_transformation,[],[f229]) ).
fof(f376,plain,
gt(n5,n4),
inference(cnf_transformation,[],[f55]) ).
fof(f390,plain,
gt(n4,n0),
inference(cnf_transformation,[],[f69]) ).
fof(f392,plain,
gt(n6,n0),
inference(cnf_transformation,[],[f71]) ).
fof(f394,plain,
gt(n1,n0),
inference(cnf_transformation,[],[f73]) ).
fof(f395,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f74]) ).
fof(f396,plain,
gt(n3,n0),
inference(cnf_transformation,[],[f75]) ).
fof(f397,plain,
gt(n4,n1),
inference(cnf_transformation,[],[f76]) ).
fof(f398,plain,
gt(n5,n1),
inference(cnf_transformation,[],[f77]) ).
fof(f401,plain,
gt(n2,n1),
inference(cnf_transformation,[],[f80]) ).
fof(f407,plain,
gt(n3,n2),
inference(cnf_transformation,[],[f86]) ).
fof(f408,plain,
gt(n4,n3),
inference(cnf_transformation,[],[f87]) ).
fof(f409,plain,
gt(n5,n3),
inference(cnf_transformation,[],[f88]) ).
fof(f412,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n2 = X0
| n3 = X0
| n4 = X0
| n0 = X0
| ~ leq(X0,n4) ),
inference(cnf_transformation,[],[f158]) ).
fof(f413,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n2 = X0
| n3 = X0
| n4 = X0
| n5 = X0
| n0 = X0
| ~ leq(X0,n5) ),
inference(cnf_transformation,[],[f160]) ).
fof(f414,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n2 = X0
| n3 = X0
| n4 = X0
| n5 = X0
| n6 = X0
| n0 = X0
| ~ leq(X0,n6) ),
inference(cnf_transformation,[],[f162]) ).
fof(f415,plain,
! [X0] :
( ~ leq(n0,X0)
| n0 = X0
| ~ leq(X0,n0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f416,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n0 = X0
| ~ leq(X0,n1) ),
inference(cnf_transformation,[],[f166]) ).
fof(f417,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n2 = X0
| n0 = X0
| ~ leq(X0,n2) ),
inference(cnf_transformation,[],[f168]) ).
fof(f418,plain,
! [X0] :
( ~ leq(n0,X0)
| n1 = X0
| n2 = X0
| n3 = X0
| n0 = X0
| ~ leq(X0,n3) ),
inference(cnf_transformation,[],[f170]) ).
fof(f422,plain,
n1 = succ(n0),
inference(cnf_transformation,[],[f101]) ).
fof(f423,plain,
n2 = succ(succ(n0)),
inference(cnf_transformation,[],[f102]) ).
fof(f425,plain,
! [X0,X1] :
( leq(X0,minus(X1,n1))
| ~ gt(X1,X0) ),
inference(definition_unfolding,[],[f239,f321]) ).
fof(f426,plain,
! [X0,X1] :
( ~ leq(X0,minus(X1,n1))
| gt(X1,X0) ),
inference(definition_unfolding,[],[f238,f321]) ).
fof(f429,plain,
! [X0,X1] :
( ~ gt(plus(X1,n1),X0)
| leq(X0,X1) ),
inference(definition_unfolding,[],[f243,f311]) ).
fof(f430,plain,
! [X0,X1] :
( gt(plus(X1,n1),X0)
| ~ leq(X0,X1) ),
inference(definition_unfolding,[],[f242,f311]) ).
fof(f431,plain,
n0 = plus(tptp_minus_1,n1),
inference(definition_unfolding,[],[f310,f311]) ).
fof(f432,plain,
! [X0] : plus(X0,n1) = plus(n1,X0),
inference(definition_unfolding,[],[f312,f311]) ).
fof(f441,plain,
! [X0] : minus(plus(X0,n1),n1) = X0,
inference(definition_unfolding,[],[f322,f321,f311]) ).
fof(f442,plain,
! [X0] : plus(minus(X0,n1),n1) = X0,
inference(definition_unfolding,[],[f323,f311,f321]) ).
fof(f443,plain,
! [X0,X1] :
( leq(plus(X0,n1),plus(X1,n1))
| ~ leq(X0,X1) ),
inference(definition_unfolding,[],[f325,f311,f311]) ).
fof(f445,plain,
! [X0,X1] :
( ~ leq(plus(X0,n1),X1)
| gt(X1,X0) ),
inference(definition_unfolding,[],[f326,f311]) ).
fof(f449,plain,
n1 = plus(n0,n1),
inference(definition_unfolding,[],[f422,f311]) ).
fof(f450,plain,
n2 = plus(plus(n0,n1),n1),
inference(definition_unfolding,[],[f423,f311,f311]) ).
fof(f455,plain,
! [X9] :
( a_select3(id_ds1_filter,pv57,X9) = a_select3(id_ds1_filter,X9,pv57)
| ~ lt(X9,plus(n1,minus(n6,n1)))
| ~ leq(n0,pv57)
| ~ leq(n0,X9)
| ~ leq(pv57,minus(n6,n1))
| ~ leq(X9,minus(n6,n1)) ),
inference(equality_resolution,[],[f363]) ).
fof(f457,definition,
( spl45_1
<=> leq(pv57,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_1])],[avatar_definition]) ).
fof(f458,plain,
( leq(pv57,minus(n6,n1))
| ~ spl45_1 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f461,definition,
( spl45_2
<=> leq(n0,pv57) ),
introduced(definition,[new_symbols(definition,[spl45_2])],[avatar_definition]) ).
fof(f462,plain,
( leq(n0,pv57)
| ~ spl45_2 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f465,definition,
( spl45_3
<=> ! [X9] :
( a_select3(id_ds1_filter,pv57,X9) = a_select3(id_ds1_filter,X9,pv57)
| ~ leq(X9,minus(n6,n1))
| ~ leq(n0,X9)
| ~ lt(X9,plus(n1,minus(n6,n1))) ) ),
introduced(definition,[new_symbols(definition,[spl45_3])],[avatar_definition]) ).
fof(f466,plain,
( ! [X9] :
( ~ lt(X9,plus(n1,minus(n6,n1)))
| ~ leq(X9,minus(n6,n1))
| ~ leq(n0,X9)
| a_select3(id_ds1_filter,pv57,X9) = a_select3(id_ds1_filter,X9,pv57) )
| ~ spl45_3 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_3 ),
inference(avatar_split_clause,[],[f455,f465,f461,f457]) ).
fof(f468,plain,
spl45_1,
inference(avatar_split_clause,[],[f367,f457]) ).
fof(f469,plain,
spl45_2,
inference(avatar_split_clause,[],[f369,f461]) ).
fof(f471,definition,
( spl45_4
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl45_4])],[avatar_definition]) ).
fof(f475,definition,
( spl45_5
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl45_5])],[avatar_definition]) ).
fof(f479,definition,
( spl45_6
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl45_6])],[avatar_definition]) ).
fof(f483,definition,
( spl45_7
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl45_7])],[avatar_definition]) ).
fof(f487,definition,
( spl45_8
<=> leq(sK44,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_8])],[avatar_definition]) ).
fof(f489,plain,
( leq(sK44,minus(n6,n1))
| ~ spl45_8 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f491,definition,
( spl45_9
<=> leq(pv5,minus(n999,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_9])],[avatar_definition]) ).
fof(f495,definition,
( spl45_10
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[spl45_10])],[avatar_definition]) ).
fof(f498,plain,
( spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_8
| ~ spl45_1
| ~ spl45_9
| ~ spl45_2
| ~ spl45_10 ),
inference(avatar_split_clause,[],[f371,f495,f461,f491,f457,f487,f483,f479,f475,f471]) ).
fof(f500,definition,
( spl45_11
<=> leq(sK43,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_11])],[avatar_definition]) ).
fof(f502,plain,
( leq(sK43,minus(n6,n1))
| ~ spl45_11 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f503,plain,
( spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_11
| ~ spl45_1
| ~ spl45_9
| ~ spl45_2
| ~ spl45_10 ),
inference(avatar_split_clause,[],[f372,f495,f461,f491,f457,f500,f483,f479,f475,f471]) ).
fof(f505,definition,
( spl45_12
<=> leq(n0,sK44) ),
introduced(definition,[new_symbols(definition,[spl45_12])],[avatar_definition]) ).
fof(f508,plain,
( spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_12
| ~ spl45_1
| ~ spl45_9
| ~ spl45_2
| ~ spl45_10 ),
inference(avatar_split_clause,[],[f373,f495,f461,f491,f457,f505,f483,f479,f475,f471]) ).
fof(f510,definition,
( spl45_13
<=> leq(n0,sK43) ),
introduced(definition,[new_symbols(definition,[spl45_13])],[avatar_definition]) ).
fof(f513,plain,
( spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_13
| ~ spl45_1
| ~ spl45_9
| ~ spl45_2
| ~ spl45_10 ),
inference(avatar_split_clause,[],[f374,f495,f461,f491,f457,f510,f483,f479,f475,f471]) ).
fof(f515,definition,
( spl45_14
<=> a_select3(q_ds1_filter,sK43,sK44) = a_select3(q_ds1_filter,sK44,sK43) ),
introduced(definition,[new_symbols(definition,[spl45_14])],[avatar_definition]) ).
fof(f518,plain,
( spl45_4
| spl45_5
| spl45_6
| spl45_7
| ~ spl45_14
| ~ spl45_1
| ~ spl45_9
| ~ spl45_2
| ~ spl45_10 ),
inference(avatar_split_clause,[],[f375,f495,f461,f491,f457,f515,f483,f479,f475,f471]) ).
fof(f520,definition,
( spl45_15
<=> leq(sK41,minus(pv57,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_15])],[avatar_definition]) ).
fof(f522,plain,
( leq(sK41,minus(pv57,n1))
| ~ spl45_15 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f523,plain,
( ~ spl45_4
| spl45_15 ),
inference(avatar_split_clause,[],[f356,f520,f471]) ).
fof(f525,definition,
( spl45_16
<=> leq(n0,sK41) ),
introduced(definition,[new_symbols(definition,[spl45_16])],[avatar_definition]) ).
fof(f528,plain,
( ~ spl45_4
| spl45_16 ),
inference(avatar_split_clause,[],[f357,f525,f471]) ).
fof(f530,definition,
( spl45_17
<=> leq(sK42,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_17])],[avatar_definition]) ).
fof(f532,plain,
( leq(sK42,minus(n6,n1))
| ~ spl45_17 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f533,plain,
( ~ spl45_4
| spl45_17 ),
inference(avatar_split_clause,[],[f358,f530,f471]) ).
fof(f535,definition,
( spl45_18
<=> leq(n0,sK42) ),
introduced(definition,[new_symbols(definition,[spl45_18])],[avatar_definition]) ).
fof(f538,plain,
( ~ spl45_4
| spl45_18 ),
inference(avatar_split_clause,[],[f359,f535,f471]) ).
fof(f540,definition,
( spl45_19
<=> a_select3(id_ds1_filter,sK41,sK42) = a_select3(id_ds1_filter,sK42,sK41) ),
introduced(definition,[new_symbols(definition,[spl45_19])],[avatar_definition]) ).
fof(f543,plain,
( ~ spl45_4
| ~ spl45_19 ),
inference(avatar_split_clause,[],[f360,f540,f471]) ).
fof(f545,definition,
( spl45_20
<=> leq(sK40,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_20])],[avatar_definition]) ).
fof(f547,plain,
( leq(sK40,minus(n6,n1))
| ~ spl45_20 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f548,plain,
( ~ spl45_5
| spl45_20 ),
inference(avatar_split_clause,[],[f351,f545,f475]) ).
fof(f550,definition,
( spl45_21
<=> leq(sK39,pv57) ),
introduced(definition,[new_symbols(definition,[spl45_21])],[avatar_definition]) ).
fof(f552,plain,
( leq(sK39,pv57)
| ~ spl45_21 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f553,plain,
( ~ spl45_5
| spl45_21 ),
inference(avatar_split_clause,[],[f352,f550,f475]) ).
fof(f555,definition,
( spl45_22
<=> leq(n0,sK40) ),
introduced(definition,[new_symbols(definition,[spl45_22])],[avatar_definition]) ).
fof(f558,plain,
( ~ spl45_5
| spl45_22 ),
inference(avatar_split_clause,[],[f353,f555,f475]) ).
fof(f560,definition,
( spl45_23
<=> leq(n0,sK39) ),
introduced(definition,[new_symbols(definition,[spl45_23])],[avatar_definition]) ).
fof(f562,plain,
( leq(n0,sK39)
| ~ spl45_23 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f563,plain,
( ~ spl45_5
| spl45_23 ),
inference(avatar_split_clause,[],[f354,f560,f475]) ).
fof(f565,definition,
( spl45_24
<=> a_select3(id_ds1_filter,sK39,sK40) = a_select3(id_ds1_filter,sK40,sK39) ),
introduced(definition,[new_symbols(definition,[spl45_24])],[avatar_definition]) ).
fof(f567,plain,
( a_select3(id_ds1_filter,sK39,sK40) != a_select3(id_ds1_filter,sK40,sK39)
| spl45_24 ),
inference(avatar_component_clause,[],[f565]) ).
fof(f568,plain,
( ~ spl45_5
| ~ spl45_24 ),
inference(avatar_split_clause,[],[f355,f565,f475]) ).
fof(f570,definition,
( spl45_25
<=> leq(sK38,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_25])],[avatar_definition]) ).
fof(f572,plain,
( leq(sK38,minus(n6,n1))
| ~ spl45_25 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f573,plain,
( ~ spl45_6
| spl45_25 ),
inference(avatar_split_clause,[],[f346,f570,f479]) ).
fof(f575,definition,
( spl45_26
<=> leq(sK37,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_26])],[avatar_definition]) ).
fof(f577,plain,
( leq(sK37,minus(n6,n1))
| ~ spl45_26 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f578,plain,
( ~ spl45_6
| spl45_26 ),
inference(avatar_split_clause,[],[f347,f575,f479]) ).
fof(f580,definition,
( spl45_27
<=> leq(n0,sK38) ),
introduced(definition,[new_symbols(definition,[spl45_27])],[avatar_definition]) ).
fof(f583,plain,
( ~ spl45_6
| spl45_27 ),
inference(avatar_split_clause,[],[f348,f580,f479]) ).
fof(f585,definition,
( spl45_28
<=> leq(n0,sK37) ),
introduced(definition,[new_symbols(definition,[spl45_28])],[avatar_definition]) ).
fof(f588,plain,
( ~ spl45_6
| spl45_28 ),
inference(avatar_split_clause,[],[f349,f585,f479]) ).
fof(f590,definition,
( spl45_29
<=> a_select3(pminus_ds1_filter,sK37,sK38) = a_select3(pminus_ds1_filter,sK38,sK37) ),
introduced(definition,[new_symbols(definition,[spl45_29])],[avatar_definition]) ).
fof(f593,plain,
( ~ spl45_6
| ~ spl45_29 ),
inference(avatar_split_clause,[],[f350,f590,f479]) ).
fof(f595,definition,
( spl45_30
<=> leq(sK36,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_30])],[avatar_definition]) ).
fof(f597,plain,
( leq(sK36,minus(n3,n1))
| ~ spl45_30 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f598,plain,
( ~ spl45_7
| spl45_30 ),
inference(avatar_split_clause,[],[f341,f595,f483]) ).
fof(f600,definition,
( spl45_31
<=> leq(sK35,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_31])],[avatar_definition]) ).
fof(f602,plain,
( leq(sK35,minus(n3,n1))
| ~ spl45_31 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f603,plain,
( ~ spl45_7
| spl45_31 ),
inference(avatar_split_clause,[],[f342,f600,f483]) ).
fof(f605,definition,
( spl45_32
<=> leq(n0,sK36) ),
introduced(definition,[new_symbols(definition,[spl45_32])],[avatar_definition]) ).
fof(f608,plain,
( ~ spl45_7
| spl45_32 ),
inference(avatar_split_clause,[],[f343,f605,f483]) ).
fof(f610,definition,
( spl45_33
<=> leq(n0,sK35) ),
introduced(definition,[new_symbols(definition,[spl45_33])],[avatar_definition]) ).
fof(f613,plain,
( ~ spl45_7
| spl45_33 ),
inference(avatar_split_clause,[],[f344,f610,f483]) ).
fof(f615,definition,
( spl45_34
<=> a_select3(r_ds1_filter,sK35,sK36) = a_select3(r_ds1_filter,sK36,sK35) ),
introduced(definition,[new_symbols(definition,[spl45_34])],[avatar_definition]) ).
fof(f618,plain,
( ~ spl45_7
| ~ spl45_34 ),
inference(avatar_split_clause,[],[f345,f615,f483]) ).
fof(f619,plain,
spl45_10,
inference(avatar_split_clause,[],[f370,f495]) ).
fof(f620,plain,
spl45_9,
inference(avatar_split_clause,[],[f368,f491]) ).
fof(f648,definition,
( spl45_39
<=> leq(n0,minus(pv57,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_39])],[avatar_definition]) ).
fof(f649,plain,
( leq(n0,minus(pv57,n1))
| ~ spl45_39 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f650,plain,
( ~ leq(n0,minus(pv57,n1))
| spl45_39 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f668,definition,
( spl45_44
<=> leq(n0,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_44])],[avatar_definition]) ).
fof(f669,plain,
( leq(n0,minus(n6,n1))
| ~ spl45_44 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f670,plain,
( ~ leq(n0,minus(n6,n1))
| spl45_44 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f691,definition,
( spl45_48
<=> ! [X0] :
( a_select3(id_ds1_filter,X0,sK40) = a_select3(id_ds1_filter,sK40,X0)
| ~ leq(X0,minus(pv57,n1))
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_48])],[avatar_definition]) ).
fof(f692,plain,
( ! [X0] :
( ~ leq(X0,minus(pv57,n1))
| a_select3(id_ds1_filter,X0,sK40) = a_select3(id_ds1_filter,sK40,X0)
| ~ leq(n0,X0) )
| ~ spl45_48 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f703,definition,
( spl45_51
<=> ! [X0] :
( ~ lt(X0,pv57)
| a_select3(id_ds1_filter,X0,sK40) = a_select3(id_ds1_filter,sK40,X0)
| ~ leq(X0,minus(n6,n1))
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_51])],[avatar_definition]) ).
fof(f704,plain,
( ! [X0] :
( ~ leq(X0,minus(n6,n1))
| a_select3(id_ds1_filter,X0,sK40) = a_select3(id_ds1_filter,sK40,X0)
| ~ lt(X0,pv57)
| ~ leq(n0,X0) )
| ~ spl45_51 ),
inference(avatar_component_clause,[],[f703]) ).
fof(f735,definition,
( spl45_57
<=> ! [X0] :
( ~ leq(n0,X0)
| a_select3(pminus_ds1_filter,X0,sK37) = a_select3(pminus_ds1_filter,sK37,X0)
| ~ leq(X0,minus(n6,n1)) ) ),
introduced(definition,[new_symbols(definition,[spl45_57])],[avatar_definition]) ).
fof(f736,plain,
( ! [X0] :
( ~ leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK37) = a_select3(pminus_ds1_filter,sK37,X0)
| ~ leq(n0,X0) )
| ~ spl45_57 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f748,definition,
( spl45_60
<=> ! [X0] :
( ~ leq(n0,X0)
| a_select3(r_ds1_filter,X0,sK36) = a_select3(r_ds1_filter,sK36,X0)
| ~ leq(X0,minus(n3,n1)) ) ),
introduced(definition,[new_symbols(definition,[spl45_60])],[avatar_definition]) ).
fof(f749,plain,
( ! [X0] :
( ~ leq(X0,minus(n3,n1))
| a_select3(r_ds1_filter,X0,sK36) = a_select3(r_ds1_filter,sK36,X0)
| ~ leq(n0,X0) )
| ~ spl45_60 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f794,plain,
leq(n0,n1),
inference(resolution,[],[f236,f394]) ).
fof(f795,plain,
leq(n0,n2),
inference(resolution,[],[f236,f395]) ).
fof(f796,plain,
leq(n0,n3),
inference(resolution,[],[f236,f396]) ).
fof(f797,plain,
leq(n0,n4),
inference(resolution,[],[f236,f390]) ).
fof(f815,plain,
leq(n2,n3),
inference(resolution,[],[f236,f407]) ).
fof(f836,plain,
tptp_minus_1 = minus(n0,n1),
inference(superposition,[],[f441,f431]) ).
fof(f839,plain,
! [X0] : plus(n1,minus(X0,n1)) = X0,
inference(forward_demodulation,[],[f442,f432]) ).
fof(f840,plain,
n2 = plus(n1,plus(n0,n1)),
inference(forward_demodulation,[],[f450,f432]) ).
fof(f841,plain,
n2 = plus(n1,n1),
inference(forward_demodulation,[],[f840,f449]) ).
fof(f845,plain,
( ! [X0] :
( ~ leq(X0,minus(n6,n1))
| ~ lt(X0,n6)
| ~ leq(n0,X0)
| a_select3(id_ds1_filter,X0,pv57) = a_select3(id_ds1_filter,pv57,X0) )
| ~ spl45_3 ),
inference(superposition,[],[f466,f839]) ).
fof(f922,definition,
( spl45_62
<=> leq(n0,n1) ),
introduced(definition,[new_symbols(definition,[spl45_62])],[avatar_definition]) ).
fof(f938,plain,
( ~ gt(n6,n0)
| spl45_44 ),
inference(resolution,[],[f425,f670]) ).
fof(f939,plain,
( ~ gt(pv57,n0)
| spl45_39 ),
inference(resolution,[],[f425,f650]) ).
fof(f949,plain,
( gt(n6,pv57)
| ~ spl45_1 ),
inference(resolution,[],[f426,f458]) ).
fof(f970,plain,
! [X0] :
( ~ gt(n2,X0)
| leq(X0,n1) ),
inference(superposition,[],[f429,f841]) ).
fof(f972,plain,
! [X0] : ~ leq(plus(X0,n1),X0),
inference(resolution,[],[f430,f232]) ).
fof(f987,plain,
! [X0] :
( ~ leq(n2,X0)
| gt(X0,n1) ),
inference(superposition,[],[f445,f841]) ).
fof(f1058,plain,
( ! [X0] :
( leq(X0,minus(n6,n1))
| ~ leq(X0,pv57) )
| ~ spl45_1 ),
inference(resolution,[],[f234,f458]) ).
fof(f1075,plain,
( gt(pv57,n0)
| n0 = pv57
| ~ spl45_2 ),
inference(resolution,[],[f237,f462]) ).
fof(f1105,definition,
( spl45_64
<=> pv57 = sK39 ),
introduced(definition,[new_symbols(definition,[spl45_64])],[avatar_definition]) ).
fof(f1107,plain,
( pv57 = sK39
| ~ spl45_64 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1109,definition,
( spl45_65
<=> gt(pv57,sK39) ),
introduced(definition,[new_symbols(definition,[spl45_65])],[avatar_definition]) ).
fof(f1111,plain,
( gt(pv57,sK39)
| ~ spl45_65 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1159,definition,
( spl45_76
<=> n0 = sK39 ),
introduced(definition,[new_symbols(definition,[spl45_76])],[avatar_definition]) ).
fof(f1161,plain,
( n0 = sK39
| ~ spl45_76 ),
inference(avatar_component_clause,[],[f1159]) ).
fof(f1204,definition,
( spl45_86
<=> n0 = pv57 ),
introduced(definition,[new_symbols(definition,[spl45_86])],[avatar_definition]) ).
fof(f1206,plain,
( n0 = pv57
| ~ spl45_86 ),
inference(avatar_component_clause,[],[f1204]) ).
fof(f1208,definition,
( spl45_87
<=> gt(pv57,n0) ),
introduced(definition,[new_symbols(definition,[spl45_87])],[avatar_definition]) ).
fof(f1210,plain,
( gt(pv57,n0)
| ~ spl45_87 ),
inference(avatar_component_clause,[],[f1208]) ).
fof(f1211,plain,
( spl45_86
| spl45_87
| ~ spl45_2 ),
inference(avatar_split_clause,[],[f1075,f461,f1208,f1204]) ).
fof(f1315,definition,
( spl45_106
<=> ! [X0] :
( ~ leq(n0,X0)
| a_select3(q_ds1_filter,X0,sK43) = a_select3(q_ds1_filter,sK43,X0)
| ~ leq(X0,minus(n6,n1)) ) ),
introduced(definition,[new_symbols(definition,[spl45_106])],[avatar_definition]) ).
fof(f1316,plain,
( ! [X0] :
( ~ leq(X0,minus(n6,n1))
| a_select3(q_ds1_filter,X0,sK43) = a_select3(q_ds1_filter,sK43,X0)
| ~ leq(n0,X0) )
| ~ spl45_106 ),
inference(avatar_component_clause,[],[f1315]) ).
fof(f1356,plain,
( leq(pv57,n6)
| ~ spl45_1 ),
inference(resolution,[],[f949,f236]) ).
fof(f1395,definition,
( spl45_119
<=> ! [X0] :
( a_select3(id_ds1_filter,X0,sK42) = a_select3(id_ds1_filter,sK42,X0)
| ~ leq(X0,minus(pv57,n1))
| ~ leq(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl45_119])],[avatar_definition]) ).
fof(f1396,plain,
( ! [X0] :
( ~ leq(X0,minus(pv57,n1))
| a_select3(id_ds1_filter,X0,sK42) = a_select3(id_ds1_filter,sK42,X0)
| ~ leq(n0,X0) )
| ~ spl45_119 ),
inference(avatar_component_clause,[],[f1395]) ).
fof(f1516,plain,
( lt(n0,pv57)
| ~ spl45_87 ),
inference(resolution,[],[f1210,f235]) ).
fof(f1546,plain,
! [X0] :
( leq(plus(X0,n1),n0)
| ~ leq(X0,tptp_minus_1) ),
inference(superposition,[],[f443,f431]) ).
fof(f1585,plain,
( n1 = pv57
| n0 = pv57
| ~ leq(pv57,n1)
| ~ spl45_2 ),
inference(resolution,[],[f416,f462]) ).
fof(f1648,definition,
( spl45_142
<=> leq(pv57,n1) ),
introduced(definition,[new_symbols(definition,[spl45_142])],[avatar_definition]) ).
fof(f1652,definition,
( spl45_143
<=> n1 = pv57 ),
introduced(definition,[new_symbols(definition,[spl45_143])],[avatar_definition]) ).
fof(f1654,plain,
( n1 = pv57
| ~ spl45_143 ),
inference(avatar_component_clause,[],[f1652]) ).
fof(f1655,plain,
( ~ spl45_142
| spl45_86
| spl45_143
| ~ spl45_2 ),
inference(avatar_split_clause,[],[f1585,f461,f1652,f1204,f1648]) ).
fof(f1786,definition,
( spl45_155
<=> n2 = pv57 ),
introduced(definition,[new_symbols(definition,[spl45_155])],[avatar_definition]) ).
fof(f1788,plain,
( n2 = pv57
| ~ spl45_155 ),
inference(avatar_component_clause,[],[f1786]) ).
fof(f1889,definition,
( spl45_167
<=> n3 = pv57 ),
introduced(definition,[new_symbols(definition,[spl45_167])],[avatar_definition]) ).
fof(f1891,plain,
( n3 = pv57
| ~ spl45_167 ),
inference(avatar_component_clause,[],[f1889]) ).
fof(f2004,definition,
( spl45_179
<=> n4 = pv57 ),
introduced(definition,[new_symbols(definition,[spl45_179])],[avatar_definition]) ).
fof(f2006,plain,
( n4 = pv57
| ~ spl45_179 ),
inference(avatar_component_clause,[],[f2004]) ).
fof(f2078,definition,
( spl45_191
<=> n5 = pv57 ),
introduced(definition,[new_symbols(definition,[spl45_191])],[avatar_definition]) ).
fof(f2080,plain,
( n5 = pv57
| ~ spl45_191 ),
inference(avatar_component_clause,[],[f2078]) ).
fof(f2121,plain,
( n1 = pv57
| n2 = pv57
| n3 = pv57
| n4 = pv57
| n5 = pv57
| pv57 = n6
| n0 = pv57
| ~ leq(pv57,n6)
| ~ spl45_2 ),
inference(resolution,[],[f414,f462]) ).
fof(f2184,definition,
( spl45_202
<=> leq(pv57,n6) ),
introduced(definition,[new_symbols(definition,[spl45_202])],[avatar_definition]) ).
fof(f2188,definition,
( spl45_203
<=> pv57 = n6 ),
introduced(definition,[new_symbols(definition,[spl45_203])],[avatar_definition]) ).
fof(f2190,plain,
( pv57 = n6
| ~ spl45_203 ),
inference(avatar_component_clause,[],[f2188]) ).
fof(f2191,plain,
( ~ spl45_202
| spl45_86
| spl45_203
| spl45_191
| spl45_179
| spl45_167
| spl45_155
| spl45_143
| ~ spl45_2 ),
inference(avatar_split_clause,[],[f2121,f461,f1652,f1786,f1889,f2004,f2078,f2188,f1204,f2184]) ).
fof(f3178,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(n0,sK36)
| ~ leq(X0,minus(n3,n1))
| a_select3(r_ds1_filter,X0,sK36) = a_select3(r_ds1_filter,sK36,X0) )
| ~ spl45_30 ),
inference(resolution,[],[f597,f365]) ).
fof(f3185,plain,
( ~ spl45_32
| spl45_60
| ~ spl45_30 ),
inference(avatar_split_clause,[],[f3178,f595,f748,f605]) ).
fof(f3446,definition,
( spl45_262
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[spl45_262])],[avatar_definition]) ).
fof(f3448,plain,
( ~ leq(n0,n0)
| spl45_262 ),
inference(avatar_component_clause,[],[f3446]) ).
fof(f3583,plain,
( $false
| spl45_44 ),
inference(resolution,[],[f938,f392]) ).
fof(f3586,plain,
spl45_44,
inference(avatar_contradiction_clause,[],[f3583]) ).
fof(f4039,plain,
( a_select3(r_ds1_filter,sK35,sK36) = a_select3(r_ds1_filter,sK36,sK35)
| ~ leq(n0,sK35)
| ~ spl45_31
| ~ spl45_60 ),
inference(resolution,[],[f749,f602]) ).
fof(f4041,plain,
( ~ spl45_33
| spl45_34
| ~ spl45_31
| ~ spl45_60 ),
inference(avatar_split_clause,[],[f4039,f748,f600,f615,f610]) ).
fof(f4314,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(n0,sK37)
| ~ leq(X0,minus(n6,n1))
| a_select3(pminus_ds1_filter,X0,sK37) = a_select3(pminus_ds1_filter,sK37,X0) )
| ~ spl45_26 ),
inference(resolution,[],[f577,f364]) ).
fof(f4331,plain,
( ~ spl45_28
| spl45_57
| ~ spl45_26 ),
inference(avatar_split_clause,[],[f4314,f575,f735,f585]) ).
fof(f4351,plain,
( ! [X0] :
( ~ leq(n0,sK42)
| a_select3(id_ds1_filter,X0,sK42) = a_select3(id_ds1_filter,sK42,X0)
| ~ leq(n0,X0)
| ~ leq(X0,minus(pv57,n1)) )
| ~ spl45_17 ),
inference(resolution,[],[f532,f361]) ).
fof(f4358,plain,
( spl45_119
| ~ spl45_18
| ~ spl45_17 ),
inference(avatar_split_clause,[],[f4351,f530,f535,f1395]) ).
fof(f4486,plain,
( a_select3(pminus_ds1_filter,sK37,sK38) = a_select3(pminus_ds1_filter,sK38,sK37)
| ~ leq(n0,sK38)
| ~ spl45_25
| ~ spl45_57 ),
inference(resolution,[],[f736,f572]) ).
fof(f4785,plain,
( a_select3(id_ds1_filter,sK41,sK42) = a_select3(id_ds1_filter,sK42,sK41)
| ~ leq(n0,sK41)
| ~ spl45_15
| ~ spl45_119 ),
inference(resolution,[],[f1396,f522]) ).
fof(f4786,plain,
( ~ spl45_16
| spl45_19
| ~ spl45_15
| ~ spl45_119 ),
inference(avatar_split_clause,[],[f4785,f1395,f520,f540,f525]) ).
fof(f5633,definition,
( spl45_485
<=> leq(n0,n3) ),
introduced(definition,[new_symbols(definition,[spl45_485])],[avatar_definition]) ).
fof(f5884,definition,
( spl45_498
<=> leq(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl45_498])],[avatar_definition]) ).
fof(f5956,definition,
( spl45_501
<=> leq(n2,pv57) ),
introduced(definition,[new_symbols(definition,[spl45_501])],[avatar_definition]) ).
fof(f5957,plain,
( leq(n2,pv57)
| ~ spl45_501 ),
inference(avatar_component_clause,[],[f5956]) ).
fof(f5958,plain,
( ~ leq(n2,pv57)
| spl45_501 ),
inference(avatar_component_clause,[],[f5956]) ).
fof(f5964,definition,
( spl45_503
<=> leq(n2,n3) ),
introduced(definition,[new_symbols(definition,[spl45_503])],[avatar_definition]) ).
fof(f6143,definition,
( spl45_511
<=> leq(n0,n4) ),
introduced(definition,[new_symbols(definition,[spl45_511])],[avatar_definition]) ).
fof(f6254,plain,
( spl45_202
| ~ spl45_1 ),
inference(avatar_split_clause,[],[f1356,f457,f2184]) ).
fof(f7559,definition,
( spl45_617
<=> leq(n6,n6) ),
introduced(definition,[new_symbols(definition,[spl45_617])],[avatar_definition]) ).
fof(f7561,plain,
( ~ leq(n6,n6)
| spl45_617 ),
inference(avatar_component_clause,[],[f7559]) ).
fof(f10368,plain,
( n1 = sK39
| n2 = sK39
| n3 = sK39
| n4 = sK39
| n0 = sK39
| ~ leq(sK39,n4)
| ~ spl45_23 ),
inference(resolution,[],[f562,f412]) ).
fof(f10369,plain,
( n1 = sK39
| n2 = sK39
| n3 = sK39
| n4 = sK39
| n5 = sK39
| n0 = sK39
| ~ leq(sK39,n5)
| ~ spl45_23 ),
inference(resolution,[],[f562,f413]) ).
fof(f10371,plain,
( n0 = sK39
| ~ leq(sK39,n0)
| ~ spl45_23 ),
inference(resolution,[],[f562,f415]) ).
fof(f10372,plain,
( n1 = sK39
| n0 = sK39
| ~ leq(sK39,n1)
| ~ spl45_23 ),
inference(resolution,[],[f562,f416]) ).
fof(f10373,plain,
( n1 = sK39
| n2 = sK39
| n0 = sK39
| ~ leq(sK39,n2)
| ~ spl45_23 ),
inference(resolution,[],[f562,f417]) ).
fof(f10374,plain,
( n1 = sK39
| n2 = sK39
| n3 = sK39
| n0 = sK39
| ~ leq(sK39,n3)
| ~ spl45_23 ),
inference(resolution,[],[f562,f418]) ).
fof(f10381,definition,
( spl45_739
<=> leq(sK39,n3) ),
introduced(definition,[new_symbols(definition,[spl45_739])],[avatar_definition]) ).
fof(f10385,definition,
( spl45_740
<=> n3 = sK39 ),
introduced(definition,[new_symbols(definition,[spl45_740])],[avatar_definition]) ).
fof(f10387,plain,
( n3 = sK39
| ~ spl45_740 ),
inference(avatar_component_clause,[],[f10385]) ).
fof(f10389,definition,
( spl45_741
<=> n2 = sK39 ),
introduced(definition,[new_symbols(definition,[spl45_741])],[avatar_definition]) ).
fof(f10391,plain,
( n2 = sK39
| ~ spl45_741 ),
inference(avatar_component_clause,[],[f10389]) ).
fof(f10393,definition,
( spl45_742
<=> n1 = sK39 ),
introduced(definition,[new_symbols(definition,[spl45_742])],[avatar_definition]) ).
fof(f10395,plain,
( n1 = sK39
| ~ spl45_742 ),
inference(avatar_component_clause,[],[f10393]) ).
fof(f10396,plain,
( ~ spl45_739
| spl45_76
| spl45_740
| spl45_741
| spl45_742
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f10374,f560,f10393,f10389,f10385,f1159,f10381]) ).
fof(f10398,definition,
( spl45_743
<=> leq(sK39,n2) ),
introduced(definition,[new_symbols(definition,[spl45_743])],[avatar_definition]) ).
fof(f10400,plain,
( ~ leq(sK39,n2)
| spl45_743 ),
inference(avatar_component_clause,[],[f10398]) ).
fof(f10401,plain,
( ~ spl45_743
| spl45_76
| spl45_741
| spl45_742
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f10373,f560,f10393,f10389,f1159,f10398]) ).
fof(f10403,definition,
( spl45_744
<=> leq(sK39,n1) ),
introduced(definition,[new_symbols(definition,[spl45_744])],[avatar_definition]) ).
fof(f10406,plain,
( ~ spl45_744
| spl45_76
| spl45_742
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f10372,f560,f10393,f1159,f10403]) ).
fof(f10408,definition,
( spl45_745
<=> leq(sK39,n0) ),
introduced(definition,[new_symbols(definition,[spl45_745])],[avatar_definition]) ).
fof(f10411,plain,
( ~ spl45_745
| spl45_76
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f10371,f560,f1159,f10408]) ).
fof(f10421,definition,
( spl45_748
<=> n5 = sK39 ),
introduced(definition,[new_symbols(definition,[spl45_748])],[avatar_definition]) ).
fof(f10423,plain,
( n5 = sK39
| ~ spl45_748 ),
inference(avatar_component_clause,[],[f10421]) ).
fof(f10425,definition,
( spl45_749
<=> n4 = sK39 ),
introduced(definition,[new_symbols(definition,[spl45_749])],[avatar_definition]) ).
fof(f10427,plain,
( n4 = sK39
| ~ spl45_749 ),
inference(avatar_component_clause,[],[f10425]) ).
fof(f10430,definition,
( spl45_750
<=> leq(sK39,n5) ),
introduced(definition,[new_symbols(definition,[spl45_750])],[avatar_definition]) ).
fof(f10432,plain,
( ~ leq(sK39,n5)
| spl45_750 ),
inference(avatar_component_clause,[],[f10430]) ).
fof(f10433,plain,
( ~ spl45_750
| spl45_76
| spl45_748
| spl45_749
| spl45_740
| spl45_741
| spl45_742
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f10369,f560,f10393,f10389,f10385,f10425,f10421,f1159,f10430]) ).
fof(f10435,definition,
( spl45_751
<=> leq(sK39,n4) ),
introduced(definition,[new_symbols(definition,[spl45_751])],[avatar_definition]) ).
fof(f10437,plain,
( ~ leq(sK39,n4)
| spl45_751 ),
inference(avatar_component_clause,[],[f10435]) ).
fof(f10438,plain,
( ~ spl45_751
| spl45_76
| spl45_749
| spl45_740
| spl45_741
| spl45_742
| ~ spl45_23 ),
inference(avatar_split_clause,[],[f10368,f560,f10393,f10389,f10385,f10425,f1159,f10435]) ).
fof(f10439,plain,
( ! [X0] :
( ~ leq(n0,sK40)
| a_select3(id_ds1_filter,X0,sK40) = a_select3(id_ds1_filter,sK40,X0)
| ~ leq(n0,X0)
| ~ leq(X0,minus(pv57,n1)) )
| ~ spl45_20 ),
inference(resolution,[],[f547,f361]) ).
fof(f10440,plain,
( ! [X0] :
( ~ lt(X0,pv57)
| ~ leq(n0,X0)
| ~ leq(n0,sK40)
| ~ leq(X0,minus(n6,n1))
| a_select3(id_ds1_filter,X0,sK40) = a_select3(id_ds1_filter,sK40,X0) )
| ~ spl45_20 ),
inference(resolution,[],[f547,f362]) ).
fof(f10450,plain,
( gt(n6,sK40)
| ~ spl45_20 ),
inference(resolution,[],[f547,f426]) ).
fof(f10497,plain,
( ~ spl45_22
| spl45_51
| ~ spl45_20 ),
inference(avatar_split_clause,[],[f10440,f545,f703,f555]) ).
fof(f10498,plain,
( spl45_48
| ~ spl45_22
| ~ spl45_20 ),
inference(avatar_split_clause,[],[f10439,f545,f555,f691]) ).
fof(f10520,plain,
( gt(pv57,n4)
| ~ spl45_191 ),
inference(superposition,[],[f376,f2080]) ).
fof(f10525,plain,
( gt(pv57,n1)
| ~ spl45_191 ),
inference(superposition,[],[f398,f2080]) ).
fof(f10527,plain,
( gt(pv57,n3)
| ~ spl45_191 ),
inference(superposition,[],[f409,f2080]) ).
fof(f11184,definition,
( spl45_810
<=> leq(n4,minus(pv57,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_810])],[avatar_definition]) ).
fof(f11185,plain,
( leq(n4,minus(pv57,n1))
| ~ spl45_810 ),
inference(avatar_component_clause,[],[f11184]) ).
fof(f11186,plain,
( ~ leq(n4,minus(pv57,n1))
| spl45_810 ),
inference(avatar_component_clause,[],[f11184]) ).
fof(f11335,definition,
( spl45_828
<=> a_select3(id_ds1_filter,sK40,pv57) = a_select3(id_ds1_filter,pv57,sK40) ),
introduced(definition,[new_symbols(definition,[spl45_828])],[avatar_definition]) ).
fof(f11337,plain,
( a_select3(id_ds1_filter,sK40,pv57) = a_select3(id_ds1_filter,pv57,sK40)
| ~ spl45_828 ),
inference(avatar_component_clause,[],[f11335]) ).
fof(f11356,definition,
( spl45_833
<=> lt(n0,pv57) ),
introduced(definition,[new_symbols(definition,[spl45_833])],[avatar_definition]) ).
fof(f11388,plain,
( a_select3(id_ds1_filter,n0,sK40) = a_select3(id_ds1_filter,sK40,n0)
| ~ lt(n0,pv57)
| ~ leq(n0,n0)
| ~ spl45_44
| ~ spl45_51 ),
inference(resolution,[],[f704,f669]) ).
fof(f11433,definition,
( spl45_845
<=> a_select3(id_ds1_filter,n0,sK40) = a_select3(id_ds1_filter,sK40,n0) ),
introduced(definition,[new_symbols(definition,[spl45_845])],[avatar_definition]) ).
fof(f11436,plain,
( ~ spl45_262
| ~ spl45_833
| spl45_845
| ~ spl45_44
| ~ spl45_51 ),
inference(avatar_split_clause,[],[f11388,f703,f668,f11433,f11356,f3446]) ).
fof(f11445,definition,
( spl45_847
<=> a_select3(id_ds1_filter,n4,sK40) = a_select3(id_ds1_filter,sK40,n4) ),
introduced(definition,[new_symbols(definition,[spl45_847])],[avatar_definition]) ).
fof(f11447,plain,
( a_select3(id_ds1_filter,n4,sK40) = a_select3(id_ds1_filter,sK40,n4)
| ~ spl45_847 ),
inference(avatar_component_clause,[],[f11445]) ).
fof(f11607,plain,
( ~ lt(sK40,n6)
| ~ leq(n0,sK40)
| a_select3(id_ds1_filter,sK40,pv57) = a_select3(id_ds1_filter,pv57,sK40)
| ~ spl45_3
| ~ spl45_20 ),
inference(resolution,[],[f845,f547]) ).
fof(f11617,definition,
( spl45_869
<=> lt(sK40,n6) ),
introduced(definition,[new_symbols(definition,[spl45_869])],[avatar_definition]) ).
fof(f11620,plain,
( spl45_828
| ~ spl45_22
| ~ spl45_869
| ~ spl45_3
| ~ spl45_20 ),
inference(avatar_split_clause,[],[f11607,f545,f465,f11617,f555,f11335]) ).
fof(f12649,plain,
( $false
| spl45_262 ),
inference(resolution,[],[f3448,f233]) ).
fof(f12650,plain,
spl45_262,
inference(avatar_contradiction_clause,[],[f12649]) ).
fof(f14275,plain,
( gt(pv57,n1)
| ~ spl45_155 ),
inference(superposition,[],[f401,f1788]) ).
fof(f14303,plain,
spl45_62,
inference(avatar_split_clause,[],[f794,f922]) ).
fof(f14305,plain,
spl45_485,
inference(avatar_split_clause,[],[f796,f5633]) ).
fof(f14306,plain,
spl45_511,
inference(avatar_split_clause,[],[f797,f6143]) ).
fof(f14310,plain,
spl45_498,
inference(avatar_split_clause,[],[f795,f5884]) ).
fof(f14406,definition,
( spl45_1188
<=> gt(n2,pv57) ),
introduced(definition,[new_symbols(definition,[spl45_1188])],[avatar_definition]) ).
fof(f14407,plain,
( ~ gt(n2,pv57)
| spl45_1188 ),
inference(avatar_component_clause,[],[f14406]) ).
fof(f14408,plain,
( gt(n2,pv57)
| ~ spl45_1188 ),
inference(avatar_component_clause,[],[f14406]) ).
fof(f14534,plain,
( gt(pv57,n1)
| ~ spl45_179 ),
inference(superposition,[],[f397,f2006]) ).
fof(f14536,plain,
( gt(pv57,n3)
| ~ spl45_179 ),
inference(superposition,[],[f408,f2006]) ).
fof(f14725,definition,
( spl45_1192
<=> gt(pv57,n1) ),
introduced(definition,[new_symbols(definition,[spl45_1192])],[avatar_definition]) ).
fof(f14730,plain,
( spl45_1192
| ~ spl45_155 ),
inference(avatar_split_clause,[],[f14275,f1786,f14725]) ).
fof(f14875,plain,
spl45_503,
inference(avatar_split_clause,[],[f815,f5964]) ).
fof(f15027,plain,
( gt(n3,sK39)
| ~ spl45_65
| ~ spl45_167 ),
inference(forward_demodulation,[],[f1111,f1891]) ).
fof(f15029,plain,
( leq(sK39,n3)
| ~ spl45_65
| ~ spl45_167 ),
inference(resolution,[],[f15027,f236]) ).
fof(f15031,plain,
( spl45_739
| ~ spl45_65
| ~ spl45_167 ),
inference(avatar_split_clause,[],[f15029,f1889,f1109,f10381]) ).
fof(f15038,plain,
( a_select3(id_ds1_filter,n0,sK40) != a_select3(id_ds1_filter,sK40,n0)
| spl45_24
| ~ spl45_76 ),
inference(superposition,[],[f567,f1161]) ).
fof(f15214,plain,
( a_select3(id_ds1_filter,n1,sK40) != a_select3(id_ds1_filter,sK40,n1)
| spl45_24
| ~ spl45_742 ),
inference(superposition,[],[f567,f10395]) ).
fof(f15227,plain,
( a_select3(id_ds1_filter,n2,sK40) != a_select3(id_ds1_filter,sK40,n2)
| spl45_24
| ~ spl45_741 ),
inference(superposition,[],[f567,f10391]) ).
fof(f15251,plain,
( lt(sK40,n6)
| ~ spl45_20 ),
inference(resolution,[],[f10450,f235]) ).
fof(f15252,plain,
( spl45_869
| ~ spl45_20 ),
inference(avatar_split_clause,[],[f15251,f545,f11617]) ).
fof(f15254,plain,
( a_select3(id_ds1_filter,sK40,n3) = a_select3(id_ds1_filter,n3,sK40)
| ~ spl45_167
| ~ spl45_828 ),
inference(forward_demodulation,[],[f11337,f1891]) ).
fof(f17149,plain,
( ~ leq(plus(minus(n6,n1),n1),pv57)
| ~ spl45_1 ),
inference(resolution,[],[f972,f1058]) ).
fof(f17392,definition,
( spl45_1299
<=> leq(n0,tptp_minus_1) ),
introduced(definition,[new_symbols(definition,[spl45_1299])],[avatar_definition]) ).
fof(f18461,plain,
( ~ leq(n2,n3)
| ~ spl45_167
| spl45_501 ),
inference(forward_demodulation,[],[f5958,f1891]) ).
fof(f18462,plain,
( ~ spl45_503
| ~ spl45_167
| spl45_501 ),
inference(avatar_split_clause,[],[f18461,f5956,f1889,f5964]) ).
fof(f18914,plain,
( a_select3(id_ds1_filter,sK40,n3) != a_select3(id_ds1_filter,n3,sK40)
| spl45_24
| ~ spl45_740 ),
inference(superposition,[],[f567,f10387]) ).
fof(f20230,plain,
~ leq(n0,tptp_minus_1),
inference(resolution,[],[f1546,f972]) ).
fof(f20251,plain,
~ spl45_1299,
inference(avatar_split_clause,[],[f20230,f17392]) ).
fof(f33486,plain,
( $false
| spl45_617 ),
inference(resolution,[],[f7561,f233]) ).
fof(f33487,plain,
spl45_617,
inference(avatar_contradiction_clause,[],[f33486]) ).
fof(f42794,plain,
( ~ spl45_845
| spl45_24
| ~ spl45_76 ),
inference(avatar_split_clause,[],[f15038,f1159,f565,f11433]) ).
fof(f53425,plain,
( ~ spl45_27
| spl45_29
| ~ spl45_25
| ~ spl45_57 ),
inference(avatar_split_clause,[],[f4486,f735,f570,f590,f580]) ).
fof(f55548,plain,
( spl45_1192
| ~ spl45_191 ),
inference(avatar_split_clause,[],[f10525,f2078,f14725]) ).
fof(f55551,plain,
( gt(pv57,n0)
| ~ spl45_65
| ~ spl45_76 ),
inference(forward_demodulation,[],[f1111,f1161]) ).
fof(f55637,plain,
( ~ leq(plus(n1,minus(n6,n1)),pv57)
| ~ spl45_1 ),
inference(forward_demodulation,[],[f17149,f432]) ).
fof(f55883,definition,
( spl45_3694
<=> leq(n2,minus(pv57,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_3694])],[avatar_definition]) ).
fof(f55884,plain,
( leq(n2,minus(pv57,n1))
| ~ spl45_3694 ),
inference(avatar_component_clause,[],[f55883]) ).
fof(f55885,plain,
( ~ leq(n2,minus(pv57,n1))
| spl45_3694 ),
inference(avatar_component_clause,[],[f55883]) ).
fof(f56362,plain,
( ~ leq(n6,pv57)
| ~ spl45_1 ),
inference(forward_demodulation,[],[f55637,f839]) ).
fof(f56447,definition,
( spl45_3780
<=> a_select3(id_ds1_filter,n2,sK40) = a_select3(id_ds1_filter,sK40,n2) ),
introduced(definition,[new_symbols(definition,[spl45_3780])],[avatar_definition]) ).
fof(f56539,plain,
( ~ spl45_87
| spl45_39 ),
inference(avatar_split_clause,[],[f939,f648,f1208]) ).
fof(f56937,definition,
( spl45_3802
<=> leq(n6,pv57) ),
introduced(definition,[new_symbols(definition,[spl45_3802])],[avatar_definition]) ).
fof(f56939,plain,
( ~ leq(n6,pv57)
| spl45_3802 ),
inference(avatar_component_clause,[],[f56937]) ).
fof(f58248,definition,
( spl45_3886
<=> gt(pv57,n3) ),
introduced(definition,[new_symbols(definition,[spl45_3886])],[avatar_definition]) ).
fof(f58593,plain,
( gt(pv57,n1)
| ~ spl45_501 ),
inference(resolution,[],[f5957,f987]) ).
fof(f58641,plain,
( spl45_1192
| ~ spl45_501 ),
inference(avatar_split_clause,[],[f58593,f5956,f14725]) ).
fof(f58972,definition,
( spl45_3916
<=> gt(pv57,n4) ),
introduced(definition,[new_symbols(definition,[spl45_3916])],[avatar_definition]) ).
fof(f63113,plain,
( spl45_3916
| ~ spl45_191 ),
inference(avatar_split_clause,[],[f10520,f2078,f58972]) ).
fof(f63448,plain,
( spl45_3886
| ~ spl45_191 ),
inference(avatar_split_clause,[],[f10527,f2078,f58248]) ).
fof(f65630,plain,
( spl45_87
| ~ spl45_65
| ~ spl45_76 ),
inference(avatar_split_clause,[],[f55551,f1159,f1109,f1208]) ).
fof(f65703,plain,
( spl45_833
| ~ spl45_87 ),
inference(avatar_split_clause,[],[f1516,f1208,f11356]) ).
fof(f66542,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(n0,sK43)
| ~ leq(X0,minus(n6,n1))
| a_select3(q_ds1_filter,X0,sK43) = a_select3(q_ds1_filter,sK43,X0) )
| ~ spl45_11 ),
inference(resolution,[],[f502,f366]) ).
fof(f66598,plain,
( ~ spl45_13
| spl45_106
| ~ spl45_11 ),
inference(avatar_split_clause,[],[f66542,f500,f1315,f510]) ).
fof(f70795,definition,
( spl45_4708
<=> leq(n1,minus(pv57,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_4708])],[avatar_definition]) ).
fof(f70796,plain,
( leq(n1,minus(pv57,n1))
| ~ spl45_4708 ),
inference(avatar_component_clause,[],[f70795]) ).
fof(f70797,plain,
( ~ leq(n1,minus(pv57,n1))
| spl45_4708 ),
inference(avatar_component_clause,[],[f70795]) ).
fof(f72135,definition,
( spl45_4739
<=> leq(n3,minus(pv57,n1)) ),
introduced(definition,[new_symbols(definition,[spl45_4739])],[avatar_definition]) ).
fof(f72136,plain,
( leq(n3,minus(pv57,n1))
| ~ spl45_4739 ),
inference(avatar_component_clause,[],[f72135]) ).
fof(f72137,plain,
( ~ leq(n3,minus(pv57,n1))
| spl45_4739 ),
inference(avatar_component_clause,[],[f72135]) ).
fof(f72245,definition,
( spl45_4746
<=> a_select3(id_ds1_filter,sK40,n3) = a_select3(id_ds1_filter,n3,sK40) ),
introduced(definition,[new_symbols(definition,[spl45_4746])],[avatar_definition]) ).
fof(f74258,plain,
( leq(pv57,n1)
| ~ spl45_1188 ),
inference(resolution,[],[f14408,f970]) ).
fof(f74264,plain,
( spl45_142
| ~ spl45_1188 ),
inference(avatar_split_clause,[],[f74258,f14406,f1648]) ).
fof(f74483,plain,
( ~ spl45_3802
| ~ spl45_1 ),
inference(avatar_split_clause,[],[f56362,f457,f56937]) ).
fof(f79790,plain,
( ~ gt(pv57,n4)
| spl45_810 ),
inference(resolution,[],[f11186,f425]) ).
fof(f79791,plain,
( ~ spl45_3916
| spl45_810 ),
inference(avatar_split_clause,[],[f79790,f11184,f58972]) ).
fof(f79794,plain,
( a_select3(id_ds1_filter,n4,sK40) = a_select3(id_ds1_filter,sK40,n4)
| ~ leq(n0,n4)
| ~ spl45_48
| ~ spl45_810 ),
inference(resolution,[],[f11185,f692]) ).
fof(f79830,plain,
( ~ spl45_511
| spl45_847
| ~ spl45_48
| ~ spl45_810 ),
inference(avatar_split_clause,[],[f79794,f11184,f691,f11445,f6143]) ).
fof(f80506,plain,
( a_select3(id_ds1_filter,n2,sK40) = a_select3(id_ds1_filter,sK40,n2)
| ~ leq(n0,n2)
| ~ spl45_48
| ~ spl45_3694 ),
inference(resolution,[],[f55884,f692]) ).
fof(f80629,plain,
( ~ gt(pv57,n1)
| spl45_4708 ),
inference(resolution,[],[f70797,f425]) ).
fof(f80630,plain,
( ~ spl45_1192
| spl45_4708 ),
inference(avatar_split_clause,[],[f80629,f70795,f14725]) ).
fof(f80634,plain,
( a_select3(id_ds1_filter,n1,sK40) = a_select3(id_ds1_filter,sK40,n1)
| ~ leq(n0,n1)
| ~ spl45_48
| ~ spl45_4708 ),
inference(resolution,[],[f70796,f692]) ).
fof(f80690,plain,
( ~ gt(pv57,n3)
| spl45_4739 ),
inference(resolution,[],[f72137,f425]) ).
fof(f80691,plain,
( ~ spl45_3886
| spl45_4739 ),
inference(avatar_split_clause,[],[f80690,f72135,f58248]) ).
fof(f80713,plain,
( a_select3(id_ds1_filter,sK40,n3) = a_select3(id_ds1_filter,n3,sK40)
| ~ leq(n0,n3)
| ~ spl45_48
| ~ spl45_4739 ),
inference(resolution,[],[f72136,f692]) ).
fof(f80895,plain,
( ~ spl45_498
| spl45_3780
| ~ spl45_48
| ~ spl45_3694 ),
inference(avatar_split_clause,[],[f80506,f55883,f691,f56447,f5884]) ).
fof(f80897,definition,
( spl45_5011
<=> a_select3(id_ds1_filter,n1,sK40) = a_select3(id_ds1_filter,sK40,n1) ),
introduced(definition,[new_symbols(definition,[spl45_5011])],[avatar_definition]) ).
fof(f86888,definition,
( spl45_5439
<=> gt(pv57,n2) ),
introduced(definition,[new_symbols(definition,[spl45_5439])],[avatar_definition]) ).
fof(f89913,plain,
( ~ spl45_5011
| spl45_24
| ~ spl45_742 ),
inference(avatar_split_clause,[],[f15214,f10393,f565,f80897]) ).
fof(f89988,plain,
( pv57 = sK39
| ~ spl45_191
| ~ spl45_748 ),
inference(forward_demodulation,[],[f10423,f2080]) ).
fof(f89989,plain,
( spl45_64
| ~ spl45_191
| ~ spl45_748 ),
inference(avatar_split_clause,[],[f89988,f10421,f2078,f1105]) ).
fof(f89991,plain,
( ~ leq(sK39,pv57)
| ~ spl45_191
| spl45_750 ),
inference(forward_demodulation,[],[f10432,f2080]) ).
fof(f89993,plain,
( ~ spl45_21
| ~ spl45_191
| spl45_750 ),
inference(avatar_split_clause,[],[f89991,f10430,f2078,f550]) ).
fof(f94898,plain,
( leq(sK39,n0)
| ~ spl45_21
| ~ spl45_86 ),
inference(superposition,[],[f552,f1206]) ).
fof(f94900,plain,
( leq(n0,minus(n0,n1))
| ~ spl45_39
| ~ spl45_86 ),
inference(superposition,[],[f649,f1206]) ).
fof(f95048,plain,
( leq(n0,tptp_minus_1)
| ~ spl45_39
| ~ spl45_86 ),
inference(forward_demodulation,[],[f94900,f836]) ).
fof(f95050,plain,
( spl45_745
| ~ spl45_21
| ~ spl45_86 ),
inference(avatar_split_clause,[],[f94898,f1204,f550,f10408]) ).
fof(f95058,plain,
( spl45_1299
| ~ spl45_39
| ~ spl45_86 ),
inference(avatar_split_clause,[],[f95048,f1204,f648,f17392]) ).
fof(f99652,plain,
( gt(pv57,sK39)
| pv57 = sK39
| ~ spl45_21 ),
inference(resolution,[],[f552,f237]) ).
fof(f99660,plain,
( spl45_64
| spl45_65
| ~ spl45_21 ),
inference(avatar_split_clause,[],[f99652,f550,f1109,f1105]) ).
fof(f99759,plain,
( leq(sK39,n1)
| ~ spl45_21
| ~ spl45_143 ),
inference(superposition,[],[f552,f1654]) ).
fof(f99842,plain,
( a_select3(id_ds1_filter,n1,sK40) = a_select3(id_ds1_filter,sK40,n1)
| ~ spl45_143
| ~ spl45_828 ),
inference(superposition,[],[f11337,f1654]) ).
fof(f99879,plain,
( spl45_5011
| ~ spl45_143
| ~ spl45_828 ),
inference(avatar_split_clause,[],[f99842,f11335,f1652,f80897]) ).
fof(f99928,plain,
( spl45_744
| ~ spl45_21
| ~ spl45_143 ),
inference(avatar_split_clause,[],[f99759,f1652,f550,f10403]) ).
fof(f99940,plain,
( ~ spl45_62
| spl45_5011
| ~ spl45_48
| ~ spl45_4708 ),
inference(avatar_split_clause,[],[f80634,f70795,f691,f80897,f922]) ).
fof(f102679,plain,
( a_select3(q_ds1_filter,sK43,sK44) = a_select3(q_ds1_filter,sK44,sK43)
| ~ leq(n0,sK44)
| ~ spl45_8
| ~ spl45_106 ),
inference(resolution,[],[f1316,f489]) ).
fof(f102802,plain,
( ~ spl45_12
| spl45_14
| ~ spl45_8
| ~ spl45_106 ),
inference(avatar_split_clause,[],[f102679,f1315,f487,f515,f505]) ).
fof(f104007,plain,
( a_select3(id_ds1_filter,sK40,pv57) != a_select3(id_ds1_filter,pv57,sK40)
| spl45_24
| ~ spl45_64 ),
inference(superposition,[],[f567,f1107]) ).
fof(f104009,plain,
( a_select3(id_ds1_filter,pv57,sK40) != a_select3(id_ds1_filter,pv57,sK40)
| spl45_24
| ~ spl45_64
| ~ spl45_828 ),
inference(forward_demodulation,[],[f104007,f11337]) ).
fof(f104010,plain,
( $false
| spl45_24
| ~ spl45_64
| ~ spl45_828 ),
inference(trivial_inequality_removal,[],[f104009]) ).
fof(f104011,plain,
( spl45_24
| ~ spl45_64
| ~ spl45_828 ),
inference(avatar_contradiction_clause,[],[f104010]) ).
fof(f104295,plain,
( spl45_1192
| ~ spl45_179 ),
inference(avatar_split_clause,[],[f14534,f2004,f14725]) ).
fof(f104297,plain,
( spl45_3886
| ~ spl45_179 ),
inference(avatar_split_clause,[],[f14536,f2004,f58248]) ).
fof(f104797,plain,
( ~ leq(n6,n6)
| ~ spl45_203
| spl45_3802 ),
inference(superposition,[],[f56939,f2190]) ).
fof(f104805,plain,
( ~ spl45_617
| ~ spl45_203
| spl45_3802 ),
inference(avatar_split_clause,[],[f104797,f56937,f2188,f7559]) ).
fof(f105005,plain,
( ~ spl45_485
| spl45_4746
| ~ spl45_48
| ~ spl45_4739 ),
inference(avatar_split_clause,[],[f80713,f72135,f691,f72245,f5633]) ).
fof(f105006,plain,
( spl45_4746
| ~ spl45_167
| ~ spl45_828 ),
inference(avatar_split_clause,[],[f15254,f11335,f1889,f72245]) ).
fof(f105007,plain,
( ~ spl45_4746
| spl45_24
| ~ spl45_740 ),
inference(avatar_split_clause,[],[f18914,f10385,f565,f72245]) ).
fof(f106655,plain,
( ~ spl45_3780
| spl45_24
| ~ spl45_741 ),
inference(avatar_split_clause,[],[f15227,f10389,f565,f56447]) ).
fof(f107305,plain,
( pv57 = sK39
| ~ spl45_155
| ~ spl45_741 ),
inference(forward_demodulation,[],[f10391,f1788]) ).
fof(f107306,plain,
( spl45_64
| ~ spl45_155
| ~ spl45_741 ),
inference(avatar_split_clause,[],[f107305,f10389,f1786,f1105]) ).
fof(f107308,plain,
( ~ leq(sK39,pv57)
| ~ spl45_155
| spl45_743 ),
inference(forward_demodulation,[],[f10400,f1788]) ).
fof(f107309,plain,
( ~ spl45_21
| ~ spl45_155
| spl45_743 ),
inference(avatar_split_clause,[],[f107308,f10398,f1786,f550]) ).
fof(f110162,plain,
( gt(pv57,n2)
| n2 = pv57
| spl45_1188 ),
inference(resolution,[],[f14407,f230]) ).
fof(f110165,plain,
( spl45_155
| spl45_5439
| spl45_1188 ),
inference(avatar_split_clause,[],[f110162,f14406,f86888,f1786]) ).
fof(f111402,plain,
( ~ gt(pv57,n2)
| spl45_3694 ),
inference(resolution,[],[f55885,f425]) ).
fof(f111403,plain,
( ~ spl45_5439
| spl45_3694 ),
inference(avatar_split_clause,[],[f111402,f55883,f86888]) ).
fof(f111431,plain,
( pv57 = sK39
| ~ spl45_179
| ~ spl45_749 ),
inference(forward_demodulation,[],[f10427,f2006]) ).
fof(f111456,plain,
( spl45_64
| ~ spl45_179
| ~ spl45_749 ),
inference(avatar_split_clause,[],[f111431,f10425,f2004,f1105]) ).
fof(f111480,plain,
( ~ leq(sK39,pv57)
| ~ spl45_179
| spl45_751 ),
inference(forward_demodulation,[],[f10437,f2006]) ).
fof(f111481,plain,
( ~ spl45_21
| ~ spl45_179
| spl45_751 ),
inference(avatar_split_clause,[],[f111480,f10435,f2004,f550]) ).
fof(f112301,plain,
( a_select3(id_ds1_filter,n4,sK40) != a_select3(id_ds1_filter,sK40,n4)
| spl45_24
| ~ spl45_749 ),
inference(superposition,[],[f567,f10427]) ).
fof(f112316,plain,
( a_select3(id_ds1_filter,n4,sK40) != a_select3(id_ds1_filter,n4,sK40)
| spl45_24
| ~ spl45_749
| ~ spl45_847 ),
inference(forward_demodulation,[],[f112301,f11447]) ).
fof(f112317,plain,
( $false
| spl45_24
| ~ spl45_749
| ~ spl45_847 ),
inference(trivial_inequality_removal,[],[f112316]) ).
fof(f112318,plain,
( spl45_24
| ~ spl45_749
| ~ spl45_847 ),
inference(avatar_contradiction_clause,[],[f112317]) ).
cnf(s1,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_3 ),
inference(sat_conversion,[],[f467]) ).
cnf(s2,plain,
spl45_1,
inference(sat_conversion,[],[f468]) ).
cnf(s3,plain,
spl45_2,
inference(sat_conversion,[],[f469]) ).
cnf(s4,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_8
| ~ spl45_9
| ~ spl45_10 ),
inference(sat_conversion,[],[f498]) ).
cnf(s5,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| ~ spl45_9
| ~ spl45_10
| spl45_11 ),
inference(sat_conversion,[],[f503]) ).
cnf(s6,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| ~ spl45_9
| ~ spl45_10
| spl45_12 ),
inference(sat_conversion,[],[f508]) ).
cnf(s7,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| ~ spl45_9
| ~ spl45_10
| spl45_13 ),
inference(sat_conversion,[],[f513]) ).
cnf(s8,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| ~ spl45_9
| ~ spl45_10
| ~ spl45_14 ),
inference(sat_conversion,[],[f518]) ).
cnf(s9,plain,
( ~ spl45_4
| spl45_15 ),
inference(sat_conversion,[],[f523]) ).
cnf(s10,plain,
( ~ spl45_4
| spl45_16 ),
inference(sat_conversion,[],[f528]) ).
cnf(s11,plain,
( ~ spl45_4
| spl45_17 ),
inference(sat_conversion,[],[f533]) ).
cnf(s12,plain,
( ~ spl45_4
| spl45_18 ),
inference(sat_conversion,[],[f538]) ).
cnf(s13,plain,
( ~ spl45_4
| ~ spl45_19 ),
inference(sat_conversion,[],[f543]) ).
cnf(s14,plain,
( ~ spl45_5
| spl45_20 ),
inference(sat_conversion,[],[f548]) ).
cnf(s15,plain,
( ~ spl45_5
| spl45_21 ),
inference(sat_conversion,[],[f553]) ).
cnf(s16,plain,
( ~ spl45_5
| spl45_22 ),
inference(sat_conversion,[],[f558]) ).
cnf(s17,plain,
( ~ spl45_5
| spl45_23 ),
inference(sat_conversion,[],[f563]) ).
cnf(s18,plain,
( ~ spl45_5
| ~ spl45_24 ),
inference(sat_conversion,[],[f568]) ).
cnf(s19,plain,
( ~ spl45_6
| spl45_25 ),
inference(sat_conversion,[],[f573]) ).
cnf(s20,plain,
( ~ spl45_6
| spl45_26 ),
inference(sat_conversion,[],[f578]) ).
cnf(s21,plain,
( ~ spl45_6
| spl45_27 ),
inference(sat_conversion,[],[f583]) ).
cnf(s22,plain,
( ~ spl45_6
| spl45_28 ),
inference(sat_conversion,[],[f588]) ).
cnf(s23,plain,
( ~ spl45_6
| ~ spl45_29 ),
inference(sat_conversion,[],[f593]) ).
cnf(s24,plain,
( ~ spl45_7
| spl45_30 ),
inference(sat_conversion,[],[f598]) ).
cnf(s25,plain,
( ~ spl45_7
| spl45_31 ),
inference(sat_conversion,[],[f603]) ).
cnf(s26,plain,
( ~ spl45_7
| spl45_32 ),
inference(sat_conversion,[],[f608]) ).
cnf(s27,plain,
( ~ spl45_7
| spl45_33 ),
inference(sat_conversion,[],[f613]) ).
cnf(s28,plain,
( ~ spl45_7
| ~ spl45_34 ),
inference(sat_conversion,[],[f618]) ).
cnf(s29,plain,
spl45_10,
inference(sat_conversion,[],[f619]) ).
cnf(s30,plain,
spl45_9,
inference(sat_conversion,[],[f620]) ).
cnf(s67,plain,
( ~ spl45_2
| spl45_86
| spl45_87 ),
inference(sat_conversion,[],[f1211]) ).
cnf(s126,plain,
( ~ spl45_2
| spl45_86
| ~ spl45_142
| spl45_143 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s156,plain,
( ~ spl45_2
| spl45_86
| spl45_143
| spl45_155
| spl45_167
| spl45_179
| spl45_191
| ~ spl45_202
| spl45_203 ),
inference(sat_conversion,[],[f2191]) ).
cnf(s176,plain,
( ~ spl45_30
| ~ spl45_32
| spl45_60 ),
inference(sat_conversion,[],[f3185]) ).
cnf(s222,plain,
spl45_44,
inference(sat_conversion,[],[f3586]) ).
cnf(s290,plain,
( ~ spl45_31
| ~ spl45_33
| spl45_34
| ~ spl45_60 ),
inference(sat_conversion,[],[f4041]) ).
cnf(s319,plain,
( ~ spl45_26
| ~ spl45_28
| spl45_57 ),
inference(sat_conversion,[],[f4331]) ).
cnf(s327,plain,
( ~ spl45_17
| ~ spl45_18
| spl45_119 ),
inference(sat_conversion,[],[f4358]) ).
cnf(s386,plain,
( ~ spl45_15
| ~ spl45_16
| spl45_19
| ~ spl45_119 ),
inference(sat_conversion,[],[f4786]) ).
cnf(s738,plain,
( ~ spl45_1
| spl45_202 ),
inference(sat_conversion,[],[f6254]) ).
cnf(s1920,plain,
( ~ spl45_23
| spl45_76
| ~ spl45_739
| spl45_740
| spl45_741
| spl45_742 ),
inference(sat_conversion,[],[f10396]) ).
cnf(s1921,plain,
( ~ spl45_23
| spl45_76
| spl45_741
| spl45_742
| ~ spl45_743 ),
inference(sat_conversion,[],[f10401]) ).
cnf(s1922,plain,
( ~ spl45_23
| spl45_76
| spl45_742
| ~ spl45_744 ),
inference(sat_conversion,[],[f10406]) ).
cnf(s1923,plain,
( ~ spl45_23
| spl45_76
| ~ spl45_745 ),
inference(sat_conversion,[],[f10411]) ).
cnf(s1925,plain,
( ~ spl45_23
| spl45_76
| spl45_740
| spl45_741
| spl45_742
| spl45_748
| spl45_749
| ~ spl45_750 ),
inference(sat_conversion,[],[f10433]) ).
cnf(s1926,plain,
( ~ spl45_23
| spl45_76
| spl45_740
| spl45_741
| spl45_742
| spl45_749
| ~ spl45_751 ),
inference(sat_conversion,[],[f10438]) ).
cnf(s1936,plain,
( ~ spl45_20
| ~ spl45_22
| spl45_51 ),
inference(sat_conversion,[],[f10497]) ).
cnf(s1937,plain,
( ~ spl45_20
| ~ spl45_22
| spl45_48 ),
inference(sat_conversion,[],[f10498]) ).
cnf(s2123,plain,
( ~ spl45_44
| ~ spl45_51
| ~ spl45_262
| ~ spl45_833
| spl45_845 ),
inference(sat_conversion,[],[f11436]) ).
cnf(s2147,plain,
( ~ spl45_3
| ~ spl45_20
| ~ spl45_22
| spl45_828
| ~ spl45_869 ),
inference(sat_conversion,[],[f11620]) ).
cnf(s2316,plain,
spl45_262,
inference(sat_conversion,[],[f12650]) ).
cnf(s2569,plain,
spl45_62,
inference(sat_conversion,[],[f14303]) ).
cnf(s2570,plain,
spl45_485,
inference(sat_conversion,[],[f14305]) ).
cnf(s2571,plain,
spl45_511,
inference(sat_conversion,[],[f14306]) ).
cnf(s2574,plain,
spl45_498,
inference(sat_conversion,[],[f14310]) ).
cnf(s2662,plain,
( ~ spl45_155
| spl45_1192 ),
inference(sat_conversion,[],[f14730]) ).
cnf(s2722,plain,
spl45_503,
inference(sat_conversion,[],[f14875]) ).
cnf(s2732,plain,
( ~ spl45_65
| ~ spl45_167
| spl45_739 ),
inference(sat_conversion,[],[f15031]) ).
cnf(s2789,plain,
( ~ spl45_20
| spl45_869 ),
inference(sat_conversion,[],[f15252]) ).
cnf(s3042,plain,
( ~ spl45_167
| spl45_501
| ~ spl45_503 ),
inference(sat_conversion,[],[f18462]) ).
cnf(s3202,plain,
~ spl45_1299,
inference(sat_conversion,[],[f20251]) ).
cnf(s5044,plain,
spl45_617,
inference(sat_conversion,[],[f33487]) ).
cnf(s6434,plain,
( spl45_24
| ~ spl45_76
| ~ spl45_845 ),
inference(sat_conversion,[],[f42794]) ).
cnf(s7953,plain,
( ~ spl45_25
| ~ spl45_27
| spl45_29
| ~ spl45_57 ),
inference(sat_conversion,[],[f53425]) ).
cnf(s8614,plain,
( ~ spl45_191
| spl45_1192 ),
inference(sat_conversion,[],[f55548]) ).
cnf(s8926,plain,
( spl45_39
| ~ spl45_87 ),
inference(sat_conversion,[],[f56539]) ).
cnf(s9379,plain,
( ~ spl45_501
| spl45_1192 ),
inference(sat_conversion,[],[f58641]) ).
cnf(s10253,plain,
( ~ spl45_191
| spl45_3916 ),
inference(sat_conversion,[],[f63113]) ).
cnf(s10362,plain,
( ~ spl45_191
| spl45_3886 ),
inference(sat_conversion,[],[f63448]) ).
cnf(s10958,plain,
( ~ spl45_65
| ~ spl45_76
| spl45_87 ),
inference(sat_conversion,[],[f65630]) ).
cnf(s10990,plain,
( ~ spl45_87
| spl45_833 ),
inference(sat_conversion,[],[f65703]) ).
cnf(s11396,plain,
( ~ spl45_11
| ~ spl45_13
| spl45_106 ),
inference(sat_conversion,[],[f66598]) ).
cnf(s13476,plain,
( spl45_142
| ~ spl45_1188 ),
inference(sat_conversion,[],[f74264]) ).
cnf(s13507,plain,
( ~ spl45_1
| ~ spl45_3802 ),
inference(sat_conversion,[],[f74483]) ).
cnf(s14286,plain,
( spl45_810
| ~ spl45_3916 ),
inference(sat_conversion,[],[f79791]) ).
cnf(s14292,plain,
( ~ spl45_48
| ~ spl45_511
| ~ spl45_810
| spl45_847 ),
inference(sat_conversion,[],[f79830]) ).
cnf(s14510,plain,
( ~ spl45_1192
| spl45_4708 ),
inference(sat_conversion,[],[f80630]) ).
cnf(s14525,plain,
( ~ spl45_3886
| spl45_4739 ),
inference(sat_conversion,[],[f80691]) ).
cnf(s14547,plain,
( ~ spl45_48
| ~ spl45_498
| ~ spl45_3694
| spl45_3780 ),
inference(sat_conversion,[],[f80895]) ).
cnf(s15808,plain,
( spl45_24
| ~ spl45_742
| ~ spl45_5011 ),
inference(sat_conversion,[],[f89913]) ).
cnf(s15844,plain,
( spl45_64
| ~ spl45_191
| ~ spl45_748 ),
inference(sat_conversion,[],[f89989]) ).
cnf(s15846,plain,
( ~ spl45_21
| ~ spl45_191
| spl45_750 ),
inference(sat_conversion,[],[f89993]) ).
cnf(s17326,plain,
( ~ spl45_21
| ~ spl45_86
| spl45_745 ),
inference(sat_conversion,[],[f95050]) ).
cnf(s17332,plain,
( ~ spl45_39
| ~ spl45_86
| spl45_1299 ),
inference(sat_conversion,[],[f95058]) ).
cnf(s18696,plain,
( ~ spl45_21
| spl45_64
| spl45_65 ),
inference(sat_conversion,[],[f99660]) ).
cnf(s18716,plain,
( ~ spl45_143
| ~ spl45_828
| spl45_5011 ),
inference(sat_conversion,[],[f99879]) ).
cnf(s18756,plain,
( ~ spl45_21
| ~ spl45_143
| spl45_744 ),
inference(sat_conversion,[],[f99928]) ).
cnf(s18780,plain,
( ~ spl45_48
| ~ spl45_62
| ~ spl45_4708
| spl45_5011 ),
inference(sat_conversion,[],[f99940]) ).
cnf(s19554,plain,
( ~ spl45_8
| ~ spl45_12
| spl45_14
| ~ spl45_106 ),
inference(sat_conversion,[],[f102802]) ).
cnf(s19857,plain,
( spl45_24
| ~ spl45_64
| ~ spl45_828 ),
inference(sat_conversion,[],[f104011]) ).
cnf(s19954,plain,
( ~ spl45_179
| spl45_1192 ),
inference(sat_conversion,[],[f104295]) ).
cnf(s19956,plain,
( ~ spl45_179
| spl45_3886 ),
inference(sat_conversion,[],[f104297]) ).
cnf(s20146,plain,
( ~ spl45_203
| ~ spl45_617
| spl45_3802 ),
inference(sat_conversion,[],[f104805]) ).
cnf(s20255,plain,
( ~ spl45_48
| ~ spl45_485
| ~ spl45_4739
| spl45_4746 ),
inference(sat_conversion,[],[f105005]) ).
cnf(s20256,plain,
( ~ spl45_167
| ~ spl45_828
| spl45_4746 ),
inference(sat_conversion,[],[f105006]) ).
cnf(s20257,plain,
( spl45_24
| ~ spl45_740
| ~ spl45_4746 ),
inference(sat_conversion,[],[f105007]) ).
cnf(s20753,plain,
( spl45_24
| ~ spl45_741
| ~ spl45_3780 ),
inference(sat_conversion,[],[f106655]) ).
cnf(s20861,plain,
( spl45_64
| ~ spl45_155
| ~ spl45_741 ),
inference(sat_conversion,[],[f107306]) ).
cnf(s20862,plain,
( ~ spl45_21
| ~ spl45_155
| spl45_743 ),
inference(sat_conversion,[],[f107309]) ).
cnf(s21549,plain,
( spl45_155
| spl45_1188
| spl45_5439 ),
inference(sat_conversion,[],[f110165]) ).
cnf(s21789,plain,
( spl45_3694
| ~ spl45_5439 ),
inference(sat_conversion,[],[f111403]) ).
cnf(s21814,plain,
( spl45_64
| ~ spl45_179
| ~ spl45_749 ),
inference(sat_conversion,[],[f111456]) ).
cnf(s21832,plain,
( ~ spl45_21
| ~ spl45_179
| spl45_751 ),
inference(sat_conversion,[],[f111481]) ).
cnf(s22026,plain,
( spl45_24
| ~ spl45_749
| ~ spl45_847 ),
inference(sat_conversion,[],[f112318]) ).
cnf(s22636,plain,
( ~ spl45_44
| ~ spl45_51
| ~ spl45_833
| spl45_845 ),
inference(rat,[],[s2123,s2316]) ).
cnf(s23842,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| ~ spl45_14 ),
inference(rat,[],[s8,s29,s30]) ).
cnf(s23843,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_13 ),
inference(rat,[],[s7,s29,s30]) ).
cnf(s23844,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_12 ),
inference(rat,[],[s6,s29,s30]) ).
cnf(s23845,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_11 ),
inference(rat,[],[s5,s29,s30]) ).
cnf(s23846,plain,
( ~ spl45_1
| ~ spl45_2
| spl45_4
| spl45_5
| spl45_6
| spl45_7
| spl45_8 ),
inference(rat,[],[s4,s29,s30]) ).
cnf(s23856,plain,
~ spl45_3802,
inference(rat,[],[s13507,s2]) ).
cnf(s23909,plain,
spl45_202,
inference(rat,[],[s738,s2]) ).
cnf(s23954,plain,
~ spl45_203,
inference(rat,[],[s20146,s5044,s23856]) ).
cnf(s24087,plain,
spl45_3,
inference(rat,[],[s1,s3,s2]) ).
cnf(s24092,plain,
( spl45_7
| spl45_6
| spl45_4
| spl45_5 ),
inference(rat,[],[s11396,s19554,s23844,s23845,s23843,s23842,s23846,s2,s3]) ).
cnf(s24093,plain,
~ spl45_7,
inference(rat,[],[s176,s290,s24,s25,s26,s27,s28]) ).
cnf(s24094,plain,
~ spl45_6,
inference(rat,[],[s7953,s319,s19,s20,s21,s22,s23]) ).
cnf(s24095,plain,
( spl45_87
| ~ spl45_5 ),
inference(rat,[],[s1923,s17326,s10958,s67,s17,s18696,s19857,s2147,s16,s2789,s14,s18,s15,s3,s24087]) ).
cnf(s24096,plain,
( ~ spl45_143
| ~ spl45_5 ),
inference(rat,[],[s15808,s1922,s18716,s18756,s17,s15,s2147,s2789,s6434,s22636,s10990,s24095,s1936,s14,s16,s18,s222,s24087]) ).
cnf(s24097,plain,
( spl45_1192
| ~ spl45_5 ),
inference(rat,[],[s156,s3042,s2662,s8614,s9379,s19954,s17332,s8926,s24095,s24096,s3,s23909,s23954,s2722,s3202]) ).
cnf(s24098,plain,
( ~ spl45_191
| spl45_741
| ~ spl45_5 ),
inference(rat,[],[s1925,s22026,s20257,s14292,s20255,s14286,s14525,s10253,s10362,s15844,s15846,s17,s15,s19857,s2147,s2789,s6434,s22636,s10990,s24095,s1936,s15808,s18780,s14510,s24097,s1937,s14,s16,s18,s2571,s2570,s2569,s222,s24087]) ).
cnf(s24099,plain,
( ~ spl45_179
| spl45_741
| ~ spl45_5 ),
inference(rat,[],[s20255,s20257,s14525,s1926,s19956,s21814,s21832,s17,s15,s19857,s2147,s2789,s6434,s22636,s10990,s24095,s1936,s15808,s18780,s14510,s24097,s1937,s14,s16,s18,s2570,s2569,s222,s24087]) ).
cnf(s24100,plain,
( spl45_155
| ~ spl45_5 ),
inference(rat,[],[s1920,s20257,s2732,s20256,s156,s24099,s24098,s20753,s14547,s21789,s21549,s17,s18696,s19857,s2147,s2789,s15,s6434,s22636,s10990,s1936,s13476,s126,s24096,s17332,s8926,s24095,s15808,s18780,s14510,s24097,s1937,s14,s16,s18,s3,s23909,s23954,s2574,s2569,s3202,s222,s24087]) ).
cnf(s24101,plain,
~ spl45_5,
inference(rat,[],[s1921,s20861,s20862,s24100,s15808,s18780,s14510,s24097,s6434,s22636,s10990,s24095,s19857,s1936,s1937,s2147,s2789,s14,s15,s16,s17,s18,s2569,s222,s24087]) ).
cnf(s24102,plain,
spl45_4,
inference(rat,[],[s24092,s24093,s24094,s24101]) ).
cnf(s24103,plain,
~ spl45_19,
inference(rat,[],[s13,s24102]) ).
cnf(s24104,plain,
spl45_18,
inference(rat,[],[s12,s24102]) ).
cnf(s24105,plain,
spl45_17,
inference(rat,[],[s11,s24102]) ).
cnf(s24106,plain,
spl45_16,
inference(rat,[],[s10,s24102]) ).
cnf(s24107,plain,
spl45_15,
inference(rat,[],[s9,s24102]) ).
cnf(s24120,plain,
spl45_119,
inference(rat,[],[s327,s24104,s24105]) ).
cnf(s24121,plain,
$false,
inference(rat,[],[s386,s24120,s24103,s24106,s24107]) ).
fof(f112319,plain,
$false,
inference(avatar_sat_refutation,[],[s24121]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV111+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.19 % Computer : n007.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 09:53:25 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 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
% 15.45/2.43 % (2292401)Will run a generic schedule for satisfiability detection.
% 15.45/2.43 % (2292408)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=52403417:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.45/2.43 % (2292406)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2976552891_2999 on theBenchmark for (2999ds/0Mi)
% 15.45/2.43 % (2292409)dis+10_1_sil=32000:sp=arity:random_seed=80933356:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.45/2.43 % (2292412)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1014718843:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.45/2.43 % (2292410)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=33073611:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.45/2.43 % (2292411)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1828329843:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.45/2.43 % (2292407)% WARNING: option uhcvi not known.
% 15.45/2.43 % (2292407)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=334036757:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.45/2.43 % TRYING [1]
% 15.45/2.43 % TRYING [2]
% 15.45/2.43 % (2292409)Instruction limit reached!
% 15.45/2.43 % (2292409)------------------------------
% 15.45/2.43 % (2292409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.43 % (2292409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.43 % (2292409)CaDiCaL version: 2.1.3
% 15.45/2.43 % (2292409)Termination reason: Instruction limit
% 15.45/2.43 % (2292409)Termination phase: Saturation
% 15.45/2.43 % (2292409)Time elapsed: 0.059 s
% 15.45/2.43 % (2292409)Peak memory usage: 13 MB
% 15.45/2.43 % (2292409)Instructions burned: 105 (million)
% 15.45/2.43 % TRYING [3]
% 15.45/2.43 % (2292410)Instruction limit reached!
% 15.45/2.43 % (2292410)------------------------------
% 15.45/2.43 % (2292410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.43 % (2292410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.43 % (2292410)CaDiCaL version: 2.1.3
% 15.45/2.43 % (2292410)Termination reason: Instruction limit
% 15.45/2.43 % (2292410)Termination phase: Saturation
% 15.45/2.43 % (2292410)Time elapsed: 0.064 s
% 15.45/2.43 % (2292410)Peak memory usage: 13 MB
% 15.45/2.43 % (2292410)Instructions burned: 116 (million)
% 15.45/2.43 % (2292411)Instruction limit reached!
% 15.45/2.43 % (2292411)------------------------------
% 15.45/2.43 % (2292411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.43 % (2292411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.43 % (2292411)CaDiCaL version: 2.1.3
% 15.45/2.43 % (2292411)Termination reason: Instruction limit
% 15.45/2.43 % (2292411)Termination phase: Saturation
% 15.45/2.43 % (2292411)Time elapsed: 0.075 s
% 15.45/2.43 % (2292411)Peak memory usage: 13 MB
% 15.45/2.43 % (2292411)Instructions burned: 133 (million)
% 15.45/2.43 % (2292420)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1568423707:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.45/2.43 % (2292421)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2925814322:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.45/2.43 % (2292422)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4019451370:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.45/2.43 % (2292412)Instruction limit reached!
% 15.45/2.43 % (2292412)------------------------------
% 15.45/2.43 % (2292412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.43 % (2292412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.43 % (2292412)CaDiCaL version: 2.1.3
% 15.45/2.43 % (2292412)Termination reason: Instruction limit
% 15.45/2.43 % (2292412)Termination phase: Saturation
% 15.45/2.43 % (2292412)Time elapsed: 0.097 s
% 15.45/2.43 % (2292412)Peak memory usage: 14 MB
% 15.45/2.43 % (2292412)Instructions burned: 159 (million)
% 15.45/2.43 % TRYING [1]
% 15.45/2.43 % TRYING [2]
% 15.45/2.43 % TRYING [3]
% 15.45/2.43 % (2292426)ott-21_1_sil=16000:fs=off:random_seed=150163933:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.45/2.43 % TRYING [4]
% 15.45/2.43 % (2292421)Instruction limit reached!
% 15.45/2.43 % (2292421)------------------------------
% 15.45/2.43 % (2292421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.43 % (2292421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.13/6.36 % (2292421)CaDiCaL version: 2.1.3
% 43.13/6.36 % (2292421)Termination reason: Instruction limit
% 43.13/6.36 % (2292421)Termination phase: Saturation
% 43.13/6.36 % (2292421)Time elapsed: 0.073 s
% 43.13/6.36 % (2292421)Peak memory usage: 13 MB
% 43.13/6.36 % (2292421)Instructions burned: 132 (million)
% 43.13/6.36 % TRYING [4]
% 43.13/6.36 % (2292428)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2865418540:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 43.13/6.36 % (2292426)Instruction limit reached!
% 43.13/6.36 % (2292426)------------------------------
% 43.13/6.36 % (2292426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.13/6.36 % (2292426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.13/6.36 % (2292426)CaDiCaL version: 2.1.3
% 43.13/6.36 % (2292426)Termination reason: Instruction limit
% 43.13/6.36 % (2292426)Termination phase: Saturation
% 43.13/6.36 % (2292426)Time elapsed: 0.089 s
% 43.13/6.36 % (2292426)Peak memory usage: 13 MB
% 43.13/6.36 % (2292426)Instructions burned: 181 (million)
% 43.13/6.36 % (2292430)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3207415351:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 43.13/6.36 % TRYING [1]
% 43.13/6.36 % TRYING [2]
% 43.13/6.36 % TRYING [5]
% 43.13/6.36 % TRYING [3]
% 43.13/6.36 % (2292420)Instruction limit reached!
% 43.13/6.36 % (2292420)------------------------------
% 43.13/6.36 % (2292420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.13/6.36 % (2292420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.13/6.36 % (2292420)CaDiCaL version: 2.1.3
% 43.13/6.36 % (2292420)Termination reason: Instruction limit
% 43.13/6.36 % (2292420)Termination phase: Finite model building constraint generation
% 43.13/6.36 % (2292420)Time elapsed: 0.267 s
% 43.13/6.36 % (2292420)Peak memory usage: 37 MB
% 43.13/6.36 % (2292420)Instructions burned: 715 (million)
% 43.13/6.36 % (2292432)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3704608060:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 43.13/6.36 % (2292422)Instruction limit reached!
% 43.13/6.36 % (2292422)------------------------------
% 43.13/6.36 % (2292422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.13/6.36 % (2292422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.13/6.36 % (2292422)CaDiCaL version: 2.1.3
% 43.13/6.36 % (2292422)Termination reason: Instruction limit
% 43.13/6.36 % (2292422)Termination phase: Saturation
% 43.13/6.36 % (2292422)Time elapsed: 0.318 s
% 43.13/6.36 % (2292422)Peak memory usage: 15 MB
% 43.13/6.36 % (2292422)Instructions burned: 685 (million)
% 43.13/6.36 % (2292434)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3238257956:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 43.13/6.36 % (2292428)Instruction limit reached!
% 43.13/6.36 % (2292428)------------------------------
% 43.13/6.36 % (2292428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.13/6.36 % (2292428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.13/6.36 % (2292428)CaDiCaL version: 2.1.3
% 43.13/6.36 % (2292428)Termination reason: Instruction limit
% 43.13/6.36 % (2292428)Termination phase: Saturation
% 43.13/6.36 % (2292428)Time elapsed: 0.296 s
% 43.13/6.36 % (2292428)Peak memory usage: 15 MB
% 43.13/6.36 % (2292428)Instructions burned: 477 (million)
% 43.13/6.36 % (2292436)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2094496565:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 43.13/6.36 % (2292430)Instruction limit reached!
% 43.13/6.36 % (2292430)------------------------------
% 43.13/6.36 % (2292430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.13/6.36 % (2292430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.13/6.36 % (2292430)CaDiCaL version: 2.1.3
% 43.13/6.36 % (2292430)Termination reason: Instruction limit
% 43.13/6.36 % (2292430)Termination phase: Finite model building SAT solving
% 43.13/6.36 % (2292430)Time elapsed: 0.355 s
% 43.13/6.36 % (2292430)Peak memory usage: 29 MB
% 43.13/6.36 % (2292430)Instructions burned: 867 (million)
% 43.13/6.36 % TRYING [5]
% 43.13/6.36 % (2292438)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1107496271:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 43.13/6.36 % (2292434)Instruction limit reached!
% 43.13/6.36 % (2292434)------------------------------
% 43.13/6.36 % (2292434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.84/12.63 % (2292434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.84/12.63 % (2292434)CaDiCaL version: 2.1.3
% 87.84/12.63 % (2292434)Termination reason: Instruction limit
% 87.84/12.63 % (2292434)Termination phase: Finite model building constraint generation
% 87.84/12.63 % (2292434)Time elapsed: 0.405 s
% 87.84/12.63 % (2292434)Peak memory usage: 102 MB
% 87.84/12.63 % (2292434)Instructions burned: 891 (million)
% 87.84/12.63 % (2292440)fmb+10_1_sil=64000:random_seed=589411151:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 87.84/12.63 % TRYING [1]
% 87.84/12.63 % TRYING [2]
% 87.84/12.63 % TRYING [3]
% 87.84/12.63 % (2292436)Instruction limit reached!
% 87.84/12.63 % (2292436)------------------------------
% 87.84/12.63 % (2292436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.84/12.63 % (2292436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.84/12.63 % (2292436)CaDiCaL version: 2.1.3
% 87.84/12.63 % (2292436)Termination reason: Instruction limit
% 87.84/12.63 % (2292436)Termination phase: Saturation
% 87.84/12.63 % (2292436)Time elapsed: 0.421 s
% 87.84/12.63 % (2292436)Peak memory usage: 18 MB
% 87.84/12.63 % (2292436)Instructions burned: 693 (million)
% 87.84/12.63 % (2292442)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1704970064:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 87.84/12.63 % TRYING [20]
% 87.84/12.63 % TRYING [4]
% 87.84/12.63 % (2292438)Instruction limit reached!
% 87.84/12.63 % (2292438)------------------------------
% 87.84/12.63 % (2292438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.84/12.63 % (2292438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.84/12.63 % (2292438)CaDiCaL version: 2.1.3
% 87.84/12.63 % (2292438)Termination reason: Instruction limit
% 87.84/12.63 % (2292438)Termination phase: Saturation
% 87.84/12.63 % (2292438)Time elapsed: 0.436 s
% 87.84/12.63 % (2292438)Peak memory usage: 20 MB
% 87.84/12.63 % (2292438)Instructions burned: 879 (million)
% 87.84/12.63 % (2292444)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=673139367:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 87.84/12.63 % (2292432)Instruction limit reached!
% 87.84/12.63 % (2292432)------------------------------
% 87.84/12.63 % (2292432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.84/12.63 % (2292432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.84/12.63 % (2292432)CaDiCaL version: 2.1.3
% 87.84/12.63 % (2292432)Termination reason: Instruction limit
% 87.84/12.63 % (2292432)Termination phase: Saturation
% 87.84/12.63 % (2292432)Time elapsed: 0.695 s
% 87.84/12.63 % (2292432)Peak memory usage: 21 MB
% 87.84/12.63 % (2292432)Instructions burned: 1179 (million)
% 87.84/12.63 % (2292446)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=869915307:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 87.84/12.63 % TRYING [8]
% 87.84/12.63 % (2292444)Instruction limit reached!
% 87.84/12.63 % (2292444)------------------------------
% 87.84/12.63 % (2292444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.84/12.63 % (2292444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.84/12.63 % (2292444)CaDiCaL version: 2.1.3
% 87.84/12.63 % (2292444)Termination reason: Instruction limit
% 87.84/12.63 % (2292444)Termination phase: Finite model building constraint generation
% 87.84/12.63 % (2292444)Time elapsed: 0.319 s
% 87.84/12.63 % (2292444)Peak memory usage: 63 MB
% 87.84/12.63 % (2292444)Instructions burned: 923 (million)
% 87.84/12.63 % (2292448)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=697621158:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 87.84/12.63 % TRYING [5]
% 87.84/12.63 % TRYING [6]
% 87.84/12.63 % (2292448)Instruction limit reached!
% 87.84/12.63 % (2292448)------------------------------
% 87.84/12.63 % (2292448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.84/12.63 % (2292448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.84/12.63 % (2292448)CaDiCaL version: 2.1.3
% 87.84/12.63 % (2292448)Termination reason: Instruction limit
% 87.84/12.63 % (2292448)Termination phase: Saturation
% 87.84/12.63 % (2292448)Time elapsed: 0.711 s
% 87.84/12.63 % (2292448)Peak memory usage: 25 MB
% 87.84/12.63 % (2292448)Instructions burned: 1473 (million)
% 87.84/12.63 % (2292450)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4031591088:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 87.84/12.63 % (2292450)Cannot represent all propositional literals internally
% 87.84/12.63 % (2292450)Refutation not found, incomplete strategy
% 177.16/27.60 % (2292450)------------------------------
% 177.16/27.60 % (2292450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.60 % (2292450)CaDiCaL version: 2.1.3
% 177.16/27.60 % (2292450)Termination reason: Refutation not found, incomplete strategy
% 177.16/27.60 % (2292450)Time elapsed: 0.042 s
% 177.16/27.60 % (2292450)Peak memory usage: 12 MB
% 177.16/27.60 % (2292450)Instructions burned: 90 (million)
% 177.16/27.60 % (2292450)------------------------------
% 177.16/27.60 % (2292450)------------------------------
% 177.16/27.60 % (2292452)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2464222756:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 177.16/27.60 % TRYING [16]
% 177.16/27.60 % (2292452)Instruction limit reached!
% 177.16/27.60 % (2292452)------------------------------
% 177.16/27.60 % (2292452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.60 % (2292452)CaDiCaL version: 2.1.3
% 177.16/27.60 % (2292452)Termination reason: Instruction limit
% 177.16/27.60 % (2292452)Termination phase: Finite model building constraint generation
% 177.16/27.60 % (2292452)Time elapsed: 0.798 s
% 177.16/27.60 % (2292452)Peak memory usage: 125 MB
% 177.16/27.60 % (2292452)Instructions burned: 2175 (million)
% 177.16/27.60 % (2292454)ott-2_1_sil=16000:newcnf=on:random_seed=1255948414:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 177.16/27.60 % (2292454)Instruction limit reached!
% 177.16/27.60 % (2292454)------------------------------
% 177.16/27.60 % (2292454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.60 % (2292454)CaDiCaL version: 2.1.3
% 177.16/27.60 % (2292454)Termination reason: Instruction limit
% 177.16/27.60 % (2292454)Termination phase: Saturation
% 177.16/27.60 % (2292454)Time elapsed: 0.518 s
% 177.16/27.60 % (2292454)Peak memory usage: 17 MB
% 177.16/27.60 % (2292454)Instructions burned: 870 (million)
% 177.16/27.60 % (2292446)Instruction limit reached!
% 177.16/27.60 % (2292446)------------------------------
% 177.16/27.60 % (2292446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.60 % (2292446)CaDiCaL version: 2.1.3
% 177.16/27.60 % (2292446)Termination reason: Instruction limit
% 177.16/27.60 % (2292446)Termination phase: Saturation
% 177.16/27.60 % (2292446)Time elapsed: 2.474 s
% 177.16/27.60 % (2292446)Peak memory usage: 26 MB
% 177.16/27.60 % (2292446)Instructions burned: 5132 (million)
% 177.16/27.60 % (2292456)ott+10_1_sil=32000:tgt=ground:random_seed=2102852995:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 177.16/27.60 % (2292457)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1150161993:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 177.16/27.60 % TRYING [1]
% 177.16/27.60 % TRYING [2]
% 177.16/27.60 % TRYING [6]
% 177.16/27.60 % TRYING [3]
% 177.16/27.60 % TRYING [4]
% 177.16/27.60 % TRYING [5]
% 177.16/27.60 % (2292442)Instruction limit reached!
% 177.16/27.60 % (2292442)------------------------------
% 177.16/27.60 % (2292442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.60 % (2292442)CaDiCaL version: 2.1.3
% 177.16/27.60 % (2292442)Termination reason: Instruction limit
% 177.16/27.60 % (2292442)Termination phase: Finite model building constraint generation
% 177.16/27.60 % (2292442)Time elapsed: 3.328 s
% 177.16/27.60 % (2292442)Peak memory usage: 595 MB
% 177.16/27.60 % (2292442)Instructions burned: 9515 (million)
% 177.16/27.60 % (2292460)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4077318387:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 177.16/27.60 % TRYING [7]
% 177.16/27.60 % TRYING [6]
% 177.16/27.60 % (2292460)Instruction limit reached!
% 177.16/27.60 % (2292460)------------------------------
% 177.16/27.60 % (2292460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.60 % (2292460)CaDiCaL version: 2.1.3
% 177.16/27.60 % (2292460)Termination reason: Instruction limit
% 177.16/27.60 % (2292460)Termination phase: Saturation
% 177.16/27.60 % (2292460)Time elapsed: 1.732 s
% 177.16/27.60 % (2292460)Peak memory usage: 27 MB
% 177.16/27.60 % (2292460)Instructions burned: 3512 (million)
% 177.16/27.60 % (2292462)dis+21_1_sil=32000:sas=cadical:random_seed=3839481491:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 177.16/27.60 % (2292456)Instruction limit reached!
% 177.16/27.60 % (2292456)------------------------------
% 177.16/27.60 % (2292456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.60 % (2292456)CaDiCaL version: 2.1.3
% 177.16/27.60 % (2292456)Termination reason: Instruction limit
% 177.16/27.60 % (2292456)Termination phase: Saturation
% 177.16/27.60 % (2292456)Time elapsed: 2.872 s
% 177.16/27.60 % (2292456)Peak memory usage: 57 MB
% 177.16/27.60 % (2292456)Instructions burned: 5114 (million)
% 177.16/27.60 % (2292464)ott+11_1_sil=16000:gs=on:random_seed=617823775:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 177.16/27.60 % (2292464)Instruction limit reached!
% 177.16/27.60 % (2292464)------------------------------
% 177.16/27.60 % (2292464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.60 % (2292464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292464)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292464)Termination reason: Instruction limit
% 177.16/27.61 % (2292464)Termination phase: Saturation
% 177.16/27.61 % (2292464)Time elapsed: 1.370 s
% 177.16/27.61 % (2292464)Peak memory usage: 28 MB
% 177.16/27.61 % (2292464)Instructions burned: 2253 (million)
% 177.16/27.61 % (2292466)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2086042737:fmbsr=1.6:i=67534_2921 on theBenchmark for (2921ds/67534Mi)
% 177.16/27.61 % (2292462)Instruction limit reached!
% 177.16/27.61 % (2292462)------------------------------
% 177.16/27.61 % (2292462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292462)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292462)Termination reason: Instruction limit
% 177.16/27.61 % (2292462)Termination phase: Saturation
% 177.16/27.61 % (2292462)Time elapsed: 1.978 s
% 177.16/27.61 % (2292462)Peak memory usage: 34 MB
% 177.16/27.61 % (2292462)Instructions burned: 3774 (million)
% 177.16/27.61 % (2292468)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2996854878:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2918 on theBenchmark for (2918ds/4591Mi)
% 177.16/27.61 % TRYING [7]
% 177.16/27.61 % TRYING [7]
% 177.16/27.61 % TRYING [7]
% 177.16/27.61 % (2292440)Instruction limit reached!
% 177.16/27.61 % (2292440)------------------------------
% 177.16/27.61 % (2292440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292440)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292440)Termination reason: Instruction limit
% 177.16/27.61 % (2292440)Termination phase: Finite model building constraint generation
% 177.16/27.61 % (2292440)Time elapsed: 8.404 s
% 177.16/27.61 % (2292440)Peak memory usage: 215 MB
% 177.16/27.61 % (2292440)Instructions burned: 22062 (million)
% 177.16/27.61 % (2292470)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2313243741:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 177.16/27.61 % (2292468)Instruction limit reached!
% 177.16/27.61 % (2292468)------------------------------
% 177.16/27.61 % (2292468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292468)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292468)Termination reason: Instruction limit
% 177.16/27.61 % (2292468)Termination phase: Saturation
% 177.16/27.61 % (2292468)Time elapsed: 1.957 s
% 177.16/27.61 % (2292468)Peak memory usage: 37 MB
% 177.16/27.61 % (2292468)Instructions burned: 4594 (million)
% 177.16/27.61 % (2292472)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1005987110:i=5211_2898 on theBenchmark for (2898ds/5211Mi)
% 177.16/27.61 % TRYING [8]
% 177.16/27.61 % (2292472)Instruction limit reached!
% 177.16/27.61 % (2292472)------------------------------
% 177.16/27.61 % (2292472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292472)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292472)Termination reason: Instruction limit
% 177.16/27.61 % (2292472)Termination phase: Saturation
% 177.16/27.61 % (2292472)Time elapsed: 2.262 s
% 177.16/27.61 % (2292472)Peak memory usage: 34 MB
% 177.16/27.61 % (2292472)Instructions burned: 5213 (million)
% 177.16/27.61 % (2292474)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=514580260:i=5497:nm=2_2876 on theBenchmark for (2876ds/5497Mi)
% 177.16/27.61 % TRYING [17]
% 177.16/27.61 % (2292474)Instruction limit reached!
% 177.16/27.61 % (2292474)------------------------------
% 177.16/27.61 % (2292474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292474)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292474)Termination reason: Instruction limit
% 177.16/27.61 % (2292474)Termination phase: Finite model building constraint generation
% 177.16/27.61 % (2292474)Time elapsed: 1.885 s
% 177.16/27.61 % (2292474)Peak memory usage: 350 MB
% 177.16/27.61 % (2292474)Instructions burned: 5499 (million)
% 177.16/27.61 % (2292476)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2106861662:fmbsr=2:i=46332_2856 on theBenchmark for (2856ds/46332Mi)
% 177.16/27.61 % TRYING [15]
% 177.16/27.61 % TRYING [8]
% 177.16/27.61 % (2292408)Instruction limit reached!
% 177.16/27.61 % (2292408)------------------------------
% 177.16/27.61 % (2292408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292408)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292408)Termination reason: Instruction limit
% 177.16/27.61 % (2292408)Termination phase: Saturation
% 177.16/27.61 % (2292408)Time elapsed: 22.081 s
% 177.16/27.61 % (2292408)Peak memory usage: 819 MB
% 177.16/27.61 % (2292408)Instructions burned: 88026 (million)
% 177.16/27.61 % (2292478)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2738847116:i=14071_2778 on theBenchmark for (2778ds/14071Mi)
% 177.16/27.61 % TRYING [12]
% 177.16/27.61 % (2292457)Instruction limit reached!
% 177.16/27.61 % (2292457)------------------------------
% 177.16/27.61 % (2292457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292457)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292457)Termination reason: Instruction limit
% 177.16/27.61 % (2292457)Termination phase: Finite model building constraint generation
% 177.16/27.61 % (2292457)Time elapsed: 19.481 s
% 177.16/27.61 % (2292457)Peak memory usage: 1289 MB
% 177.16/27.61 % (2292457)Instructions burned: 54283 (million)
% 177.16/27.61 % (2292480)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1469676180:i=22565:add=on:rawr=on_2767 on theBenchmark for (2767ds/22565Mi)
% 177.16/27.61 % (2292470)Instruction limit reached!
% 177.16/27.61 % (2292470)------------------------------
% 177.16/27.61 % (2292470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292470)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292470)Termination reason: Instruction limit
% 177.16/27.61 % (2292470)Termination phase: Saturation
% 177.16/27.61 % (2292470)Time elapsed: 15.123 s
% 177.16/27.61 % (2292470)Peak memory usage: 440 MB
% 177.16/27.61 % (2292470)Instructions burned: 29341 (million)
% 177.16/27.61 % (2292482)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=513267589:i=8173:av=off_2754 on theBenchmark for (2754ds/8173Mi)
% 177.16/27.61 % (2292478)Instruction limit reached!
% 177.16/27.61 % (2292478)------------------------------
% 177.16/27.61 % (2292478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292478)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292478)Termination reason: Instruction limit
% 177.16/27.61 % (2292478)Termination phase: Finite model building constraint generation
% 177.16/27.61 % (2292478)Time elapsed: 2.751 s
% 177.16/27.61 % (2292478)Peak memory usage: 875 MB
% 177.16/27.61 % (2292478)Instructions burned: 14076 (million)
% 177.16/27.61 % (2292484)dis+10_16:1_sil=16000:random_seed=3078370607:i=9155:fsr=off_2750 on theBenchmark for (2750ds/9155Mi)
% 177.16/27.61 % TRYING [9]
% 177.16/27.61 % (2292484) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2292401-2292484"...
% 177.16/27.61 % (2292484)...printing done.
% 177.16/27.61 % (2292484)Refutation found. Thanks to Tanya!
% 177.16/27.61 % SZS status Theorem for theBenchmark
% 177.16/27.61 % SZS output start Proof for theBenchmark
% See solution above
% 177.16/27.61 % (2292484)------------------------------
% 177.16/27.61 % (2292484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 177.16/27.61 % (2292484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.16/27.61 % (2292484)CaDiCaL version: 2.1.3
% 177.16/27.61 % (2292484)Termination reason: Refutation
% 177.16/27.61 % (2292484)Time elapsed: 2.090 s
% 177.16/27.61 % (2292484)Peak memory usage: 60 MB
% 177.16/27.61 % (2292484)Instructions burned: 7759 (million)
% 177.16/27.61 % (2292401)Success in time 27.386 s
% 177.16/27.61 % Vampire exiting
%------------------------------------------------------------------------------