%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV621_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:26:08 PM UTC 2026
% Result : Theorem 18.13s 2.94s
% Output : Refutation 18.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 18
% Syntax : Number of formulae : 77 ( 40 unt; 0 typ; 0 def)
% Number of atoms : 134 ( 76 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 106 ( 49 ~; 43 |; 0 &)
% ( 2 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 5 ( 4 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 30 ( 28 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 4 con; 0-5 aty)
% Number of variables : 92 ( 92 !; 0 ?; 92 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
complex: $tType ).
tff(type_def_6,type,
bool: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(type_def_8,type,
real: $tType ).
tff(type_def_9,type,
fun: ( $tType * $tType ) > $tType ).
tff(func_def_0,type,
big_co1399186613setsum:
!>[X0: $tType,X1: $tType] : fun(fun(X0,X1),fun(fun(X0,bool),X1)) ).
tff(func_def_1,type,
combb:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,X1) * fun(X2,X0) ) > fun(X2,X1) ) ).
tff(func_def_2,type,
combc:
!>[X0: $tType,X1: $tType,X2: $tType] : ( fun(X0,fun(X1,X2)) > fun(X1,fun(X0,X2)) ) ).
tff(func_def_3,type,
combk:
!>[X0: $tType,X1: $tType] : ( X0 > fun(X1,X0) ) ).
tff(func_def_4,type,
combs:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,fun(X1,X2)) * fun(X0,X1) ) > fun(X0,X2) ) ).
tff(func_def_5,type,
fFT_Mirabelle_root: nat > complex ).
tff(func_def_6,type,
inverse_divide:
!>[X0: $tType] : fun(X0,fun(X0,X0)) ).
tff(func_def_7,type,
minus_minus:
!>[X0: $tType] : fun(X0,fun(X0,X0)) ).
tff(func_def_8,type,
one_one:
!>[X0: $tType] : X0 ).
tff(func_def_9,type,
times_times:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_10,type,
zero_zero:
!>[X0: $tType] : X0 ).
tff(func_def_11,type,
power_power:
!>[X0: $tType] : ( X0 > fun(nat,X0) ) ).
tff(func_def_12,type,
ord_atLeastLessThan:
!>[X0: $tType] : ( ( X0 * X0 ) > fun(X0,bool) ) ).
tff(func_def_13,type,
aa:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * X0 ) > X1 ) ).
tff(func_def_14,type,
fFalse: bool ).
tff(func_def_15,type,
fTrue: bool ).
tff(func_def_16,type,
k: nat ).
tff(func_def_17,type,
n: nat ).
tff(func_def_18,type,
sK0: ( fun(nat,bool) * nat ) > nat ).
tff(func_def_19,type,
sK1: ( fun(nat,bool) * nat ) > nat ).
tff(func_def_20,type,
sK2: ( fun(nat,bool) * nat ) > nat ).
tff(func_def_21,type,
sK3: ( fun(nat,bool) * nat ) > nat ).
tff(func_def_22,type,
sK4:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * fun(X0,bool) ) > X0 ) ).
tff(func_def_23,type,
sK5: ( real * nat ) > real ).
tff(func_def_24,type,
sK6: ( real * nat ) > real ).
tff(pred_def_1,type,
one:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
zero:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
power:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
field:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
mult_zero:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
group_add:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
semiring_0:
!>[X0: $tType] : $o ).
tff(pred_def_8,type,
monoid_mult:
!>[X0: $tType] : $o ).
tff(pred_def_9,type,
linorder:
!>[X0: $tType] : $o ).
tff(pred_def_10,type,
zero_neq_one:
!>[X0: $tType] : $o ).
tff(pred_def_11,type,
ab_group_add:
!>[X0: $tType] : $o ).
tff(pred_def_12,type,
division_ring:
!>[X0: $tType] : $o ).
tff(pred_def_13,type,
comm_semiring_1:
!>[X0: $tType] : $o ).
tff(pred_def_14,type,
linordered_idom:
!>[X0: $tType] : $o ).
tff(pred_def_15,type,
comm_monoid_add:
!>[X0: $tType] : $o ).
tff(pred_def_16,type,
no_zero_divisors:
!>[X0: $tType] : $o ).
tff(pred_def_17,type,
linordered_field:
!>[X0: $tType] : $o ).
tff(pred_def_18,type,
linordered_semidom:
!>[X0: $tType] : $o ).
tff(pred_def_19,type,
field_inverse_zero:
!>[X0: $tType] : $o ).
tff(pred_def_20,type,
ordered_ab_group_add:
!>[X0: $tType] : $o ).
tff(pred_def_21,type,
ring_n68954251visors:
!>[X0: $tType] : $o ).
tff(pred_def_22,type,
ring_11004092258visors:
!>[X0: $tType] : $o ).
tff(pred_def_23,type,
divisi14063676e_zero:
!>[X0: $tType] : $o ).
tff(pred_def_24,type,
linord1117847801e_zero:
!>[X0: $tType] : $o ).
tff(pred_def_25,type,
ord_less:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_26,type,
ord_less_eq:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_27,type,
member:
!>[X0: $tType] : ( ( X0 * fun(X0,bool) ) > $o ) ).
tff(pred_def_28,type,
pp: bool > $o ).
tff(f1,axiom,
ord_less(nat,zero_zero(nat),k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_assms_I1_J) ).
tff(f2,axiom,
ord_less(nat,k,n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_assms_I2_J) ).
tff(f4,axiom,
! [X0: $tType] :
( field(X0)
=> ! [X1: nat,X2: X0] :
( ( X2 != one_one(X0) )
=> ( aa(fun(nat,bool),X0,aa(fun(nat,X0),fun(fun(nat,bool),X0),big_co1399186613setsum(nat,X0),power_power(X0,X2)),ord_atLeastLessThan(nat,zero_zero(nat),X1)) = aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),aa(nat,X0,power_power(X0,X2),X1)),one_one(X0))),aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),X2),one_one(X0))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_geometric__sum) ).
tff(f11,axiom,
! [X0: $tType] :
( divisi14063676e_zero(X0)
=> ! [X1: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),X1),zero_zero(X0)) = zero_zero(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_divide__zero) ).
tff(f12,axiom,
! [X0: $tType] :
( group_add(X0)
=> ! [X1: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),X1),X1) = zero_zero(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_diff__self) ).
tff(f14,axiom,
! [X0: $tType] :
( field_inverse_zero(X0)
=> ! [X1: nat,X2: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),aa(nat,X0,power_power(X0,X2),X1)) = aa(nat,X0,power_power(X0,aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),X2)),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_power__one__over) ).
tff(f41,axiom,
! [X0: nat] : ( fFT_Mirabelle_root(X0) != zero_zero(complex) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_root__nonzero) ).
tff(f45,axiom,
! [X0: nat,X1: nat] :
( ord_less(nat,zero_zero(nat),X1)
=> ( ord_less(nat,X1,X0)
=> ( aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),X1))),ord_atLeastLessThan(nat,zero_zero(nat),X0)) = zero_zero(complex) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_root__summation) ).
tff(f50,axiom,
! [X0: $tType] :
( ring_11004092258visors(X0)
=> ! [X1: nat,X2: X0] :
( ( X2 != zero_zero(X0) )
=> ( aa(nat,X0,power_power(X0,X2),X1) != zero_zero(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_field__power__not__zero) ).
tff(f56,axiom,
! [X0: $tType] :
( division_ring(X0)
=> ! [X1: X0,X2: X0] :
( ( X2 != zero_zero(X0) )
=> ( ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),X1),X2) = one_one(X0) )
<=> ( X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_55_right__inverse__eq) ).
tff(f93,axiom,
! [X0: nat,X1: nat,X2: nat] :
( ord_less(nat,zero_zero(nat),X2)
=> ( aa(nat,complex,power_power(complex,fFT_Mirabelle_root(times_times(nat,X2,X1))),times_times(nat,X2,X0)) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X1)),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_root__cancel) ).
tff(f136,axiom,
divisi14063676e_zero(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex_Ocomplex___Fields_Odivision__ring__inverse__zero) ).
tff(f137,axiom,
ring_11004092258visors(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex_Ocomplex___Rings_Oring__1__no__zero__divisors) ).
tff(f139,axiom,
field_inverse_zero(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex_Ocomplex___Fields_Ofield__inverse__zero) ).
tff(f143,axiom,
division_ring(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex_Ocomplex___Fields_Odivision__ring) ).
tff(f148,axiom,
group_add(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex_Ocomplex___Groups_Ogroup__add) ).
tff(f150,axiom,
field(complex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Complex_Ocomplex___Fields_Ofield) ).
tff(f160,conjecture,
aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k))),ord_atLeastLessThan(nat,zero_zero(nat),n)) = aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),n)),one_one(complex))),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),one_one(complex))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f161,negated_conjecture,
( ( ~ aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k))),ord_atLeastLessThan(nat,zero_zero(nat),n)) ) = aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),n)),one_one(complex))),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),one_one(complex))) ),
inference(negated_conjecture,[status(cth)],[f160]) ).
tff(f162,plain,
aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k))),ord_atLeastLessThan(nat,zero_zero(nat),n)) != aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),n)),one_one(complex))),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),one_one(complex))),
inference(flattening,[],[f161]) ).
tff(f163,plain,
! [X0: $tType] :
( ! [X1: nat,X2: X0] :
( ( aa(fun(nat,bool),X0,aa(fun(nat,X0),fun(fun(nat,bool),X0),big_co1399186613setsum(nat,X0),power_power(X0,X2)),ord_atLeastLessThan(nat,zero_zero(nat),X1)) = aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),aa(nat,X0,power_power(X0,X2),X1)),one_one(X0))),aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),X2),one_one(X0))) )
| ( one_one(X0) = X2 ) )
| ~ field(X0) ),
inference(ennf_transformation,[],[f4]) ).
tff(f171,plain,
! [X0: $tType] :
( ! [X1: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),X1),zero_zero(X0)) = zero_zero(X0) )
| ~ divisi14063676e_zero(X0) ),
inference(ennf_transformation,[],[f11]) ).
tff(f172,plain,
! [X0: $tType] :
( ! [X1: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),X1),X1) = zero_zero(X0) )
| ~ group_add(X0) ),
inference(ennf_transformation,[],[f12]) ).
tff(f175,plain,
! [X0: $tType] :
( ! [X1: nat,X2: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),aa(nat,X0,power_power(X0,X2),X1)) = aa(nat,X0,power_power(X0,aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),X2)),X1) )
| ~ field_inverse_zero(X0) ),
inference(ennf_transformation,[],[f14]) ).
tff(f218,plain,
! [X0: nat,X1: nat] :
( ( aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),X1))),ord_atLeastLessThan(nat,zero_zero(nat),X0)) = zero_zero(complex) )
| ~ ord_less(nat,X1,X0)
| ~ ord_less(nat,zero_zero(nat),X1) ),
inference(ennf_transformation,[],[f45]) ).
tff(f219,plain,
! [X0: nat,X1: nat] :
( ( aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),X1))),ord_atLeastLessThan(nat,zero_zero(nat),X0)) = zero_zero(complex) )
| ~ ord_less(nat,X1,X0)
| ~ ord_less(nat,zero_zero(nat),X1) ),
inference(flattening,[],[f218]) ).
tff(f224,plain,
! [X0: $tType] :
( ! [X1: nat,X2: X0] :
( ( aa(nat,X0,power_power(X0,X2),X1) != zero_zero(X0) )
| ( zero_zero(X0) = X2 ) )
| ~ ring_11004092258visors(X0) ),
inference(ennf_transformation,[],[f50]) ).
tff(f230,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] :
( ( ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),X1),X2) = one_one(X0) )
<=> ( X1 = X2 ) )
| ( zero_zero(X0) = X2 ) )
| ~ division_ring(X0) ),
inference(ennf_transformation,[],[f56]) ).
tff(f261,plain,
! [X0: nat,X1: nat,X2: nat] :
( ( aa(nat,complex,power_power(complex,fFT_Mirabelle_root(times_times(nat,X2,X1))),times_times(nat,X2,X0)) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X1)),X0) )
| ~ ord_less(nat,zero_zero(nat),X2) ),
inference(ennf_transformation,[],[f93]) ).
tff(f265,plain,
ord_less(nat,zero_zero(nat),k),
inference(cnf_transformation,[],[f1]) ).
tff(f266,plain,
ord_less(nat,k,n),
inference(cnf_transformation,[],[f2]) ).
tff(f268,plain,
! [X0: $tType,X2: X0,X1: nat] :
( ~ field(X0)
| ( one_one(X0) = X2 )
| ( aa(fun(nat,bool),X0,aa(fun(nat,X0),fun(fun(nat,bool),X0),big_co1399186613setsum(nat,X0),power_power(X0,X2)),ord_atLeastLessThan(nat,zero_zero(nat),X1)) = aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),aa(nat,X0,power_power(X0,X2),X1)),one_one(X0))),aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),X2),one_one(X0))) ) ),
inference(cnf_transformation,[],[f163]) ).
tff(f278,plain,
! [X0: $tType,X1: X0] :
( ~ divisi14063676e_zero(X0)
| ( zero_zero(X0) = aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),X1),zero_zero(X0)) ) ),
inference(cnf_transformation,[],[f171]) ).
tff(f279,plain,
! [X0: $tType,X1: X0] :
( ~ group_add(X0)
| ( zero_zero(X0) = aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),X1),X1) ) ),
inference(cnf_transformation,[],[f172]) ).
tff(f282,plain,
! [X0: $tType,X2: X0,X1: nat] :
( ~ field_inverse_zero(X0)
| ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),aa(nat,X0,power_power(X0,X2),X1)) = aa(nat,X0,power_power(X0,aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),X2)),X1) ) ),
inference(cnf_transformation,[],[f175]) ).
tff(f333,plain,
! [X0: nat] : ( fFT_Mirabelle_root(X0) != zero_zero(complex) ),
inference(cnf_transformation,[],[f41]) ).
tff(f336,plain,
! [X0: nat,X1: nat] :
( ~ ord_less(nat,zero_zero(nat),X1)
| ~ ord_less(nat,X1,X0)
| ( zero_zero(complex) = aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),X1))),ord_atLeastLessThan(nat,zero_zero(nat),X0)) ) ),
inference(cnf_transformation,[],[f219]) ).
tff(f343,plain,
! [X0: $tType,X2: X0,X1: nat] :
( ~ ring_11004092258visors(X0)
| ( zero_zero(X0) = X2 )
| ( aa(nat,X0,power_power(X0,X2),X1) != zero_zero(X0) ) ),
inference(cnf_transformation,[],[f224]) ).
tff(f350,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( one_one(X0) != aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),X1),X2) )
| ( zero_zero(X0) = X2 )
| ( X1 = X2 )
| ~ division_ring(X0) ),
inference(cnf_transformation,[],[f230]) ).
tff(f403,plain,
! [X2: nat,X0: nat,X1: nat] :
( ~ ord_less(nat,zero_zero(nat),X2)
| ( aa(nat,complex,power_power(complex,fFT_Mirabelle_root(times_times(nat,X2,X1))),times_times(nat,X2,X0)) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X1)),X0) ) ),
inference(cnf_transformation,[],[f261]) ).
tff(f449,plain,
divisi14063676e_zero(complex),
inference(cnf_transformation,[],[f136]) ).
tff(f450,plain,
ring_11004092258visors(complex),
inference(cnf_transformation,[],[f137]) ).
tff(f452,plain,
field_inverse_zero(complex),
inference(cnf_transformation,[],[f139]) ).
tff(f456,plain,
division_ring(complex),
inference(cnf_transformation,[],[f143]) ).
tff(f461,plain,
group_add(complex),
inference(cnf_transformation,[],[f148]) ).
tff(f463,plain,
field(complex),
inference(cnf_transformation,[],[f150]) ).
tff(f473,plain,
aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k))),ord_atLeastLessThan(nat,zero_zero(nat),n)) != aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),n)),one_one(complex))),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k)),one_one(complex))),
inference(cnf_transformation,[],[f162]) ).
tff(f505,plain,
! [X0: $tType,X1: X0] :
( divisi14063676e_zero(X0)
| ( zero_zero(X0) = aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),X1),zero_zero(X0)) ) ),
inference(consistent_polarity_flipping,[],[f278]) ).
tff(f506,plain,
! [X0: $tType,X1: X0] :
( group_add(X0)
| ( zero_zero(X0) = aa(X0,X0,aa(X0,fun(X0,X0),minus_minus(X0),X1),X1) ) ),
inference(consistent_polarity_flipping,[],[f279]) ).
tff(f509,plain,
! [X0: $tType,X2: X0,X1: nat] :
( field_inverse_zero(X0)
| ( aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),aa(nat,X0,power_power(X0,X2),X1)) = aa(nat,X0,power_power(X0,aa(X0,X0,aa(X0,fun(X0,X0),inverse_divide(X0),one_one(X0)),X2)),X1) ) ),
inference(consistent_polarity_flipping,[],[f282]) ).
tff(f562,plain,
! [X0: $tType,X2: X0,X1: nat] :
( ring_11004092258visors(X0)
| ( zero_zero(X0) = X2 )
| ( aa(nat,X0,power_power(X0,X2),X1) != zero_zero(X0) ) ),
inference(consistent_polarity_flipping,[],[f343]) ).
tff(f591,plain,
~ divisi14063676e_zero(complex),
inference(consistent_polarity_flipping,[],[f449]) ).
tff(f592,plain,
~ ring_11004092258visors(complex),
inference(consistent_polarity_flipping,[],[f450]) ).
tff(f593,plain,
~ field_inverse_zero(complex),
inference(consistent_polarity_flipping,[],[f452]) ).
tff(f595,plain,
~ group_add(complex),
inference(consistent_polarity_flipping,[],[f461]) ).
tff(f633,plain,
! [X0: complex,X1: nat] :
( ( zero_zero(complex) != aa(nat,complex,power_power(complex,X0),X1) )
| ( zero_zero(complex) = X0 ) ),
inference(resolution,[],[f562,f592]) ).
tff(f643,plain,
! [X0: complex] : ( zero_zero(complex) = aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),X0),X0) ),
inference(resolution,[],[f506,f595]) ).
tff(f653,plain,
! [X0: complex] : ( zero_zero(complex) = aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),X0),zero_zero(complex)) ),
inference(resolution,[],[f505,f591]) ).
tff(f1022,plain,
! [X0: nat,X1: nat] : ( aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),X1) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(times_times(nat,k,X0))),times_times(nat,k,X1)) ),
inference(resolution,[],[f403,f265]) ).
tff(f1605,plain,
! [X0: complex,X1: nat] : ( aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),aa(nat,complex,power_power(complex,X0),X1)) = aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),X0)),X1) ),
inference(resolution,[],[f509,f593]) ).
tff(f1662,plain,
! [X0: nat] :
( ~ ord_less(nat,k,X0)
| ( zero_zero(complex) = aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),k))),ord_atLeastLessThan(nat,zero_zero(nat),X0)) ) ),
inference(resolution,[],[f336,f265]) ).
tff(f1854,plain,
! [X0: complex,X1: nat] :
( ( aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,X0)),ord_atLeastLessThan(nat,zero_zero(nat),X1)) = aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,X0),X1)),one_one(complex))),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),X0),one_one(complex))) )
| ( one_one(complex) = X0 ) ),
inference(resolution,[],[f268,f463]) ).
tff(f2874,plain,
! [X0: nat,X1: nat] :
( ( zero_zero(complex) != aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),X1) )
| ( zero_zero(complex) = fFT_Mirabelle_root(times_times(nat,k,X0)) ) ),
inference(superposition,[],[f633,f1022]) ).
tff(f2881,plain,
! [X0: nat,X1: nat] : ( zero_zero(complex) != aa(nat,complex,power_power(complex,fFT_Mirabelle_root(X0)),X1) ),
inference(forward_subsumption_resolution,[],[f2874,f333]) ).
tff(f17698,plain,
( ( aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k))),ord_atLeastLessThan(nat,zero_zero(nat),n)) != aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k))),ord_atLeastLessThan(nat,zero_zero(nat),n)) )
| ( one_one(complex) = aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k) ) ),
inference(superposition,[],[f473,f1854]) ).
tff(f17763,plain,
one_one(complex) = aa(nat,complex,power_power(complex,aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),fFT_Mirabelle_root(n))),k),
inference(trivial_inequality_removal,[],[f17698]) ).
tff(f17791,plain,
one_one(complex) = aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),one_one(complex)),aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k)),
inference(superposition,[],[f17763,f1605]) ).
tff(f17793,plain,
aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,one_one(complex))),ord_atLeastLessThan(nat,zero_zero(nat),n)) != aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,one_one(complex)),n)),one_one(complex))),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),one_one(complex)),one_one(complex))),
inference(superposition,[],[f473,f17763]) ).
tff(f17823,plain,
aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,one_one(complex))),ord_atLeastLessThan(nat,zero_zero(nat),n)) != aa(complex,complex,aa(complex,fun(complex,complex),inverse_divide(complex),aa(complex,complex,aa(complex,fun(complex,complex),minus_minus(complex),aa(nat,complex,power_power(complex,one_one(complex)),n)),one_one(complex))),zero_zero(complex)),
inference(forward_demodulation,[],[f17793,f643]) ).
tff(f17829,plain,
zero_zero(complex) != aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,one_one(complex))),ord_atLeastLessThan(nat,zero_zero(nat),n)),
inference(forward_demodulation,[],[f17823,f653]) ).
tff(f23756,plain,
( ( one_one(complex) != one_one(complex) )
| ( zero_zero(complex) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k) )
| ( one_one(complex) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k) )
| ~ division_ring(complex) ),
inference(superposition,[],[f350,f17791]) ).
tff(f23819,plain,
( ( zero_zero(complex) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k) )
| ( one_one(complex) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k) )
| ~ division_ring(complex) ),
inference(trivial_inequality_removal,[],[f23756]) ).
tff(f23824,plain,
( ( one_one(complex) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k) )
| ~ division_ring(complex) ),
inference(forward_subsumption_resolution,[],[f23819,f2881]) ).
tff(f23830,plain,
one_one(complex) = aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k),
inference(forward_subsumption_resolution,[],[f23824,f456]) ).
tff(f47875,plain,
zero_zero(complex) = aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,aa(nat,complex,power_power(complex,fFT_Mirabelle_root(n)),k))),ord_atLeastLessThan(nat,zero_zero(nat),n)),
inference(resolution,[],[f266,f1662]) ).
tff(f47897,plain,
zero_zero(complex) = aa(fun(nat,bool),complex,aa(fun(nat,complex),fun(fun(nat,bool),complex),big_co1399186613setsum(nat,complex),power_power(complex,one_one(complex))),ord_atLeastLessThan(nat,zero_zero(nat),n)),
inference(forward_demodulation,[],[f47875,f23830]) ).
tff(f47899,plain,
$false,
inference(forward_subsumption_resolution,[],[f47897,f17829]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV621_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n014.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 12:03:46 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.54/1.51 % (1737533)Will run a generic schedule for satisfiability detection.
% 8.54/1.51 % (1737538)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=155023757_2999 on theBenchmark for (2999ds/0Mi)
% 8.54/1.51 % (1737539)% WARNING: option uhcvi not known.
% 8.54/1.51 % Exception at run slice level
% 8.54/1.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.54/1.51 % (1737539)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3192147490:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.54/1.51 % (1737540)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=491353688:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.54/1.51 % (1737541)dis+10_1_sil=32000:sp=arity:random_seed=254202362:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.54/1.51 % (1737542)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2013863435:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.54/1.51 % (1737544)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1157346282:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.54/1.51 % (1737543)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1601875371:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.54/1.51 % (1737546)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2524781197:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.54/1.51 % Exception at run slice level
% 8.54/1.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 8.54/1.51 % (1737554)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1778323949:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.54/1.51 % (1737554)Instruction limit reached!
% 8.54/1.51 % (1737554)------------------------------
% 8.54/1.51 % (1737554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.51 % (1737554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.51 % (1737554)CaDiCaL version: 2.1.3
% 8.54/1.51 % (1737554)Termination reason: Instruction limit
% 8.54/1.51 % (1737554)Termination phase: Saturation
% 8.54/1.51 % (1737554)Time elapsed: 0.044 s
% 8.54/1.51 % (1737554)Peak memory usage: 13 MB
% 8.54/1.51 % (1737554)Instructions burned: 133 (million)
% 8.54/1.51 % (1737541)Instruction limit reached!
% 8.54/1.51 % (1737541)------------------------------
% 8.54/1.51 % (1737541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.51 % (1737541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.51 % (1737541)CaDiCaL version: 2.1.3
% 8.54/1.51 % (1737541)Termination reason: Instruction limit
% 8.54/1.51 % (1737541)Termination phase: Saturation
% 8.54/1.51 % (1737541)Time elapsed: 0.066 s
% 8.54/1.51 % (1737541)Peak memory usage: 12 MB
% 8.54/1.51 % (1737541)Instructions burned: 104 (million)
% 8.54/1.51 % (1737542)Instruction limit reached!
% 8.54/1.51 % (1737542)------------------------------
% 8.54/1.51 % (1737542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.51 % (1737542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.51 % (1737542)CaDiCaL version: 2.1.3
% 8.54/1.51 % (1737542)Termination reason: Instruction limit
% 8.54/1.51 % (1737542)Termination phase: Saturation
% 8.54/1.51 % (1737542)Time elapsed: 0.072 s
% 8.54/1.51 % (1737542)Peak memory usage: 13 MB
% 8.54/1.51 % (1737542)Instructions burned: 119 (million)
% 8.54/1.51 % (1737556)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=4257190230:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 8.54/1.51 % (1737543)Instruction limit reached!
% 8.54/1.51 % (1737543)------------------------------
% 8.54/1.51 % (1737543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.51 % (1737543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.51 % (1737543)CaDiCaL version: 2.1.3
% 8.54/1.51 % (1737543)Termination reason: Instruction limit
% 8.54/1.51 % (1737543)Termination phase: Saturation
% 8.54/1.51 % (1737543)Time elapsed: 0.082 s
% 8.54/1.51 % (1737543)Peak memory usage: 13 MB
% 8.54/1.51 % (1737543)Instructions burned: 131 (million)
% 8.54/1.51 % (1737557)ott-21_1_sil=16000:fs=off:random_seed=1129861503:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.54/1.51 % (1737558)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3326408038:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 18.13/2.94 % (1737560)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2385449353:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 18.13/2.94 % (1737544)Instruction limit reached!
% 18.13/2.94 % (1737544)------------------------------
% 18.13/2.94 % (1737544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737544)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737544)Termination reason: Instruction limit
% 18.13/2.94 % (1737544)Termination phase: Saturation
% 18.13/2.94 % (1737544)Time elapsed: 0.105 s
% 18.13/2.94 % (1737544)Peak memory usage: 14 MB
% 18.13/2.94 % (1737544)Instructions burned: 159 (million)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737564)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3865079039:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 18.13/2.94 % (1737565)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2561885489:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737568)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=1315926953:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 18.13/2.94 % (1737557)Instruction limit reached!
% 18.13/2.94 % (1737557)------------------------------
% 18.13/2.94 % (1737557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737557)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737557)Termination reason: Instruction limit
% 18.13/2.94 % (1737557)Termination phase: Saturation
% 18.13/2.94 % (1737557)Time elapsed: 0.095 s
% 18.13/2.94 % (1737557)Peak memory usage: 12 MB
% 18.13/2.94 % (1737557)Instructions burned: 181 (million)
% 18.13/2.94 % (1737570)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3827320859:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 18.13/2.94 % (1737556)Instruction limit reached!
% 18.13/2.94 % (1737556)------------------------------
% 18.13/2.94 % (1737556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737556)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737556)Termination reason: Instruction limit
% 18.13/2.94 % (1737556)Termination phase: Saturation
% 18.13/2.94 % (1737556)Time elapsed: 0.209 s
% 18.13/2.94 % (1737556)Peak memory usage: 16 MB
% 18.13/2.94 % (1737556)Instructions burned: 687 (million)
% 18.13/2.94 % (1737572)fmb+10_1_sil=64000:random_seed=668883471:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 18.13/2.94 % (1737572)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737574)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2847967223:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737576)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2766939294:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737578)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3192611628:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 18.13/2.94 % (1737558)Instruction limit reached!
% 18.13/2.94 % (1737558)------------------------------
% 18.13/2.94 % (1737558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737558)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737558)Termination reason: Instruction limit
% 18.13/2.94 % (1737558)Termination phase: Saturation
% 18.13/2.94 % (1737558)Time elapsed: 0.323 s
% 18.13/2.94 % (1737558)Peak memory usage: 14 MB
% 18.13/2.94 % (1737558)Instructions burned: 478 (million)
% 18.13/2.94 % (1737580)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2991872643:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 18.13/2.94 % (1737580)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 18.13/2.94 % (1737568)Instruction limit reached!
% 18.13/2.94 % (1737568)------------------------------
% 18.13/2.94 % (1737568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737568)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737568)Termination reason: Instruction limit
% 18.13/2.94 % (1737568)Termination phase: Saturation
% 18.13/2.94 % (1737568)Time elapsed: 0.382 s
% 18.13/2.94 % (1737568)Peak memory usage: 18 MB
% 18.13/2.94 % (1737568)Instructions burned: 693 (million)
% 18.13/2.94 % (1737582)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1463963130:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737584)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=297111074:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737586)ott-2_1_sil=16000:newcnf=on:random_seed=2143989204:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 18.13/2.94 % (1737570)Instruction limit reached!
% 18.13/2.94 % (1737570)------------------------------
% 18.13/2.94 % (1737570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737570)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737570)Termination reason: Instruction limit
% 18.13/2.94 % (1737570)Termination phase: Saturation
% 18.13/2.94 % (1737570)Time elapsed: 0.523 s
% 18.13/2.94 % (1737570)Peak memory usage: 19 MB
% 18.13/2.94 % (1737570)Instructions burned: 879 (million)
% 18.13/2.94 % (1737588)ott+10_1_sil=32000:tgt=ground:random_seed=2710857141:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 18.13/2.94 % (1737564)Instruction limit reached!
% 18.13/2.94 % (1737564)------------------------------
% 18.13/2.94 % (1737564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737564)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737564)Termination reason: Instruction limit
% 18.13/2.94 % (1737564)Termination phase: Saturation
% 18.13/2.94 % (1737564)Time elapsed: 0.731 s
% 18.13/2.94 % (1737564)Peak memory usage: 23 MB
% 18.13/2.94 % (1737564)Instructions burned: 1180 (million)
% 18.13/2.94 % (1737590)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3864452459:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737592)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=654892630:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 18.13/2.94 % (1737586)Instruction limit reached!
% 18.13/2.94 % (1737586)------------------------------
% 18.13/2.94 % (1737586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737586)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737586)Termination reason: Instruction limit
% 18.13/2.94 % (1737586)Termination phase: Saturation
% 18.13/2.94 % (1737586)Time elapsed: 0.481 s
% 18.13/2.94 % (1737586)Peak memory usage: 17 MB
% 18.13/2.94 % (1737586)Instructions burned: 870 (million)
% 18.13/2.94 % (1737594)dis+21_1_sil=32000:sas=cadical:random_seed=805146733:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 18.13/2.94 % (1737580)Instruction limit reached!
% 18.13/2.94 % (1737580)------------------------------
% 18.13/2.94 % (1737580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737580)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737580)Termination reason: Instruction limit
% 18.13/2.94 % (1737580)Termination phase: Saturation
% 18.13/2.94 % (1737580)Time elapsed: 0.817 s
% 18.13/2.94 % (1737580)Peak memory usage: 28 MB
% 18.13/2.94 % (1737580)Instructions burned: 1473 (million)
% 18.13/2.94 % (1737596)ott+11_1_sil=16000:gs=on:random_seed=628381149:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 18.13/2.94 % (1737578)Instruction limit reached!
% 18.13/2.94 % (1737578)------------------------------
% 18.13/2.94 % (1737578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737578)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737578)Termination reason: Instruction limit
% 18.13/2.94 % (1737578)Termination phase: Saturation
% 18.13/2.94 % (1737578)Time elapsed: 1.515 s
% 18.13/2.94 % (1737578)Peak memory usage: 37 MB
% 18.13/2.94 % (1737578)Instructions burned: 5132 (million)
% 18.13/2.94 % (1737598)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3333752063:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 18.13/2.94 % Exception at run slice level
% 18.13/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 18.13/2.94 % (1737600)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2998442213:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi)
% 18.13/2.94 % (1737596)Instruction limit reached!
% 18.13/2.94 % (1737596)------------------------------
% 18.13/2.94 % (1737596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737596)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737596)Termination reason: Instruction limit
% 18.13/2.94 % (1737596)Termination phase: Saturation
% 18.13/2.94 % (1737596)Time elapsed: 1.273 s
% 18.13/2.94 % (1737596)Peak memory usage: 26 MB
% 18.13/2.94 % (1737596)Instructions burned: 2251 (million)
% 18.13/2.94 % (1737602)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1575315002:i=29340_2974 on theBenchmark for (2974ds/29340Mi)
% 18.13/2.94 % (1737539) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1737533-1737539"...
% 18.13/2.94 % (1737539)...printing done.
% 18.13/2.94 % (1737539)Refutation found. Thanks to Tanya!
% 18.13/2.94 % SZS status Theorem for theBenchmark
% 18.13/2.94 % SZS output start Proof for theBenchmark
% See solution above
% 18.13/2.94 % (1737539)------------------------------
% 18.13/2.94 % (1737539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.13/2.94 % (1737539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.13/2.94 % (1737539)CaDiCaL version: 2.1.3
% 18.13/2.94 % (1737539)Termination reason: Refutation
% 18.13/2.94 % (1737539)Time elapsed: 2.662 s
% 18.13/2.94 % (1737539)Peak memory usage: 37 MB
% 18.13/2.94 % (1737539)Instructions burned: 4684 (million)
% 18.13/2.94 % (1737533)Success in time 2.712 s
% 18.13/2.94 % Vampire exiting
%------------------------------------------------------------------------------