%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP156^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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:10:55 AM UTC 2026
% Result : Theorem 0.68s 0.38s
% Output : Refutation 0.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 45 ( 30 unt; 0 typ; 0 def)
% Number of atoms : 112 ( 65 equ; 0 cnn)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 294 ( 21 ~; 12 |; 3 &; 252 @)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Number of types : 33 ( 32 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 176 ( 173 usr; 23 con; 0-4 aty)
% Number of variables : 18 ( 0 ^; 18 !; 0 ?; 18 :)
% 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,
vAND: $o > $o > $o ).
thf(func_def_101,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_102,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_103,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_104,type,
vOR: $o > $o > $o ).
thf(func_def_105,type,
vIMP: $o > $o > $o ).
thf(func_def_106,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_107,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_108,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_109,type,
db4:
!>[X0: $tType] : X0 ).
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: ( product_prod_a_a > $o ) > ( product_prod_a_a > $o ) > product_prod_a_a ).
thf(func_def_114,type,
sK4: set_Pr1741234931a_real > product_prod_a_real ).
thf(func_def_115,type,
sK5: set_Pr1741234931a_real > product_prod_a_real ).
thf(func_def_116,type,
sK6: set_Pr1741234931a_real > real ).
thf(func_def_117,type,
sK7: set_Pr1741234931a_real > real ).
thf(func_def_118,type,
sK8: set_Pr1948701895od_a_a > product_prod_a_a ).
thf(func_def_119,type,
sK9: set_Pr1948701895od_a_a > product_prod_a_a ).
thf(func_def_120,type,
sK10: set_Pr1948701895od_a_a > real ).
thf(func_def_121,type,
sK11: set_Pr1948701895od_a_a > real ).
thf(func_def_122,type,
sK12: set_Pr147102617l_real > real ).
thf(func_def_123,type,
sK13: set_Pr147102617l_real > real ).
thf(func_def_124,type,
sK14: set_Pr147102617l_real > real ).
thf(func_def_125,type,
sK15: set_Pr147102617l_real > real ).
thf(func_def_126,type,
sK16: set_Product_prod_a_a > a ).
thf(func_def_127,type,
sK17: set_Product_prod_a_a > a ).
thf(func_def_128,type,
sK18: set_Product_prod_a_a > real ).
thf(func_def_129,type,
sK19: set_Product_prod_a_a > real ).
thf(func_def_130,type,
sK20: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a > product_prod_a_a ).
thf(func_def_131,type,
sK21: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a > product_prod_a_a ).
thf(func_def_132,type,
sK22: set_a > set_a > a > a ).
thf(func_def_133,type,
sK23: set_a > set_a > a > a ).
thf(func_def_134,type,
sK24: set_real > set_real > real > real ).
thf(func_def_135,type,
sK25: set_real > set_real > real > real ).
thf(func_def_136,type,
sK26: ( product_prod_a_a > $o ) > a ).
thf(func_def_137,type,
sK27: ( product_prod_a_a > $o ) > a ).
thf(func_def_138,type,
sK28: product_prod_a_a > a ).
thf(func_def_139,type,
sK29: product_prod_a_a > a ).
thf(func_def_140,type,
sK30: ( product_prod_a_a > $o ) > a ).
thf(func_def_141,type,
sK31: ( product_prod_a_a > $o ) > a ).
thf(func_def_142,type,
sK32: product_prod_a_a > a ).
thf(func_def_143,type,
sK33: product_prod_a_a > a ).
thf(func_def_144,type,
sK34: set_Pr147102617l_real > real ).
thf(func_def_145,type,
sK35: set_Pr147102617l_real > real ).
thf(func_def_146,type,
sK36: set_Pr147102617l_real > real ).
thf(func_def_147,type,
sK37: set_Pr147102617l_real > real ).
thf(func_def_148,type,
sK38: set_Product_prod_a_a > a ).
thf(func_def_149,type,
sK39: set_Product_prod_a_a > a ).
thf(func_def_150,type,
sK40: set_Product_prod_a_a > real ).
thf(func_def_151,type,
sK41: set_Product_prod_a_a > real ).
thf(func_def_152,type,
sK42: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_153,type,
sK43: real > real > real ).
thf(func_def_154,type,
sK44: ( real > real ) > real ).
thf(func_def_155,type,
sK45: ( real > real ) > real ).
thf(func_def_156,type,
sK46: ( real > real ) > real ).
thf(func_def_157,type,
sK47: ( real > real ) > real ).
thf(func_def_158,type,
sK48: ( real > real ) > real ).
thf(func_def_159,type,
sK49: ( real > real ) > real ).
thf(func_def_160,type,
sK50: ( real > real ) > real ).
thf(func_def_161,type,
sK51: ( real > real ) > real ).
thf(func_def_162,type,
vNOT: $o > $o ).
thf(func_def_163,type,
sK52: set_Product_prod_a_a > a ).
thf(func_def_164,type,
sK53: set_Product_prod_a_a > a ).
thf(func_def_165,type,
sK54: set_Product_prod_a_a > real ).
thf(func_def_166,type,
sK55: set_Product_prod_a_a > real ).
thf(func_def_167,type,
sK56: set_Pr147102617l_real > real ).
thf(func_def_168,type,
sK57: set_Pr147102617l_real > real ).
thf(func_def_169,type,
sK58: set_Pr147102617l_real > real ).
thf(func_def_170,type,
sK59: set_Pr147102617l_real > real ).
thf(func_def_171,type,
sK60: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_172,type,
sK61: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_173,type,
sK62: set_Product_prod_a_a > set_Product_prod_a_a > product_prod_a_a ).
thf(func_def_174,type,
sK63: 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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',fact_7_u__0) ).
thf(f10,axiom,
( ( plus_plus_real @ u @ v )
= one_one_real ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_assms_I5_J) ).
thf(f83,axiom,
! [X0: real,X1: real] :
( ( ( plus_plus_real @ X0 @ X1 )
= X0 )
= ( X1 = zero_zero_real ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_82_add__cancel__left__right) ).
thf(f97,axiom,
! [X0: a] :
( ( plus_plus_a @ X0 @ zero_zero_a )
= X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_add_Oright__neutral) ).
thf(f239,axiom,
! [X0: a] :
( ( real_V1035702895aleR_a @ zero_zero_real @ X0 )
= zero_zero_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_238_scale__zero__left) ).
thf(f242,axiom,
! [X0: a] :
( ( real_V1035702895aleR_a @ one_one_real @ X0 )
= X0 ),
file('/export/starexec/sandbox2/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/sandbox2/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(f366,plain,
member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation,
inference(rectify,[],[f6]) ).
thf(f367,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation )
= $true ),
inference(fool_elimination,[],[f366]) ).
thf(f368,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(f369,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,[],[f368]) ).
thf(f370,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(f371,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,[],[f370]) ).
thf(f422,plain,
! [X0: real,X1: real] :
( ( ( plus_plus_real @ X0 @ X1 )
= X0 )
= ( zero_zero_real = X1 ) ),
inference(fool_elimination,[],[f83]) ).
thf(f706,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(f707,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,[],[f706]) ).
thf(f718,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,[],[f707]) ).
thf(f727,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,[],[f369]) ).
thf(f728,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(flattening,[],[f727]) ).
thf(f729,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,[],[f371]) ).
thf(f984,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation )
= $true ),
inference(cnf_transformation,[],[f367]) ).
thf(f985,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(cnf_transformation,[],[f728]) ).
thf(f986,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,[],[f729]) ).
thf(f988,plain,
( one_one_real
= ( plus_plus_real @ u @ v ) ),
inference(cnf_transformation,[],[f10]) ).
thf(f1061,plain,
! [X0: real,X1: real] :
( ( ( plus_plus_real @ X0 @ X1 )
= X0 )
= ( zero_zero_real = X1 ) ),
inference(cnf_transformation,[],[f422]) ).
thf(f1075,plain,
! [X0: a] :
( ( plus_plus_a @ X0 @ zero_zero_a )
= X0 ),
inference(cnf_transformation,[],[f97]) ).
thf(f1240,plain,
! [X0: a] :
( zero_zero_a
= ( real_V1035702895aleR_a @ zero_zero_real @ X0 ) ),
inference(cnf_transformation,[],[f239]) ).
thf(f1243,plain,
! [X0: a] :
( ( real_V1035702895aleR_a @ one_one_real @ X0 )
= X0 ),
inference(cnf_transformation,[],[f242]) ).
thf(f1384,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,[],[f718]) ).
thf(f2112,plain,
! [X0: real,X1: real] :
( ( ( ( plus_plus_real @ X0 @ X1 )
= X0 )
= $false )
| ( $true
= ( zero_zero_real = X1 ) ) ),
inference(iff_proxy_clausification,[],[f1061]) ).
thf(f2113,plain,
! [X0: real,X1: real] :
( ( ( plus_plus_real @ X0 @ X1 )
!= X0 )
| ( $true
= ( zero_zero_real = X1 ) ) ),
inference(equality_proxy_clausification,[],[f2112]) ).
thf(f2114,plain,
! [X0: real,X1: real] :
( ( ( plus_plus_real @ X0 @ X1 )
!= X0 )
| ( zero_zero_real = X1 ) ),
inference(equality_proxy_clausification,[],[f2113]) ).
thf(f2360,plain,
u = one_one_real,
inference(global_subsumption,[],[f985,f986,f1384]) ).
thf(f2361,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 ) ),
inference(constrained_superposition,[],[f1384,f2360]) ).
thf(f2436,plain,
( one_one_real
= ( plus_plus_real @ one_one_real @ v ) ),
inference(forward_demodulation,[],[f988,f2360]) ).
thf(f2439,plain,
( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ x @ ( real_V1035702895aleR_a @ v @ y ) ) @ y ) @ relation ) ),
inference(constrained_superposition,[],[f2361,f1243]) ).
thf(f3297,plain,
( ( one_one_real != one_one_real )
| ( zero_zero_real = v ) ),
inference(constrained_superposition,[],[f2114,f2436]) ).
thf(f3299,plain,
zero_zero_real = v,
inference(trivial_inequality_removal,[],[f3297]) ).
thf(f3313,plain,
( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ x @ ( real_V1035702895aleR_a @ zero_zero_real @ y ) ) @ y ) @ relation ) ),
inference(constrained_superposition,[],[f2439,f3299]) ).
thf(f3353,plain,
( $true
!= ( member449909584od_a_a @ ( product_Pair_a_a @ ( plus_plus_a @ x @ zero_zero_a ) @ y ) @ relation ) ),
inference(forward_demodulation,[],[f3313,f1240]) ).
thf(f3358,plain,
( ( member449909584od_a_a @ ( product_Pair_a_a @ x @ y ) @ relation )
!= $true ),
inference(forward_demodulation,[],[f3353,f1075]) ).
thf(f3363,plain,
$false,
inference(global_subsumption,[],[f3358,f984]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP156^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n005.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 20:02:31 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.68/0.38 % (2137297)Will run a generic schedule for satisfiability detection.
% 0.68/0.38 % (2137307)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1436184405:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.68/0.38 % (2137303)% WARNING: option uhcvi not known.
% 0.68/0.38 % (2137306)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=691075543:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.68/0.38 % (2137302)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=621658455_2999 on theBenchmark for (2999ds/0Mi)
% 0.68/0.38 % (2137304)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2443847340:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.68/0.38 % (2137305)dis+10_1_sil=32000:sp=arity:random_seed=425648295:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.68/0.38 % (2137303)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3375625339:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.68/0.38 % (2137308)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2562845950:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.68/0.38 % (2137306)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.68/0.38 % (2137303)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.68/0.38 % (2137307)Instruction limit reached!
% 0.68/0.38 % (2137307)------------------------------
% 0.68/0.38 % (2137307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.38 % (2137307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.38 % (2137307)CaDiCaL version: 2.1.3
% 0.68/0.38 % (2137307)Termination reason: Instruction limit
% 0.68/0.38 % (2137307)Termination phase: Saturation
% 0.68/0.38 % (2137307)Time elapsed: 0.031 s
% 0.68/0.38 % (2137307)Peak memory usage: 13 MB
% 0.68/0.38 % (2137307)Instructions burned: 134 (million)
% 0.68/0.38 % Exception at run slice level
% 0.68/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.68/0.38 % (2137303)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.68/0.38 % (2137316)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=236915189:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.68/0.38 % (2137305)Instruction limit reached!
% 0.68/0.38 % (2137305)------------------------------
% 0.68/0.38 % (2137305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.38 % (2137305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.38 % (2137305)CaDiCaL version: 2.1.3
% 0.68/0.38 % (2137305)Termination reason: Instruction limit
% 0.68/0.38 % (2137305)Termination phase: Saturation
% 0.68/0.38 % (2137305)Time elapsed: 0.043 s
% 0.68/0.38 % (2137305)Peak memory usage: 12 MB
% 0.68/0.38 % (2137305)Instructions burned: 104 (million)
% 0.68/0.38 % (2137306)Instruction limit reached!
% 0.68/0.38 % (2137306)------------------------------
% 0.68/0.38 % (2137306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.38 % (2137306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.38 % (2137306)CaDiCaL version: 2.1.3
% 0.68/0.38 % (2137306)Termination reason: Instruction limit
% 0.68/0.38 % (2137306)Termination phase: Saturation
% 0.68/0.38 % (2137306)Time elapsed: 0.049 s
% 0.68/0.38 % (2137306)Peak memory usage: 12 MB
% 0.68/0.38 % (2137306)Instructions burned: 117 (million)
% 0.68/0.38 % Exception at run slice level
% 0.68/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.68/0.38 % (2137318)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2408528979:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.68/0.38 % (2137319)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2637997350:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.68/0.38 % (2137322)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3344549782:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.68/0.38 % (2137319)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.68/0.38 % (2137320)ott-21_1_sil=16000:fs=off:random_seed=1654245849:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.68/0.38 % (2137304) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2137297-2137304"...
% 0.68/0.38 % (2137304)...printing done.
% 0.68/0.38 % (2137304)Refutation found. Thanks to Tanya!
% 0.68/0.38 % SZS status Theorem for theBenchmark
% 0.68/0.38 % SZS output start Proof for theBenchmark
% See solution above
% 0.68/0.38 % (2137304)------------------------------
% 0.68/0.38 % (2137304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.68/0.38 % (2137304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.68/0.38 % (2137304)CaDiCaL version: 2.1.3
% 0.68/0.38 % (2137304)Termination reason: Refutation
% 0.68/0.38 % (2137304)Time elapsed: 0.095 s
% 0.68/0.38 % (2137304)Peak memory usage: 14 MB
% 0.68/0.38 % (2137304)Instructions burned: 202 (million)
% 0.68/0.38 % (2137297)Success in time 0.144 s
% 0.68/0.38 % Vampire exiting
%------------------------------------------------------------------------------