%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP106^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 : Wed Sep 30 08:08:22 AM UTC 2026
% Result : Theorem 0.87s 0.54s
% Output : Refutation 0.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 42 ( 23 unt; 0 typ; 3 def)
% Number of atoms : 144 ( 34 equ; 0 cnn)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 722 ( 32 ~; 25 |; 0 &; 656 @)
% ( 3 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 11 ( 10 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 109 ( 106 usr; 15 con; 0-4 aty)
% Number of variables : 28 ( 0 sgn 28 !; 0 ?; 28 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
partia1993116613t_unit: $tType ).
thf(type_def_6,type,
partia1833973666xt_a_b: $tType ).
thf(type_def_7,type,
partia96731725t_unit: $tType ).
thf(type_def_8,type,
set_Product_prod_a_a: $tType ).
thf(type_def_9,type,
product_prod_a_a: $tType ).
thf(type_def_10,type,
set_a: $tType ).
thf(type_def_11,type,
nat: $tType ).
thf(type_def_12,type,
int: $tType ).
thf(type_def_13,type,
b: $tType ).
thf(type_def_14,type,
a: $tType ).
thf(type_def_15,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
partia206007992t_unit: partia1993116613t_unit > set_Product_prod_a_a ).
thf(func_def_1,type,
partia1955795460t_unit: partia96731725t_unit > set_a ).
thf(func_def_2,type,
partia1066395285xt_a_b: partia1833973666xt_a_b > set_a ).
thf(func_def_3,type,
units_a_Product_unit: partia96731725t_unit > set_a ).
thf(func_def_4,type,
units_a_ring_ext_a_b: partia1833973666xt_a_b > set_a ).
thf(func_def_5,type,
comm_g1684316527t_unit: partia96731725t_unit > $o ).
thf(func_def_6,type,
comm_g791708116xt_a_b: partia1833973666xt_a_b > $o ).
thf(func_def_7,type,
group_a_Product_unit: partia96731725t_unit > $o ).
thf(func_def_8,type,
group_a_ring_ext_a_b: partia1833973666xt_a_b > $o ).
thf(func_def_9,type,
mult_a_Product_unit: partia96731725t_unit > a > a > a ).
thf(func_def_10,type,
mult_a_ring_ext_a_b: partia1833973666xt_a_b > a > a > a ).
thf(func_def_11,type,
one_a_Product_unit: partia96731725t_unit > a ).
thf(func_def_12,type,
one_a_ring_ext_a_b: partia1833973666xt_a_b > a ).
thf(func_def_13,type,
units_873712258t_unit: partia96731725t_unit > partia96731725t_unit ).
thf(func_def_14,type,
units_1411277569xt_a_b: partia1833973666xt_a_b > partia96731725t_unit ).
thf(func_def_15,type,
minus_minus_int: int > int > int ).
thf(func_def_16,type,
minus_minus_nat: nat > nat > nat ).
thf(func_def_17,type,
plus_plus_int: int > int > int ).
thf(func_def_18,type,
plus_plus_nat: nat > nat > nat ).
thf(func_def_19,type,
uminus_uminus_int: int > int ).
thf(func_def_20,type,
suc: nat > nat ).
thf(func_def_21,type,
semiri2019852685at_int: nat > int ).
thf(func_def_22,type,
semiri1382578993at_nat: nat > nat ).
thf(func_def_23,type,
product_Pair_a_a: a > a > product_prod_a_a ).
thf(func_def_24,type,
a_inv_a_b: partia1833973666xt_a_b > a > a ).
thf(func_def_25,type,
a_minus_a_b: partia1833973666xt_a_b > a > a > a ).
thf(func_def_26,type,
abelian_group_a_b: partia1833973666xt_a_b > $o ).
thf(func_def_27,type,
add_pow_a_b_int: partia1833973666xt_a_b > int > a > a ).
thf(func_def_28,type,
add_pow_a_b_nat: partia1833973666xt_a_b > nat > a > a ).
thf(func_def_29,type,
field_a_b: partia1833973666xt_a_b > $o ).
thf(func_def_30,type,
add_a_b: partia1833973666xt_a_b > a > a > a ).
thf(func_def_31,type,
more_a_b: partia1833973666xt_a_b > b ).
thf(func_def_32,type,
zero_a_b: partia1833973666xt_a_b > a ).
thf(func_def_33,type,
semiring_a_b: partia1833973666xt_a_b > $o ).
thf(func_def_34,type,
collec645855634od_a_a: ( product_prod_a_a > $o ) > set_Product_prod_a_a ).
thf(func_def_35,type,
collect_a: ( a > $o ) > set_a ).
thf(func_def_36,type,
member449909584od_a_a: product_prod_a_a > set_Product_prod_a_a > $o ).
thf(func_def_37,type,
member_a: a > set_a > $o ).
thf(func_def_38,type,
r: partia1833973666xt_a_b ).
thf(func_def_39,type,
r2: a ).
thf(func_def_40,type,
r3: a ).
thf(func_def_41,type,
r4: a ).
thf(func_def_42,type,
rel: partia1993116613t_unit ).
thf(func_def_43,type,
s: a ).
thf(func_def_44,type,
s2: a ).
thf(func_def_45,type,
s3: a ).
thf(func_def_49,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_50,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_51,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_52,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_53,type,
sP0: partia1833973666xt_a_b > $o ).
thf(func_def_54,type,
sP1: partia1833973666xt_a_b > $o ).
thf(func_def_55,type,
sP2: partia1833973666xt_a_b > $o ).
thf(func_def_56,type,
sP3: partia96731725t_unit > $o ).
thf(func_def_57,type,
sK4: a > a ).
thf(func_def_58,type,
sK5: partia1833973666xt_a_b > a > a ).
thf(func_def_59,type,
sK6: partia1833973666xt_a_b > a ).
thf(func_def_60,type,
sK7: partia1833973666xt_a_b > a ).
thf(func_def_61,type,
sK8: partia1833973666xt_a_b > a ).
thf(func_def_62,type,
sK9: partia1833973666xt_a_b > a ).
thf(func_def_63,type,
sK10: partia1833973666xt_a_b > a ).
thf(func_def_64,type,
sK11: partia1833973666xt_a_b > a ).
thf(func_def_65,type,
sK12: partia1833973666xt_a_b > a ).
thf(func_def_66,type,
sK13: ( product_prod_a_a > $o ) > ( product_prod_a_a > $o ) > product_prod_a_a ).
thf(func_def_67,type,
sK14: partia1833973666xt_a_b > a > a ).
thf(func_def_68,type,
sK15: partia1833973666xt_a_b > a ).
thf(func_def_69,type,
sK16: partia1833973666xt_a_b > a ).
thf(func_def_70,type,
sK17: partia1833973666xt_a_b > a ).
thf(func_def_71,type,
sK18: partia1833973666xt_a_b > a ).
thf(func_def_72,type,
sK19: partia1833973666xt_a_b > a ).
thf(func_def_73,type,
sK20: partia1833973666xt_a_b > a ).
thf(func_def_74,type,
sK21: partia1833973666xt_a_b > a ).
thf(func_def_75,type,
sK22: partia1833973666xt_a_b > a ).
thf(func_def_76,type,
sK23: partia1833973666xt_a_b > a ).
thf(func_def_77,type,
sK24: a > partia96731725t_unit > a ).
thf(func_def_78,type,
sK25: ( product_prod_a_a > $o ) > a ).
thf(func_def_79,type,
sK26: ( product_prod_a_a > $o ) > a ).
thf(func_def_80,type,
sK27: a > a ).
thf(func_def_81,type,
sK28: product_prod_a_a > a ).
thf(func_def_82,type,
sK29: product_prod_a_a > a ).
thf(func_def_83,type,
sK30: partia96731725t_unit > a ).
thf(func_def_84,type,
sK31: partia96731725t_unit > a ).
thf(func_def_85,type,
sK32: partia96731725t_unit > a ).
thf(func_def_86,type,
sK33: partia96731725t_unit > a ).
thf(func_def_87,type,
sK34: partia96731725t_unit > a ).
thf(func_def_88,type,
sK35: partia96731725t_unit > a ).
thf(func_def_89,type,
sK36: partia96731725t_unit > a ).
thf(func_def_90,type,
sK37: product_prod_a_a > a ).
thf(func_def_91,type,
sK38: product_prod_a_a > a ).
thf(func_def_92,type,
sK39: a > a ).
thf(func_def_93,type,
sK40: a ).
thf(func_def_94,type,
sK41: ( nat > $o ) > nat ).
thf(func_def_95,type,
sK42: partia96731725t_unit > a > a ).
thf(func_def_96,type,
sK43: ( a > $o ) > ( a > $o ) > a ).
thf(func_def_97,type,
sK44: ( product_prod_a_a > $o ) > a ).
thf(func_def_98,type,
sK45: ( product_prod_a_a > $o ) > a ).
thf(func_def_99,type,
sK46: a > a ).
thf(func_def_100,type,
sK47: a > a ).
thf(func_def_101,type,
sK48: a ).
thf(func_def_102,type,
sK49: a > partia1833973666xt_a_b > a ).
thf(func_def_103,type,
sK50: a > a ).
thf(func_def_104,type,
vNOT: $o > $o ).
thf(f5,axiom,
! [X3: a,X2: a,X1: a,X0: a] :
( ( member449909584od_a_a @ ( product_Pair_a_a @ X0 @ X1 ) @ ( partia206007992t_unit @ rel ) )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ X2 @ X3 ) @ ( partia206007992t_unit @ rel ) )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ X3 @ X0 ) @ ( mult_a_ring_ext_a_b @ r @ X1 @ X2 ) ) @ ( mult_a_ring_ext_a_b @ r @ X1 @ X3 ) ) @ ( partia206007992t_unit @ rel ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_closed__rel__add) ).
thf(f11,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_f5) ).
thf(f12,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_f4) ).
thf(f283,conjecture,
member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(f284,negated_conjecture,
~ ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) ),
inference(negated_conjecture,[status(cth)],[f283]) ).
thf(f343,plain,
member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ),
inference(rectify,[],[f11]) ).
thf(f344,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(fool_elimination,[],[f343]) ).
thf(f472,plain,
member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ),
inference(rectify,[],[f12]) ).
thf(f473,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(fool_elimination,[],[f472]) ).
thf(f553,plain,
! [X0: a,X1: a,X2: a,X3: a] :
( ( member449909584od_a_a @ ( product_Pair_a_a @ X3 @ X2 ) @ ( partia206007992t_unit @ rel ) )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ X1 @ X0 ) @ ( partia206007992t_unit @ rel ) )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ X0 @ X3 ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X1 ) ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X0 ) ) @ ( partia206007992t_unit @ rel ) ) ) ),
inference(rectify,[],[f5]) ).
thf(f554,plain,
! [X2: a,X3: a,X1: a,X0: a] :
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ X3 @ X2 ) @ ( partia206007992t_unit @ rel ) )
= $true )
=> ( ( ( member449909584od_a_a @ ( product_Pair_a_a @ X1 @ X0 ) @ ( partia206007992t_unit @ rel ) )
= $true )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ X0 @ X3 ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X1 ) ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X0 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ) ) ),
inference(fool_elimination,[],[f553]) ).
thf(f576,plain,
~ ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) ),
inference(rectify,[],[f284]) ).
thf(f577,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
!= $true ),
inference(fool_elimination,[],[f576]) ).
thf(f702,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
!= $true ),
inference(flattening,[],[f577]) ).
thf(f731,plain,
! [X2: a,X3: a,X1: a,X0: a] :
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ X0 @ X3 ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X1 ) ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X0 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ X1 @ X0 ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ X3 @ X2 ) @ ( partia206007992t_unit @ rel ) )
!= $true ) ),
inference(ennf_transformation,[],[f554]) ).
thf(f732,plain,
! [X2: a,X1: a,X0: a,X3: a] :
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ X1 @ X0 ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ X0 @ X3 ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X1 ) ) @ ( mult_a_ring_ext_a_b @ r @ X2 @ X0 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ X3 @ X2 ) @ ( partia206007992t_unit @ rel ) )
!= $true ) ),
inference(flattening,[],[f731]) ).
thf(f1233,plain,
! [X0: a,X1: a,X2: a,X3: a] :
( ( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ X1 @ X2 ) @ ( partia206007992t_unit @ rel ) ) )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ X2 @ X3 ) @ ( mult_a_ring_ext_a_b @ r @ X0 @ X1 ) ) @ ( mult_a_ring_ext_a_b @ r @ X0 @ X2 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ X3 @ X0 ) @ ( partia206007992t_unit @ rel ) )
!= $true ) ),
inference(rectify,[],[f732]) ).
thf(f1326,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(cnf_transformation,[],[f473]) ).
thf(f1329,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ),
inference(cnf_transformation,[],[f344]) ).
thf(f1372,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
!= $true ),
inference(cnf_transformation,[],[f702]) ).
thf(f1612,plain,
! [X2: a,X3: a,X0: a,X1: a] :
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ X2 @ X3 ) @ ( mult_a_ring_ext_a_b @ r @ X0 @ X1 ) ) @ ( mult_a_ring_ext_a_b @ r @ X0 @ X2 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ X1 @ X2 ) @ ( partia206007992t_unit @ rel ) ) )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ X3 @ X0 ) @ ( partia206007992t_unit @ rel ) )
!= $true ) ),
inference(cnf_transformation,[],[f1233]) ).
thf(f1767,definition,
( spl51_14
<=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl51_14])],[avatar_definition]) ).
thf(f1769,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ~ spl51_14 ),
inference(avatar_component_clause,[],[f1767]) ).
thf(f1770,plain,
spl51_14,
inference(avatar_split_clause,[],[f1326,f1767]) ).
thf(f1846,definition,
( spl51_31
<=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl51_31])],[avatar_definition]) ).
thf(f1848,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( add_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) ) ) @ ( mult_a_ring_ext_a_b @ r @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| spl51_31 ),
inference(avatar_component_clause,[],[f1846]) ).
thf(f1849,plain,
~ spl51_31,
inference(avatar_split_clause,[],[f1372,f1846]) ).
thf(f1862,definition,
( spl51_34
<=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl51_34])],[avatar_definition]) ).
thf(f1864,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
= $true )
| ~ spl51_34 ),
inference(avatar_component_clause,[],[f1862]) ).
thf(f1865,plain,
spl51_34,
inference(avatar_split_clause,[],[f1329,f1862]) ).
thf(f2758,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| ( $true != $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| spl51_31 ),
inference(superposition,[],[f1848,f1612]) ).
thf(f2759,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r3 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s2 @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| spl51_31 ),
inference(trivial_inequality_removal,[],[f2758]) ).
thf(f2760,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( mult_a_ring_ext_a_b @ r @ r2 @ r4 ) @ ( mult_a_ring_ext_a_b @ r @ s @ s3 ) ) @ ( partia206007992t_unit @ rel ) )
!= $true )
| spl51_31
| ~ spl51_34 ),
inference(forward_subsumption_resolution,[],[f2759,f1864]) ).
thf(f2761,plain,
( $false
| ~ spl51_14
| spl51_31
| ~ spl51_34 ),
inference(forward_subsumption_resolution,[],[f2760,f1769]) ).
thf(f2762,plain,
( ~ spl51_14
| spl51_31
| ~ spl51_34 ),
inference(avatar_contradiction_clause,[],[f2761]) ).
cnf(s14,plain,
spl51_14,
inference(sat_conversion,[],[f1770]) ).
cnf(s29,plain,
~ spl51_31,
inference(sat_conversion,[],[f1849]) ).
cnf(s33,plain,
spl51_34,
inference(sat_conversion,[],[f1865]) ).
cnf(s116,plain,
( ~ spl51_14
| spl51_31
| ~ spl51_34 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s117,plain,
~ spl51_14,
inference(rat,[],[s116,s33,s29]) ).
cnf(s118,plain,
$false,
inference(rat,[],[s14,s117]) ).
thf(f2763,plain,
$false,
inference(avatar_sat_refutation,[],[s118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP106^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.18 % Computer : n011.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Tue Sep 29 19:55:01 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running higher-order theorem proving
% 0.22/0.33 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.87/0.50 % (563005)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.87/0.50 % (563016)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=609832401:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.87/0.50 % (563012)lrs+10_16_si=on:nwc=1.5:random_seed=2356850658:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.87/0.50 % (563013)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=364824924:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.87/0.50 % (563015)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=90366019:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.87/0.50 % (563017)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.87/0.50 % (563017)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.87/0.50 % (563011)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=423280227:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.87/0.50 % (563014)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=3906572124:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.87/0.50 % (563013)Instruction limit reached!
% 0.87/0.50 % (563013)------------------------------
% 0.87/0.50 % (563013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.50 % (563013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.50 % (563013)CaDiCaL version: 2.1.3
% 0.87/0.50 % (563013)Termination reason: Instruction limit
% 0.87/0.50 % (563013)Termination phase: shuffling
% 0.87/0.50 % (563013)Time elapsed: 0.002 s
% 0.87/0.50 % (563013)Peak memory usage: 10 MB
% 0.87/0.50 % (563013)Instructions burned: 4 (million)
% 0.87/0.50 % (563017)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=1061464121:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.87/0.50 % (563012)Instruction limit reached!
% 0.87/0.50 % (563012)------------------------------
% 0.87/0.50 % (563012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.50 % (563012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.50 % (563012)CaDiCaL version: 2.1.3
% 0.87/0.50 % (563012)Termination reason: Instruction limit
% 0.87/0.50 % (563012)Termination phase: shuffling
% 0.87/0.50 % (563012)Time elapsed: 0.008 s
% 0.87/0.50 % (563012)Peak memory usage: 10 MB
% 0.87/0.50 % (563012)Instructions burned: 20 (million)
% 0.87/0.50 % (563015)Instruction limit reached!
% 0.87/0.50 % (563015)------------------------------
% 0.87/0.50 % (563015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.50 % (563015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.50 % (563015)CaDiCaL version: 2.1.3
% 0.87/0.50 % (563015)Termination reason: Instruction limit
% 0.87/0.50 % (563015)Termination phase: Property scanning
% 0.87/0.50 % (563015)Time elapsed: 0.010 s
% 0.87/0.50 % (563015)Peak memory usage: 10 MB
% 0.87/0.50 % (563015)Instructions burned: 24 (million)
% 0.87/0.50 % (563016)Instruction limit reached!
% 0.87/0.50 % (563016)------------------------------
% 0.87/0.50 % (563016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.50 % (563016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.50 % (563016)CaDiCaL version: 2.1.3
% 0.87/0.50 % (563016)Termination reason: Instruction limit
% 0.87/0.50 % (563016)Termination phase: Property scanning
% 0.87/0.50 % (563016)Time elapsed: 0.018 s
% 0.87/0.50 % (563016)Peak memory usage: 11 MB
% 0.87/0.50 % (563016)Instructions burned: 79 (million)
% 0.87/0.50 % (563029)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.87/0.50 % (563028)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=375386425:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.87/0.50 % (563029)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=660371428:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.87/0.53 % (563028)Instruction limit reached!
% 0.87/0.53 % (563028)------------------------------
% 0.87/0.53 % (563028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.53 % (563028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.53 % (563028)CaDiCaL version: 2.1.3
% 0.87/0.53 % (563028)Termination reason: Instruction limit
% 0.87/0.53 % (563028)Termination phase: shuffling
% 0.87/0.53 % (563028)Time elapsed: 0.003 s
% 0.87/0.53 % (563028)Peak memory usage: 10 MB
% 0.87/0.53 % (563028)Instructions burned: 6 (million)
% 0.87/0.53 % (563030)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=4074889961:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.87/0.53 % (563029)Instruction limit reached!
% 0.87/0.53 % (563029)------------------------------
% 0.87/0.53 % (563029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.53 % (563029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.53 % (563029)CaDiCaL version: 2.1.3
% 0.87/0.53 % (563029)Termination reason: Instruction limit
% 0.87/0.53 % (563029)Termination phase: shuffling
% 0.87/0.53 % (563029)Time elapsed: 0.004 s
% 0.87/0.53 % (563029)Peak memory usage: 10 MB
% 0.87/0.53 % (563029)Instructions burned: 9 (million)
% 0.87/0.53 % (563011)Instruction limit reached!
% 0.87/0.53 % (563011)------------------------------
% 0.87/0.53 % (563011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.53 % (563011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.53 % (563011)CaDiCaL version: 2.1.3
% 0.87/0.53 % (563011)Termination reason: Instruction limit
% 0.87/0.53 % (563011)Termination phase: Function definition elimination
% 0.87/0.53 % (563011)Time elapsed: 0.038 s
% 0.87/0.53 % (563011)Peak memory usage: 11 MB
% 0.87/0.53 % (563011)Instructions burned: 88 (million)
% 0.87/0.53 % (563033)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.87/0.53 % (563033)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.87/0.53 % (563030)Instruction limit reached!
% 0.87/0.53 % (563030)------------------------------
% 0.87/0.53 % (563030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.53 % (563030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.53 % (563030)CaDiCaL version: 2.1.3
% 0.87/0.53 % (563030)Termination reason: Instruction limit
% 0.87/0.53 % (563030)Termination phase: shuffling
% 0.87/0.53 % (563030)Time elapsed: 0.006 s
% 0.87/0.53 % (563030)Peak memory usage: 10 MB
% 0.87/0.53 % (563030)Instructions burned: 13 (million)
% 0.87/0.53 % (563026)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3325575836:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.87/0.53 % (563033)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=205750046:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.87/0.53 % (563026)Instruction limit reached!
% 0.87/0.53 % (563026)------------------------------
% 0.87/0.53 % (563026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.53 % (563026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.53 % (563026)CaDiCaL version: 2.1.3
% 0.87/0.53 % (563026)Termination reason: Instruction limit
% 0.87/0.53 % (563026)Termination phase: shuffling
% 0.87/0.53 % (563026)Time elapsed: 0.002 s
% 0.87/0.53 % (563026)Peak memory usage: 10 MB
% 0.87/0.53 % (563026)Instructions burned: 2 (million)
% 0.87/0.53 % (563033)Instruction limit reached!
% 0.87/0.53 % (563033)------------------------------
% 0.87/0.53 % (563033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.53 % (563033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.53 % (563033)CaDiCaL version: 2.1.3
% 0.87/0.53 % (563033)Termination reason: Instruction limit
% 0.87/0.53 % (563033)Termination phase: Property scanning
% 0.87/0.53 % (563033)Time elapsed: 0.009 s
% 0.87/0.53 % (563033)Peak memory usage: 10 MB
% 0.87/0.54 % (563033)Instructions burned: 41 (million)
% 0.87/0.54 % (563035)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=3965170345:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.87/0.54 % (563037)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.87/0.54 % (563036)lrs+10_1_si=on:cs=on:random_seed=4190926939:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.87/0.54 % (563037)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=1554421762:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.87/0.54 % (563041)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3761021154:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.87/0.54 % (563037)Instruction limit reached!
% 0.87/0.54 % (563037)------------------------------
% 0.87/0.54 % (563037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563037)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563037)Termination reason: Instruction limit
% 0.87/0.54 % (563037)Termination phase: shuffling
% 0.87/0.54 % (563037)Time elapsed: 0.003 s
% 0.87/0.54 % (563037)Peak memory usage: 10 MB
% 0.87/0.54 % (563037)Instructions burned: 7 (million)
% 0.87/0.54 % (563036)Instruction limit reached!
% 0.87/0.54 % (563036)------------------------------
% 0.87/0.54 % (563036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563036)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563036)Termination reason: Instruction limit
% 0.87/0.54 % (563036)Termination phase: shuffling
% 0.87/0.54 % (563036)Time elapsed: 0.004 s
% 0.87/0.54 % (563036)Peak memory usage: 10 MB
% 0.87/0.54 % (563036)Instructions burned: 9 (million)
% 0.87/0.54 % (563040)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1933511406:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 0.87/0.54 % (563046)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=4136546080:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.87/0.54 % (563047)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1776396652:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.87/0.54 % (563041)Refutation not found, incomplete strategy
% 0.87/0.54 % (563041)------------------------------
% 0.87/0.54 % (563041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563041)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563041)Termination reason: Refutation not found, incomplete strategy
% 0.87/0.54 % (563041)Time elapsed: 0.021 s
% 0.87/0.54 % (563041)Peak memory usage: 13 MB
% 0.87/0.54 % (563041)Instructions burned: 86 (million)
% 0.87/0.54 % (563041)------------------------------
% 0.87/0.54 % (563041)------------------------------
% 0.87/0.54 % (563040)Instruction limit reached!
% 0.87/0.54 % (563040)------------------------------
% 0.87/0.54 % (563040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563040)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563040)Termination reason: Instruction limit
% 0.87/0.54 % (563040)Termination phase: Property scanning
% 0.87/0.54 % (563040)Time elapsed: 0.018 s
% 0.87/0.54 % (563040)Peak memory usage: 10 MB
% 0.87/0.54 % (563040)Instructions burned: 38 (million)
% 0.87/0.54 % (563047)Instruction limit reached!
% 0.87/0.54 % (563047)------------------------------
% 0.87/0.54 % (563047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563047)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563047)Termination reason: Instruction limit
% 0.87/0.54 % (563047)Termination phase: shuffling
% 0.87/0.54 % (563047)Time elapsed: 0.007 s
% 0.87/0.54 % (563047)Peak memory usage: 10 MB
% 0.87/0.54 % (563047)Instructions burned: 15 (million)
% 0.87/0.54 % (563035)Instruction limit reached!
% 0.87/0.54 % (563035)------------------------------
% 0.87/0.54 % (563035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563035)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563035)Termination reason: Instruction limit
% 0.87/0.54 % (563035)Termination phase: Property scanning
% 0.87/0.54 % (563035)Time elapsed: 0.036 s
% 0.87/0.54 % (563035)Peak memory usage: 11 MB
% 0.87/0.54 % (563035)Instructions burned: 86 (million)
% 0.87/0.54 % (563046)Instruction limit reached!
% 0.87/0.54 % (563046)------------------------------
% 0.87/0.54 % (563046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563046)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563046)Termination reason: Instruction limit
% 0.87/0.54 % (563046)Termination phase: Property scanning
% 0.87/0.54 % (563046)Time elapsed: 0.012 s
% 0.87/0.54 % (563046)Peak memory usage: 10 MB
% 0.87/0.54 % (563046)Instructions burned: 27 (million)
% 0.87/0.54 % (563017)Instruction limit reached!
% 0.87/0.54 % (563017)------------------------------
% 0.87/0.54 % (563017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563017)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563017)Termination reason: Instruction limit
% 0.87/0.54 % (563017)Termination phase: Saturation
% 0.87/0.54 % (563017)Time elapsed: 0.090 s
% 0.87/0.54 % (563017)Peak memory usage: 13 MB
% 0.87/0.54 % (563017)Instructions burned: 159 (million)
% 0.87/0.54 % (563055)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1167681910:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.87/0.54 % (563057)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2003076540:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.87/0.54 % (563059)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2092858710:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.87/0.54 % (563060)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1298582066:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.87/0.54 % (563059)Instruction limit reached!
% 0.87/0.54 % (563059)------------------------------
% 0.87/0.54 % (563059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563059)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563059)Termination reason: Instruction limit
% 0.87/0.54 % (563059)Termination phase: shuffling
% 0.87/0.54 % (563059)Time elapsed: 0.002 s
% 0.87/0.54 % (563059)Peak memory usage: 10 MB
% 0.87/0.54 % (563059)Instructions burned: 4 (million)
% 0.87/0.54 % (563057)Instruction limit reached!
% 0.87/0.54 % (563057)------------------------------
% 0.87/0.54 % (563057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563057)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563057)Termination reason: Instruction limit
% 0.87/0.54 % (563057)Termination phase: shuffling
% 0.87/0.54 % (563057)Time elapsed: 0.006 s
% 0.87/0.54 % (563057)Peak memory usage: 10 MB
% 0.87/0.54 % (563057)Instructions burned: 15 (million)
% 0.87/0.54 % (563063)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3950399249:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.87/0.54 % (563066)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3884199745:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.87/0.54 % (563060)Instruction limit reached!
% 0.87/0.54 % (563060)------------------------------
% 0.87/0.54 % (563060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563060)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563060)Termination reason: Instruction limit
% 0.87/0.54 % (563060)Termination phase: shuffling
% 0.87/0.54 % (563060)Time elapsed: 0.012 s
% 0.87/0.54 % (563060)Peak memory usage: 10 MB
% 0.87/0.54 % (563060)Instructions burned: 27 (million)
% 0.87/0.54 % (563063)Instruction limit reached!
% 0.87/0.54 % (563063)------------------------------
% 0.87/0.54 % (563063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563063)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563063)Termination reason: Instruction limit
% 0.87/0.54 % (563063)Termination phase: Property scanning
% 0.87/0.54 % (563063)Time elapsed: 0.011 s
% 0.87/0.54 % (563063)Peak memory usage: 10 MB
% 0.87/0.54 % (563063)Instructions burned: 25 (million)
% 0.87/0.54 % (563014) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-563005-563014"...
% 0.87/0.54 % (563076)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.87/0.54 % (563076)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.87/0.54 % (563078)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.87/0.54 % (563014)...printing done.
% 0.87/0.54 % (563076)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3073396640:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.87/0.54 % (563078)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=2208565349:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.87/0.54 % (563014)Refutation found. Thanks to Tanya!
% 0.87/0.54 % SZS status Theorem for theBenchmark
% 0.87/0.54 % SZS output start Proof for theBenchmark
% See solution above
% 0.87/0.54 % (563014)------------------------------
% 0.87/0.54 % (563014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.54 % (563014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.54 % (563014)CaDiCaL version: 2.1.3
% 0.87/0.54 % (563014)Termination reason: Refutation
% 0.87/0.54 % (563014)Time elapsed: 0.127 s
% 0.87/0.54 % (563014)Peak memory usage: 15 MB
% 0.87/0.54 % (563014)Instructions burned: 282 (million)
% 0.87/0.54 % (563005)Success in time 0.195 s
% 0.87/0.54 % Vampire exiting
%------------------------------------------------------------------------------