%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP156^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 : n006.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:35 AM UTC 2026
% Result : Theorem 1.16s 0.49s
% Output : Refutation 1.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 13
% Syntax : Number of formulae : 69 ( 30 unt; 0 typ; 4 def)
% Number of atoms : 183 ( 77 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 384 ( 48 ~; 47 |; 3 &; 276 @)
% ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 33 ( 32 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 167 ( 164 usr; 27 con; 0-4 aty)
% Number of variables : 22 ( 0 sgn 22 !; 0 ?; 22 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
set_Pr1741234931a_real: $tType ).
thf(type_def_6,type,
produc1826081171a_real: $tType ).
thf(type_def_7,type,
set_Pr1948701895od_a_a: $tType ).
thf(type_def_8,type,
produc1572603623od_a_a: $tType ).
thf(type_def_9,type,
produc826782210l_real: $tType ).
thf(type_def_10,type,
produc578556564l_real: $tType ).
thf(type_def_11,type,
produc1286132450l_real: $tType ).
thf(type_def_12,type,
produc1088645164real_a: $tType ).
thf(type_def_13,type,
produc2096821232od_a_a: $tType ).
thf(type_def_14,type,
produc348734722a_real: $tType ).
thf(type_def_15,type,
produc1921647824od_a_a: $tType ).
thf(type_def_16,type,
produc1016684094_a_a_a: $tType ).
thf(type_def_17,type,
set_Pr147102617l_real: $tType ).
thf(type_def_18,type,
produc391212143l_real: $tType ).
thf(type_def_19,type,
produc443621487t_real: $tType ).
thf(type_def_20,type,
set_se1596668135od_a_a: $tType ).
thf(type_def_21,type,
set_Pr1928503567a_real: $tType ).
thf(type_def_22,type,
produc1396156303t_real: $tType ).
thf(type_def_23,type,
produc1232925073real_a: $tType ).
thf(type_def_24,type,
produc1923333543_set_a: $tType ).
thf(type_def_25,type,
produc957004601l_real: $tType ).
thf(type_def_26,type,
set_Product_prod_a_a: $tType ).
thf(type_def_27,type,
product_prod_a_set_a: $tType ).
thf(type_def_28,type,
product_prod_a_real: $tType ).
thf(type_def_29,type,
product_prod_real_a: $tType ).
thf(type_def_30,type,
set_set_real: $tType ).
thf(type_def_31,type,
product_prod_a_a: $tType ).
thf(type_def_32,type,
set_set_a: $tType ).
thf(type_def_33,type,
set_real: $tType ).
thf(type_def_34,type,
set_a: $tType ).
thf(type_def_35,type,
real: $tType ).
thf(type_def_36,type,
a: $tType ).
thf(type_def_37,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
one_one_real: real ).
thf(func_def_1,type,
plus_p77862768l_real: produc957004601l_real > produc957004601l_real > produc957004601l_real ).
thf(func_def_2,type,
plus_p2005278886t_real: produc443621487t_real > produc443621487t_real > produc443621487t_real ).
thf(func_def_3,type,
plus_p125342128_set_a: produc1923333543_set_a > produc1923333543_set_a > produc1923333543_set_a ).
thf(func_def_4,type,
plus_p1243198544real_a: product_prod_real_a > product_prod_real_a > product_prod_real_a ).
thf(func_def_5,type,
plus_p1952869542l_real: produc391212143l_real > produc391212143l_real > produc391212143l_real ).
thf(func_def_6,type,
plus_p1582417306real_a: produc1232925073real_a > produc1232925073real_a > produc1232925073real_a ).
thf(func_def_7,type,
plus_p541014626a_real: product_prod_a_real > product_prod_a_real > product_prod_a_real ).
thf(func_def_8,type,
plus_p1745648536t_real: produc1396156303t_real > produc1396156303t_real > produc1396156303t_real ).
thf(func_def_9,type,
plus_p1265825342_set_a: product_prod_a_set_a > product_prod_a_set_a > product_prod_a_set_a ).
thf(func_def_10,type,
plus_p1505579230od_a_a: product_prod_a_a > product_prod_a_a > product_prod_a_a ).
thf(func_def_11,type,
plus_plus_real: real > real > real ).
thf(func_def_12,type,
plus_p1708760016l_real: set_Pr147102617l_real > set_Pr147102617l_real > set_Pr147102617l_real ).
thf(func_def_13,type,
plus_p130512152a_real: set_Pr1928503567a_real > set_Pr1928503567a_real > set_Pr1928503567a_real ).
thf(func_def_14,type,
plus_p634297534od_a_a: set_Product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a ).
thf(func_def_15,type,
plus_plus_set_real: set_real > set_real > set_real ).
thf(func_def_16,type,
plus_p1613276318od_a_a: set_se1596668135od_a_a > set_se1596668135od_a_a > set_se1596668135od_a_a ).
thf(func_def_17,type,
plus_p768704801t_real: set_set_real > set_set_real > set_set_real ).
thf(func_def_18,type,
plus_plus_set_set_a: set_set_a > set_set_a > set_set_a ).
thf(func_def_19,type,
plus_plus_set_a: set_a > set_a > set_a ).
thf(func_def_20,type,
plus_plus_a: a > a > a ).
thf(func_def_21,type,
zero_z342251165l_real: produc578556564l_real ).
thf(func_def_22,type,
zero_z1937883107real_a: produc1088645164real_a ).
thf(func_def_23,type,
zero_z590476811l_real: produc826782210l_real ).
thf(func_def_24,type,
zero_z396988537od_a_a: produc2096821232od_a_a ).
thf(func_def_25,type,
zero_z659284464l_real: produc957004601l_real ).
thf(func_def_26,type,
zero_z1407338960real_a: product_prod_real_a ).
thf(func_def_27,type,
zero_z2135370393l_real: produc1286132450l_real ).
thf(func_def_28,type,
zero_z53797895od_a_a: produc1921647824od_a_a ).
thf(func_def_29,type,
zero_z705155042a_real: product_prod_a_real ).
thf(func_def_30,type,
zero_z950819678od_a_a: product_prod_a_a ).
thf(func_def_31,type,
zero_zero_real: real ).
thf(func_def_32,type,
zero_z257140542od_a_a: set_Product_prod_a_a ).
thf(func_def_33,type,
zero_zero_set_real: set_real ).
thf(func_def_34,type,
zero_zero_set_a: set_a ).
thf(func_def_35,type,
zero_zero_a: a ).
thf(func_def_36,type,
ord_less_real: real > real > $o ).
thf(func_def_37,type,
ord_le108336051od_a_a: set_Product_prod_a_a > set_Product_prod_a_a > $o ).
thf(func_def_38,type,
ord_le1342644953l_real: produc957004601l_real > produc957004601l_real > $o ).
thf(func_def_39,type,
ord_less_eq_real: real > real > $o ).
thf(func_def_40,type,
ord_le1824328871od_a_a: set_Product_prod_a_a > set_Product_prod_a_a > $o ).
thf(func_def_41,type,
ord_less_eq_set_real: set_real > set_real > $o ).
thf(func_def_42,type,
prefer1113819806a_real: set_Pr1741234931a_real > $o ).
thf(func_def_43,type,
prefer225425826od_a_a: set_Pr1948701895od_a_a > $o ).
thf(func_def_44,type,
prefer1247792113f_real: set_Pr147102617l_real > $o ).
thf(func_def_45,type,
prefer529818233pref_a: set_Product_prod_a_a > $o ).
thf(func_def_46,type,
produc1175086478l_real: produc957004601l_real > real > produc578556564l_real ).
thf(func_def_47,type,
produc1430099868real_a: produc957004601l_real > a > produc1088645164real_a ).
thf(func_def_48,type,
produc886678603a_real: product_prod_a_real > product_prod_a_real > produc1826081171a_real ).
thf(func_def_49,type,
produc1474507607od_a_a: product_prod_a_a > product_prod_a_a > produc1572603623od_a_a ).
thf(func_def_50,type,
produc454274172a_real: product_prod_a_a > real > produc348734722a_real ).
thf(func_def_51,type,
produc2061588782_a_a_a: product_prod_a_a > a > produc1016684094_a_a_a ).
thf(func_def_52,type,
produc1926903988l_real: real > produc957004601l_real > produc826782210l_real ).
thf(func_def_53,type,
produc454550562od_a_a: real > product_prod_a_a > produc2096821232od_a_a ).
thf(func_def_54,type,
produc705216881l_real: real > real > produc957004601l_real ).
thf(func_def_55,type,
produc247649703t_real: real > set_real > produc443621487t_real ).
thf(func_def_56,type,
produc1872317017_set_a: real > set_a > produc1923333543_set_a ).
thf(func_def_57,type,
product_Pair_real_a: real > a > product_prod_real_a ).
thf(func_def_58,type,
produc1812461223l_real: set_real > real > produc391212143l_real ).
thf(func_def_59,type,
produc617496131real_a: set_real > a > produc1232925073real_a ).
thf(func_def_60,type,
produc64206290l_real: a > produc957004601l_real > produc1286132450l_real ).
thf(func_def_61,type,
produc1299253312od_a_a: a > product_prod_a_a > produc1921647824od_a_a ).
thf(func_def_62,type,
product_Pair_a_real: a > real > product_prod_a_real ).
thf(func_def_63,type,
produc1391501065t_real: a > set_real > produc1396156303t_real ).
thf(func_def_64,type,
product_Pair_a_set_a: a > set_a > product_prod_a_set_a ).
thf(func_def_65,type,
product_Pair_a_a: a > a > product_prod_a_a ).
thf(func_def_66,type,
real_V368978776od_a_a: real > produc1572603623od_a_a > produc1572603623od_a_a ).
thf(func_def_67,type,
real_V195069393a_real: real > produc348734722a_real > produc348734722a_real ).
thf(func_def_68,type,
real_V1538726831_a_a_a: real > produc1016684094_a_a_a > produc1016684094_a_a_a ).
thf(func_def_69,type,
real_V1943155903od_a_a: real > produc2096821232od_a_a > produc2096821232od_a_a ).
thf(func_def_70,type,
real_V1139189034l_real: real > produc957004601l_real > produc957004601l_real ).
thf(func_def_71,type,
real_V1214981142real_a: real > product_prod_real_a > product_prod_real_a ).
thf(func_def_72,type,
real_V296206913od_a_a: real > produc1921647824od_a_a > produc1921647824od_a_a ).
thf(func_def_73,type,
real_V512797224a_real: real > product_prod_a_real > product_prod_a_real ).
thf(func_def_74,type,
real_V543523736od_a_a: real > product_prod_a_a > product_prod_a_a ).
thf(func_def_75,type,
real_V453051771R_real: real > real > real ).
thf(func_def_76,type,
real_V1035702895aleR_a: real > a > a ).
thf(func_def_77,type,
collec1300223524l_real: ( produc957004601l_real > $o ) > set_Pr147102617l_real ).
thf(func_def_78,type,
collec645855634od_a_a: ( product_prod_a_a > $o ) > set_Product_prod_a_a ).
thf(func_def_79,type,
collect_real: ( real > $o ) > set_real ).
thf(func_def_80,type,
collect_a: ( a > $o ) > set_a ).
thf(func_def_81,type,
member384820540a_real: produc1826081171a_real > set_Pr1741234931a_real > $o ).
thf(func_def_82,type,
member2057358096od_a_a: produc1572603623od_a_a > set_Pr1948701895od_a_a > $o ).
thf(func_def_83,type,
member1068169442l_real: produc957004601l_real > set_Pr147102617l_real > $o ).
thf(func_def_84,type,
member1103263856a_real: product_prod_a_real > set_Pr1928503567a_real > $o ).
thf(func_def_85,type,
member449909584od_a_a: product_prod_a_a > set_Product_prod_a_a > $o ).
thf(func_def_86,type,
member_real: real > set_real > $o ).
thf(func_def_87,type,
member1838126896od_a_a: set_Product_prod_a_a > set_se1596668135od_a_a > $o ).
thf(func_def_88,type,
member_set_real: set_real > set_set_real > $o ).
thf(func_def_89,type,
member_set_a: set_a > set_set_a > $o ).
thf(func_def_90,type,
member_a: a > set_a > $o ).
thf(func_def_91,type,
relation: set_Product_prod_a_a ).
thf(func_def_92,type,
u: real ).
thf(func_def_93,type,
v: real ).
thf(func_def_94,type,
x: a ).
thf(func_def_95,type,
y: a ).
thf(func_def_99,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_100,type,
vOR: $o > $o > $o ).
thf(func_def_101,type,
vAND: $o > $o > $o ).
thf(func_def_102,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_103,type,
vIMP: $o > $o > $o ).
thf(func_def_104,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_105,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_106,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_107,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_108,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_109,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_110,type,
sP0: real > real > real > $o ).
thf(func_def_111,type,
sP1: real > real > real > $o ).
thf(func_def_112,type,
sP2: real > real > real > $o ).
thf(func_def_113,type,
sK3: set_Product_prod_a_a > a ).
thf(func_def_114,type,
sK4: set_Product_prod_a_a > a ).
thf(func_def_115,type,
sK5: set_Product_prod_a_a > real ).
thf(func_def_116,type,
sK6: set_Product_prod_a_a > real ).
thf(func_def_117,type,
sK7: ( real > real ) > real ).
thf(func_def_118,type,
sK8: ( real > real ) > real ).
thf(func_def_119,type,
sK9: product_prod_a_a > a ).
thf(func_def_120,type,
sK10: product_prod_a_a > a ).
thf(func_def_121,type,
sK11: ( product_prod_a_a > $o ) > a ).
thf(func_def_122,type,
sK12: ( product_prod_a_a > $o ) > a ).
thf(func_def_123,type,
sK13: product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_124,type,
sK14: product_prod_a_a > set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_125,type,
sK15: ( real > real ) > real ).
thf(func_def_126,type,
sK16: ( real > real ) > real ).
thf(func_def_127,type,
sK17: ( real > real ) > real ).
thf(func_def_128,type,
sK18: ( real > real ) > real ).
thf(func_def_129,type,
sK19: real > real > real ).
thf(func_def_130,type,
sK20: set_Pr147102617l_real > real ).
thf(func_def_131,type,
sK21: set_Pr147102617l_real > real ).
thf(func_def_132,type,
sK22: set_Pr147102617l_real > real ).
thf(func_def_133,type,
sK23: set_Pr147102617l_real > real ).
thf(func_def_134,type,
sK24: ( product_prod_a_a > $o ) > a ).
thf(func_def_135,type,
sK25: ( product_prod_a_a > $o ) > a ).
thf(func_def_136,type,
sK26: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_137,type,
sK27: product_prod_a_a > a ).
thf(func_def_138,type,
sK28: product_prod_a_a > a ).
thf(func_def_139,type,
sK29: set_Pr147102617l_real > real ).
thf(func_def_140,type,
sK30: set_Pr147102617l_real > real ).
thf(func_def_141,type,
sK31: set_Pr147102617l_real > real ).
thf(func_def_142,type,
sK32: set_Pr147102617l_real > real ).
thf(func_def_143,type,
sK33: set_Product_prod_a_a > a ).
thf(func_def_144,type,
sK34: set_Product_prod_a_a > a ).
thf(func_def_145,type,
sK35: set_Product_prod_a_a > real ).
thf(func_def_146,type,
sK36: set_Product_prod_a_a > real ).
thf(func_def_147,type,
sK37: ( real > real ) > real ).
thf(func_def_148,type,
sK38: ( real > real ) > real ).
thf(func_def_149,type,
vNOT: $o > $o ).
thf(func_def_150,type,
sK39: set_Pr147102617l_real > real ).
thf(func_def_151,type,
sK40: set_Pr147102617l_real > real ).
thf(func_def_152,type,
sK41: set_Pr147102617l_real > real ).
thf(func_def_153,type,
sK42: set_Pr147102617l_real > real ).
thf(func_def_154,type,
sK43: set_Product_prod_a_a > a ).
thf(func_def_155,type,
sK44: set_Product_prod_a_a > a ).
thf(func_def_156,type,
sK45: set_Product_prod_a_a > real ).
thf(func_def_157,type,
sK46: set_Product_prod_a_a > real ).
thf(func_def_158,type,
sK47: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_159,type,
sK48: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_160,type,
sK49: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_161,type,
sK50: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(f6,axiom,
member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_assms_I2_J) ).
thf(f7,axiom,
( ( ( u != one_one_real )
& ( u != zero_zero_real ) )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6__092_060open_062u_A_092_060noteq_062_A0_A_092_060and_062_Au_A_092_060noteq_062_A1_A_092_060longrightarrow_062_Au_A_K_092_060_094sub_062R_Ax_A_L_Av_A_K_092_060_094sub_062R_Ay_A_092_060succeq_062_Ay_092_060close_062) ).
thf(f8,axiom,
( ( u = zero_zero_real )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_u__0) ).
thf(f10,axiom,
( ( plus_plus_real @ u @ v )
= one_one_real ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_assms_I5_J) ).
thf(f73,axiom,
! [X1: real,X0: real] :
( ( X0
= ( plus_plus_real @ X0 @ X1 ) )
= ( X1 = zero_zero_real ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_add__cancel__right__right) ).
thf(f187,axiom,
! [X0: a] :
( ( plus_plus_a @ X0 @ zero_zero_a )
= X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_add_Ocomm__neutral) ).
thf(f239,axiom,
! [X0: a] :
( ( real_V1035702895aleR_a @ zero_zero_real @ X0 )
= zero_zero_a ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_scale__zero__left) ).
thf(f242,axiom,
! [X0: a] :
( ( real_V1035702895aleR_a @ one_one_real @ X0 )
= X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_scaleR__one) ).
thf(f354,conjecture,
member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(f355,negated_conjecture,
~ ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ),
inference(negated_conjecture,[status(cth)],[f354]) ).
thf(f436,plain,
! [X0: real,X1: real] :
( ( ( plus_plus_real @ X1 @ X0 )
= X1 )
= ( zero_zero_real = X0 ) ),
inference(rectify,[],[f73]) ).
thf(f437,plain,
! [X1: real,X0: real] :
( ( zero_zero_real = X0 )
= ( ( plus_plus_real @ X1 @ X0 )
= X1 ) ),
inference(fool_elimination,[],[f436]) ).
thf(f440,plain,
member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation,
inference(rectify,[],[f6]) ).
thf(f441,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation )
= $true ),
inference(fool_elimination,[],[f440]) ).
thf(f448,plain,
( ( u = zero_zero_real )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ) ),
inference(rectify,[],[f8]) ).
thf(f449,plain,
( ( u = zero_zero_real )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true ) ),
inference(fool_elimination,[],[f448]) ).
thf(f552,plain,
( ( ( u != one_one_real )
& ( u != zero_zero_real ) )
=> ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ) ),
inference(rectify,[],[f7]) ).
thf(f553,plain,
( ( ( u != one_one_real )
& ( u != zero_zero_real ) )
=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true ) ),
inference(fool_elimination,[],[f552]) ).
thf(f604,plain,
~ ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ),
inference(rectify,[],[f355]) ).
thf(f605,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
!= $true ),
inference(fool_elimination,[],[f604]) ).
thf(f742,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
!= $true ),
inference(flattening,[],[f605]) ).
thf(f834,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true )
| ( u = one_one_real )
| ( u = zero_zero_real ) ),
inference(ennf_transformation,[],[f553]) ).
thf(f835,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true )
| ( u = zero_zero_real )
| ( u = one_one_real ) ),
inference(flattening,[],[f834]) ).
thf(f908,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true )
| ( u != zero_zero_real ) ),
inference(ennf_transformation,[],[f449]) ).
thf(f1078,plain,
! [X0: real,X1: real] :
( ( zero_zero_real = X1 )
= ( ( plus_plus_real @ X0 @ X1 )
= X0 ) ),
inference(rectify,[],[f437]) ).
thf(f1188,plain,
! [X0: a] :
( ( plus_plus_a @ X0 @ zero_zero_a )
= X0 ),
inference(cnf_transformation,[],[f187]) ).
thf(f1312,plain,
! [X0: real,X1: real] :
( ( zero_zero_real = X1 )
= ( ( plus_plus_real @ X0 @ X1 )
= X0 ) ),
inference(cnf_transformation,[],[f1078]) ).
thf(f1361,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true )
| ( u = zero_zero_real )
| ( u = one_one_real ) ),
inference(cnf_transformation,[],[f835]) ).
thf(f1362,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation )
= $true ),
inference(cnf_transformation,[],[f441]) ).
thf(f1367,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true )
| ( u != zero_zero_real ) ),
inference(cnf_transformation,[],[f908]) ).
thf(f1420,plain,
! [X0: a] :
( zero_zero_a
= ( real_V1035702895aleR_a @ zero_zero_real @ X0 ) ),
inference(cnf_transformation,[],[f239]) ).
thf(f1446,plain,
! [X0: a] :
( ( real_V1035702895aleR_a @ one_one_real @ X0 )
= X0 ),
inference(cnf_transformation,[],[f242]) ).
thf(f1458,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
!= $true ),
inference(cnf_transformation,[],[f742]) ).
thf(f1481,plain,
( one_one_real
= ( plus_plus_real @ u @ v ) ),
inference(cnf_transformation,[],[f10]) ).
thf(f1995,plain,
! [X0: real,X1: real] :
( ( ( zero_zero_real = X1 )
= $true )
| ( ( ( plus_plus_real @ X0 @ X1 )
= X0 )
= $false ) ),
inference(iff_proxy_clausification,[],[f1312]) ).
thf(f1999,plain,
! [X0: real,X1: real] :
( ( zero_zero_real = X1 )
| ( ( ( plus_plus_real @ X0 @ X1 )
= X0 )
= $false ) ),
inference(equality_proxy_clausification,[],[f1995]) ).
thf(f2000,plain,
! [X0: real,X1: real] :
( ( ( plus_plus_real @ X0 @ X1 )
!= X0 )
| ( zero_zero_real = X1 ) ),
inference(equality_proxy_clausification,[],[f1999]) ).
thf(f2401,definition,
( spl51_1
<=> ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl51_1])],[avatar_definition]) ).
thf(f2402,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ u @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation )
!= $true )
| spl51_1 ),
inference(avatar_component_clause,[],[f2401]) ).
thf(f2405,definition,
( spl51_2
<=> ( u = zero_zero_real ) ),
introduced(definition,[new_symbols(definition,[spl51_2])],[avatar_definition]) ).
thf(f2408,plain,
( spl51_1
| ~ spl51_2 ),
inference(avatar_split_clause,[],[f1367,f2405,f2401]) ).
thf(f2410,definition,
( spl51_3
<=> ( u = one_one_real ) ),
introduced(definition,[new_symbols(definition,[spl51_3])],[avatar_definition]) ).
thf(f2412,plain,
( ( u = one_one_real )
| ~ spl51_3 ),
inference(avatar_component_clause,[],[f2410]) ).
thf(f2413,plain,
( spl51_1
| spl51_3
| spl51_2 ),
inference(avatar_split_clause,[],[f1361,f2405,f2410,f2401]) ).
thf(f2414,plain,
~ spl51_1,
inference(avatar_split_clause,[],[f1458,f2401]) ).
thf(f2417,plain,
( ( one_one_real
= ( plus_plus_real @ one_one_real @ v ) )
| ~ spl51_3 ),
inference(forward_demodulation,[],[f1481,f2412]) ).
thf(f2561,plain,
( ( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ ( real_V1035702895aleR_a @ one_one_real @ x ) @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ) )
| spl51_1
| ~ spl51_3 ),
inference(forward_demodulation,[],[f2402,f2412]) ).
thf(f2562,plain,
( ( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ x @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ) )
| spl51_1
| ~ spl51_3 ),
inference(forward_demodulation,[],[f2561,f1446]) ).
thf(f2925,definition,
( spl51_9
<=> ( zero_zero_real = v ) ),
introduced(definition,[new_symbols(definition,[spl51_9])],[avatar_definition]) ).
thf(f2927,plain,
( ( zero_zero_real = v )
| ~ spl51_9 ),
inference(avatar_component_clause,[],[f2925]) ).
thf(f3441,plain,
( ( zero_zero_real = v )
| ( one_one_real != one_one_real )
| ~ spl51_3 ),
inference(superposition,[],[f2000,f2417]) ).
thf(f3444,plain,
( ( zero_zero_real = v )
| ~ spl51_3 ),
inference(trivial_inequality_removal,[],[f3441]) ).
thf(f3445,plain,
( spl51_9
| ~ spl51_3 ),
inference(avatar_split_clause,[],[f3444,f2410,f2925]) ).
thf(f3448,plain,
( ( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ x @ ( real_V1035702895aleR_a @ zero_zero_real @ y ) ) @ y ) @ relation ) )
| spl51_1
| ~ spl51_3
| ~ spl51_9 ),
inference(superposition,[],[f2562,f2927]) ).
thf(f3457,plain,
( ( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ x @ zero_zero_a ) @ y ) @ relation ) )
| spl51_1
| ~ spl51_3
| ~ spl51_9 ),
inference(forward_demodulation,[],[f3448,f1420]) ).
thf(f3458,plain,
( ( ( member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation )
!= $true )
| spl51_1
| ~ spl51_3
| ~ spl51_9 ),
inference(forward_demodulation,[],[f3457,f1188]) ).
thf(f3459,plain,
( $false
| spl51_1
| ~ spl51_3
| ~ spl51_9 ),
inference(forward_subsumption_resolution,[],[f3458,f1362]) ).
thf(f3460,plain,
( spl51_1
| ~ spl51_3
| ~ spl51_9 ),
inference(avatar_contradiction_clause,[],[f3459]) ).
cnf(s1,plain,
( spl51_1
| ~ spl51_2 ),
inference(sat_conversion,[],[f2408]) ).
cnf(s2,plain,
( spl51_1
| spl51_2
| spl51_3 ),
inference(sat_conversion,[],[f2413]) ).
cnf(s3,plain,
~ spl51_1,
inference(sat_conversion,[],[f2414]) ).
cnf(s8,plain,
( ~ spl51_3
| spl51_9 ),
inference(sat_conversion,[],[f3445]) ).
cnf(s11,plain,
( spl51_1
| ~ spl51_3
| ~ spl51_9 ),
inference(sat_conversion,[],[f3460]) ).
cnf(s12,plain,
( spl51_2
| spl51_3 ),
inference(rat,[],[s2,s3]) ).
cnf(s13,plain,
~ spl51_2,
inference(rat,[],[s1,s3]) ).
cnf(s14,plain,
spl51_3,
inference(rat,[],[s12,s13]) ).
cnf(s15,plain,
~ spl51_9,
inference(rat,[],[s11,s3,s14]) ).
cnf(s16,plain,
$false,
inference(rat,[],[s8,s15,s14]) ).
thf(f3461,plain,
$false,
inference(avatar_sat_refutation,[],[s16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP156^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.09/0.19 % Computer : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 20:02:24 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.21/0.28 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.49/0.44 % (1241081)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.49/0.44 % (1241090)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=322602276:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.49/0.44 % (1241092)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.49/0.44 % (1241092)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.49/0.44 % (1241090)Instruction limit reached!
% 0.49/0.44 % (1241090)------------------------------
% 0.49/0.44 % (1241090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.44 % (1241090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.44 % (1241090)CaDiCaL version: 2.1.3
% 0.49/0.44 % (1241090)Termination reason: Instruction limit
% 0.49/0.44 % (1241090)Termination phase: Property scanning
% 0.49/0.44 % (1241090)Time elapsed: 0.006 s
% 0.49/0.44 % (1241090)Peak memory usage: 10 MB
% 0.49/0.44 % (1241090)Instructions burned: 24 (million)
% 0.49/0.44 % (1241088)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3565955337:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.49/0.44 % (1241087)lrs+10_16_si=on:nwc=1.5:random_seed=1228294481:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.49/0.44 % (1241089)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=2828580846: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.49/0.44 % (1241091)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3860804578:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.49/0.44 % (1241092)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=2101860678:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.49/0.44 % (1241088)Instruction limit reached!
% 0.49/0.44 % (1241088)------------------------------
% 0.49/0.44 % (1241088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.44 % (1241088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.44 % (1241088)CaDiCaL version: 2.1.3
% 0.49/0.44 % (1241088)Termination reason: Instruction limit
% 0.49/0.44 % (1241088)Termination phase: shuffling
% 0.49/0.44 % (1241088)Time elapsed: 0.004 s
% 0.49/0.44 % (1241088)Peak memory usage: 10 MB
% 0.49/0.44 % (1241088)Instructions burned: 7 (million)
% 0.49/0.44 % (1241087)Instruction limit reached!
% 0.49/0.44 % (1241087)------------------------------
% 0.49/0.44 % (1241087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.44 % (1241087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.44 % (1241087)CaDiCaL version: 2.1.3
% 0.49/0.44 % (1241087)Termination reason: Instruction limit
% 0.49/0.44 % (1241087)Termination phase: Property scanning
% 0.49/0.44 % (1241087)Time elapsed: 0.009 s
% 0.49/0.44 % (1241087)Peak memory usage: 10 MB
% 0.49/0.44 % (1241087)Instructions burned: 20 (million)
% 0.49/0.44 % (1241086)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2969438176:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.49/0.44 % (1241097)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2310802498:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.49/0.44 % (1241097)Instruction limit reached!
% 0.49/0.44 % (1241097)------------------------------
% 0.49/0.44 % (1241097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.44 % (1241097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.44 % (1241097)CaDiCaL version: 2.1.3
% 0.49/0.44 % (1241097)Termination reason: Instruction limit
% 0.49/0.44 % (1241097)Termination phase: shuffling
% 0.49/0.44 % (1241097)Time elapsed: 0.002 s
% 0.49/0.44 % (1241097)Peak memory usage: 10 MB
% 0.49/0.44 % (1241097)Instructions burned: 2 (million)
% 0.49/0.44 % (1241100)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4150875343:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.49/0.47 % (1241100)Instruction limit reached!
% 0.49/0.47 % (1241100)------------------------------
% 0.49/0.47 % (1241100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.47 % (1241100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.47 % (1241100)CaDiCaL version: 2.1.3
% 0.49/0.47 % (1241100)Termination reason: Instruction limit
% 0.49/0.47 % (1241100)Termination phase: shuffling
% 0.49/0.47 % (1241100)Time elapsed: 0.003 s
% 0.49/0.47 % (1241100)Peak memory usage: 10 MB
% 0.49/0.47 % (1241100)Instructions burned: 6 (million)
% 0.49/0.47 % (1241101)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.49/0.47 % (1241101)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1084044981:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.49/0.47 % (1241091)Instruction limit reached!
% 0.49/0.47 % (1241091)------------------------------
% 0.49/0.47 % (1241091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.47 % (1241091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.47 % (1241091)CaDiCaL version: 2.1.3
% 0.49/0.47 % (1241091)Termination reason: Instruction limit
% 0.49/0.47 % (1241091)Termination phase: Property scanning
% 0.49/0.47 % (1241091)Time elapsed: 0.036 s
% 0.49/0.47 % (1241091)Peak memory usage: 12 MB
% 0.49/0.47 % (1241105)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3981631219:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.49/0.47 % (1241091)Instructions burned: 77 (million)
% 0.49/0.47 % (1241101)Instruction limit reached!
% 0.49/0.47 % (1241101)------------------------------
% 0.49/0.47 % (1241101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.47 % (1241101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.47 % (1241101)CaDiCaL version: 2.1.3
% 0.49/0.47 % (1241101)Termination reason: Instruction limit
% 0.49/0.47 % (1241101)Termination phase: shuffling
% 0.49/0.47 % (1241101)Time elapsed: 0.004 s
% 0.49/0.47 % (1241101)Peak memory usage: 10 MB
% 0.49/0.47 % (1241101)Instructions burned: 8 (million)
% 0.49/0.47 % (1241105)Instruction limit reached!
% 0.49/0.47 % (1241105)------------------------------
% 0.49/0.47 % (1241105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.47 % (1241105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.47 % (1241105)CaDiCaL version: 2.1.3
% 0.49/0.47 % (1241105)Termination reason: Instruction limit
% 0.49/0.47 % (1241105)Termination phase: shuffling
% 0.49/0.47 % (1241105)Time elapsed: 0.003 s
% 0.49/0.47 % (1241105)Peak memory usage: 10 MB
% 0.49/0.47 % (1241105)Instructions burned: 13 (million)
% 0.49/0.47 % (1241106)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.49/0.47 % (1241106)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.49/0.47 % (1241111)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.49/0.47 % (1241106)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1873340707: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.49/0.47 % (1241111)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=1496347413:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.49/0.47 % (1241111)Instruction limit reached!
% 0.49/0.47 % (1241111)------------------------------
% 0.49/0.47 % (1241111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.47 % (1241111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.47 % (1241111)CaDiCaL version: 2.1.3
% 0.49/0.47 % (1241111)Termination reason: Instruction limit
% 0.49/0.47 % (1241111)Termination phase: shuffling
% 0.49/0.47 % (1241111)Time elapsed: 0.001 s
% 0.49/0.47 % (1241111)Peak memory usage: 10 MB
% 0.49/0.47 % (1241111)Instructions burned: 3 (million)
% 1.16/0.49 % (1241086)Instruction limit reached!
% 1.16/0.49 % (1241086)------------------------------
% 1.16/0.49 % (1241086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241086)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241086)Termination reason: Instruction limit
% 1.16/0.49 % (1241086)Termination phase: Property scanning
% 1.16/0.49 % (1241086)Time elapsed: 0.040 s
% 1.16/0.49 % (1241086)Peak memory usage: 12 MB
% 1.16/0.49 % (1241086)Instructions burned: 89 (million)
% 1.16/0.49 % (1241109)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=3175726295:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.16/0.49 % (1241110)lrs+10_1_si=on:cs=on:random_seed=2639651000:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.16/0.49 % (1241106)Instruction limit reached!
% 1.16/0.49 % (1241106)------------------------------
% 1.16/0.49 % (1241106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241106)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241106)Termination reason: Instruction limit
% 1.16/0.49 % (1241106)Termination phase: shuffling
% 1.16/0.49 % (1241106)Time elapsed: 0.013 s
% 1.16/0.49 % (1241106)Peak memory usage: 10 MB
% 1.16/0.49 % (1241106)Instructions burned: 28 (million)
% 1.16/0.49 % (1241110)Instruction limit reached!
% 1.16/0.49 % (1241110)------------------------------
% 1.16/0.49 % (1241110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241110)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241110)Termination reason: Instruction limit
% 1.16/0.49 % (1241110)Termination phase: shuffling
% 1.16/0.49 % (1241110)Time elapsed: 0.004 s
% 1.16/0.49 % (1241110)Peak memory usage: 10 MB
% 1.16/0.49 % (1241110)Instructions burned: 8 (million)
% 1.16/0.49 % (1241118)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3878863837:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.16/0.49 % (1241118)Instruction limit reached!
% 1.16/0.49 % (1241118)------------------------------
% 1.16/0.49 % (1241118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241118)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241118)Termination reason: Instruction limit
% 1.16/0.49 % (1241118)Termination phase: Preprocessing 3
% 1.16/0.49 % (1241118)Time elapsed: 0.009 s
% 1.16/0.49 % (1241118)Peak memory usage: 11 MB
% 1.16/0.49 % (1241118)Instructions burned: 38 (million)
% 1.16/0.49 % (1241120)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=973058463:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.16/0.49 % (1241092)Instruction limit reached!
% 1.16/0.49 % (1241092)------------------------------
% 1.16/0.49 % (1241092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241092)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241092)Termination reason: Instruction limit
% 1.16/0.49 % (1241092)Termination phase: Saturation
% 1.16/0.49 % (1241092)Time elapsed: 0.075 s
% 1.16/0.49 % (1241092)Peak memory usage: 14 MB
% 1.16/0.49 % (1241092)Instructions burned: 157 (million)
% 1.16/0.49 % (1241125)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1392730185:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.16/0.49 % (1241127)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3036788152:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.16/0.49 % (1241131)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=534495669:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.16/0.49 % (1241127)Instruction limit reached!
% 1.16/0.49 % (1241127)------------------------------
% 1.16/0.49 % (1241127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241127)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241127)Termination reason: Instruction limit
% 1.16/0.49 % (1241127)Termination phase: Property scanning
% 1.16/0.49 % (1241127)Time elapsed: 0.007 s
% 1.16/0.49 % (1241127)Peak memory usage: 10 MB
% 1.16/0.49 % (1241127)Instructions burned: 16 (million)
% 1.16/0.49 % (1241109)Instruction limit reached!
% 1.16/0.49 % (1241109)------------------------------
% 1.16/0.49 % (1241109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241109)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241109)Termination reason: Instruction limit
% 1.16/0.49 % (1241109)Termination phase: Property scanning
% 1.16/0.49 % (1241109)Time elapsed: 0.036 s
% 1.16/0.49 % (1241109)Peak memory usage: 11 MB
% 1.16/0.49 % (1241109)Instructions burned: 87 (million)
% 1.16/0.49 % (1241125)Instruction limit reached!
% 1.16/0.49 % (1241125)------------------------------
% 1.16/0.49 % (1241125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241125)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241125)Termination reason: Instruction limit
% 1.16/0.49 % (1241125)Termination phase: Property scanning
% 1.16/0.49 % (1241125)Time elapsed: 0.012 s
% 1.16/0.49 % (1241125)Peak memory usage: 10 MB
% 1.16/0.49 % (1241125)Instructions burned: 27 (million)
% 1.16/0.49 % (1241132)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=888249509:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.16/0.49 % (1241132)Instruction limit reached!
% 1.16/0.49 % (1241132)------------------------------
% 1.16/0.49 % (1241132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241132)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241132)Termination reason: Instruction limit
% 1.16/0.49 % (1241132)Termination phase: Property scanning
% 1.16/0.49 % (1241132)Time elapsed: 0.007 s
% 1.16/0.49 % (1241132)Peak memory usage: 10 MB
% 1.16/0.49 % (1241132)Instructions burned: 16 (million)
% 1.16/0.49 % (1241140)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=143030311: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)
% 1.16/0.49 % (1241142)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1823012062:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.16/0.49 % (1241144)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1926084709:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.16/0.49 % (1241140)Instruction limit reached!
% 1.16/0.49 % (1241140)------------------------------
% 1.16/0.49 % (1241140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241140)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241140)Termination reason: Instruction limit
% 1.16/0.49 % (1241140)Termination phase: shuffling
% 1.16/0.49 % (1241140)Time elapsed: 0.002 s
% 1.16/0.49 % (1241140)Peak memory usage: 10 MB
% 1.16/0.49 % (1241140)Instructions burned: 4 (million)
% 1.16/0.49 % (1241146)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3528044792:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.16/0.49 % (1241144)Instruction limit reached!
% 1.16/0.49 % (1241144)------------------------------
% 1.16/0.49 % (1241144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241144)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241142)Instruction limit reached!
% 1.16/0.49 % (1241142)------------------------------
% 1.16/0.49 % (1241142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241144)Termination reason: Instruction limit
% 1.16/0.49 % (1241144)Termination phase: Property scanning
% 1.16/0.49 % (1241144)Time elapsed: 0.011 s
% 1.16/0.49 % (1241144)Peak memory usage: 10 MB
% 1.16/0.49 % (1241142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241144)Instructions burned: 24 (million)
% 1.16/0.49 % (1241142)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241142)Termination reason: Instruction limit
% 1.16/0.49 % (1241142)Termination phase: shuffling
% 1.16/0.49 % (1241142)Time elapsed: 0.012 s
% 1.16/0.49 % (1241142)Peak memory usage: 10 MB
% 1.16/0.49 % (1241142)Instructions burned: 26 (million)
% 1.16/0.49 % (1241153)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
% 1.16/0.49 % (1241153)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.16/0.49 % (1241153)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=2932572242:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.16/0.49 % (1241131) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1241081-1241131"...
% 1.16/0.49 % (1241158)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.16/0.49 % (1241153)Instruction limit reached!
% 1.16/0.49 % (1241153)------------------------------
% 1.16/0.49 % (1241153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241153)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241153)Termination reason: Instruction limit
% 1.16/0.49 % (1241153)Termination phase: shuffling
% 1.16/0.49 % (1241153)Time elapsed: 0.006 s
% 1.16/0.49 % (1241153)Peak memory usage: 10 MB
% 1.16/0.49 % (1241153)Instructions burned: 14 (million)
% 1.16/0.49 % (1241131)...printing done.
% 1.16/0.49 % (1241131)Refutation found. Thanks to Tanya!
% 1.16/0.49 % SZS status Theorem for theBenchmark
% 1.16/0.49 % SZS output start Proof for theBenchmark
% See solution above
% 1.16/0.49 % (1241131)------------------------------
% 1.16/0.49 % (1241131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.16/0.49 % (1241131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.16/0.49 % (1241131)CaDiCaL version: 2.1.3
% 1.16/0.49 % (1241131)Termination reason: Refutation
% 1.16/0.49 % (1241131)Time elapsed: 0.057 s
% 1.16/0.49 % (1241131)Peak memory usage: 14 MB
% 1.16/0.49 % (1241131)Instructions burned: 221 (million)
% 1.16/0.49 % (1241081)Success in time 0.2 s
% 1.16/0.49 % Vampire exiting
%------------------------------------------------------------------------------