%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP065^1 : TPTP v9.2.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 08:55:16 AM UTC 2026
% Result : Theorem 0.32s 1.33s
% Output : Refutation 0.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 2
% Syntax : Number of formulae : 13 ( 13 unt; 0 typ; 0 def)
% Number of atoms : 31 ( 14 equ; 0 cnn)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 15 ( 8 ~; 0 |; 0 &; 7 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 2 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 19 ( 16 usr; 3 con; 0-3 aty)
% Number of variables : 4 ( 4 ^; 0 !; 0 ?; 4 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
tree_b: $tType ).
thf(type_def_7,type,
b: $tType ).
thf(func_def_0,type,
tree_b: $tType ).
thf(func_def_1,type,
b: $tType ).
thf(func_def_2,type,
heapIm229596387mpty_b: tree_b > $o ).
thf(func_def_3,type,
heapIm1140443834left_b: tree_b > tree_b ).
thf(func_def_4,type,
heapIm1257206335ight_b: tree_b > tree_b ).
thf(func_def_5,type,
e_b: tree_b ).
thf(func_def_6,type,
t_b: b > tree_b > tree_b > tree_b ).
thf(func_def_7,type,
pred_Tree_b: ( b > $o ) > tree_b > $o ).
thf(func_def_8,type,
in_tree_b: b > tree_b > $o ).
thf(func_def_9,type,
val_b: tree_b > b ).
thf(func_def_10,type,
ord_less_eq_Tree_b_o: ( tree_b > $o ) > ( tree_b > $o ) > $o ).
thf(func_def_11,type,
ord_less_eq_b_o: ( b > $o ) > ( b > $o ) > $o ).
thf(func_def_20,type,
sK0: ( tree_b > $o ) > tree_b ).
thf(func_def_21,type,
sK1: ( tree_b > $o ) > b ).
thf(func_def_22,type,
sK2: ( tree_b > $o ) > tree_b ).
thf(func_def_23,type,
sK3: tree_b > b ).
thf(func_def_24,type,
sK4: tree_b > tree_b ).
thf(func_def_25,type,
sK5: tree_b > tree_b ).
thf(f68,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f67]) ).
thf(f67,plain,
$true != $true,
inference(boolean_simplification,[status(thm)],[f66]) ).
thf(f66,plain,
( ( e_b = e_b )
!= $true ),
inference(beta_eta_normalization,[status(thm)],[f65]) ).
thf(f65,plain,
( ( ^ [Y0: tree_b] : ( e_b = Y0 )
@ e_b )
!= $true ),
inference(definition_unfolding,[status(thm)],[f61,f63]) ).
thf(f63,plain,
( heapIm229596387mpty_b
= ( ^ [Y0: tree_b] : ( e_b = Y0 ) ) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
thf(f31,plain,
( heapIm229596387mpty_b
= ( ^ [Y0: tree_b] : ( e_b = Y0 ) ) ),
inference(fool_elimination,[status(thm)],[f1]) ).
thf(f1,axiom,
( ( ^ [X0: tree_b] : ( e_b = X0 ) )
= heapIm229596387mpty_b ),
file('/export/starexec/sandbox/tmp/tmp.GJjXH3hXcY/DTF2THF_5122.p',fact_0_hs__is__empty__def) ).
thf(f61,plain,
( ( heapIm229596387mpty_b @ e_b )
!= $true ),
inference(cnf_transformation,[status(thm)],[f40]) ).
thf(f40,plain,
( ( heapIm229596387mpty_b @ e_b )
!= $true ),
inference(flattening,[status(thm)],[f33]) ).
thf(f33,plain,
( ( heapIm229596387mpty_b @ e_b )
!= $true ),
inference(fool_elimination,[status(thm)],[f32]) ).
thf(f32,plain,
~ ( heapIm229596387mpty_b @ e_b ),
inference(rectify,[status(thm)],[f15]) ).
thf(f15,negated_conjecture,
~ ( heapIm229596387mpty_b @ e_b ),
inference(negated_conjecture,[status(cth)],[f14]) ).
thf(f14,conjecture,
heapIm229596387mpty_b @ e_b,
file('/export/starexec/sandbox/tmp/tmp.GJjXH3hXcY/DTF2THF_5122.p',conj_0) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP065^1 : TPTP v9.2.1. Released v7.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.34 % Computer : n017.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue Feb 24 08:23:56 EST 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.20/0.47 ---- Original DTF file ---
% 0.32/0.47 thf(spec,logic,$$dhol).
% 0.32/0.47 %------------------------------------------------------------------------------
% 0.32/0.47 % File : ITP065^1 : TPTP v9.2.1. Released v7.5.0.
% 0.32/0.47 % Domain : Interactive Theorem Proving
% 0.32/0.47 % Problem : Sledgehammer HeapImperative problem prob_1087__5351268_1
% 0.32/0.47 % Version : Especial.
% 0.32/0.47 % English :
% 0.32/0.47
% 0.32/0.47 % Refs : [BH+15] Blanchette et al. (2015), Mining the Archive of Formal
% 0.32/0.47 % : [Des21] Desharnais (2021), Email to Geoff Sutcliffe
% 0.32/0.47 % Source : [Des21]
% 0.32/0.47 % Names : HeapImperative/prob_1087__5351268_1 [Des21]
% 0.32/0.47
% 0.32/0.47 % Status : Theorem
% 0.32/0.47 % Rating : 0.11 v9.1.0, 0.12 v9.0.0, 0.30 v8.2.0, 0.15 v8.1.0, 0.18 v7.5.0
% 0.32/0.47 % Syntax : Number of formulae : 26 ( 11 unt; 12 typ; 0 def)
% 0.32/0.47 % Number of atoms : 30 ( 16 equ; 0 cnn)
% 0.32/0.47 % Maximal formula atoms : 4 ( 2 avg)
% 0.32/0.47 % Number of connectives : 79 ( 5 ~; 2 |; 4 &; 62 @)
% 0.32/0.47 % ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% 0.32/0.47 % Maximal formula depth : 14 ( 5 avg)
% 0.32/0.47 % Number of types : 3 ( 2 usr)
% 0.32/0.47 % Number of type conns : 25 ( 25 >; 0 *; 0 +; 0 <<)
% 0.32/0.47 % Number of symbols : 11 ( 10 usr; 1 con; 0-3 aty)
% 0.32/0.47 % Number of variables : 40 ( 1 ^; 39 !; 0 ?; 40 :)
% 0.32/0.47 % SPC : TH0_THM_EQU_NAR
% 0.32/0.47
% 0.32/0.47 % Comments : This file was generated by Sledgehammer 2021-02-23 15:31:56.775
% 0.32/0.47 %------------------------------------------------------------------------------
% 0.32/0.47 % Could-be-implicit typings (2)
% 0.32/0.47 thf(ty_n_t__Heap__OTree_Itf__b_J,type,
% 0.32/0.47 tree_b: $tType ).
% 0.32/0.47
% 0.32/0.47 thf(ty_n_tf__b,type,
% 0.32/0.47 b: $tType ).
% 0.32/0.47
% 0.32/0.47 % Explicit typings (10)
% 0.32/0.47 thf(sy_c_HeapImperative__Mirabelle__ksbqzsoydx_Ohs__is__empty_001tf__b,type,
% 0.32/0.47 heapIm229596387mpty_b: tree_b > $o ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_HeapImperative__Mirabelle__ksbqzsoydx_Oleft_001tf__b,type,
% 0.32/0.47 heapIm1140443834left_b: tree_b > tree_b ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_HeapImperative__Mirabelle__ksbqzsoydx_Oright_001tf__b,type,
% 0.32/0.47 heapIm1257206335ight_b: tree_b > tree_b ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_Heap_OTree_OE_001tf__b,type,
% 0.32/0.47 e_b: tree_b ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_Heap_OTree_OT_001tf__b,type,
% 0.32/0.47 t_b: b > tree_b > tree_b > tree_b ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_Heap_OTree_Opred__Tree_001tf__b,type,
% 0.32/0.47 pred_Tree_b: ( b > $o ) > tree_b > $o ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_Heap_Oin__tree_001tf__b,type,
% 0.32/0.47 in_tree_b: b > tree_b > $o ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_Heap_Oval_001tf__b,type,
% 0.32/0.47 val_b: tree_b > b ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_Orderings_Oord__class_Oless__eq_001_062_It__Heap__OTree_Itf__b_J_M_Eo_J,type,
% 0.32/0.47 ord_less_eq_Tree_b_o: ( tree_b > $o ) > ( tree_b > $o ) > $o ).
% 0.32/0.47
% 0.32/0.47 thf(sy_c_Orderings_Oord__class_Oless__eq_001_062_Itf__b_M_Eo_J,type,
% 0.32/0.47 ord_less_eq_b_o: ( b > $o ) > ( b > $o ) > $o ).
% 0.32/0.47
% 0.32/0.47 % Relevant facts (13)
% 0.32/0.47 thf(fact_0_hs__is__empty__def,axiom,
% 0.32/0.47 ( heapIm229596387mpty_b
% 0.32/0.47 = ( ^ [T: tree_b] : ( T = e_b ) ) ) ).
% 0.32/0.47
% 0.32/0.47 % hs_is_empty_def
% 0.32/0.47 thf(fact_1_in__tree_Osimps_I1_J,axiom,
% 0.32/0.47 ! [V: b] :
% 0.32/0.47 ~ ( in_tree_b @ V @ e_b ) ).
% 0.32/0.47
% 0.32/0.47 % in_tree.simps(1)
% 0.32/0.47 thf(fact_2_Tree_Opred__inject_I1_J,axiom,
% 0.32/0.47 ! [P: b > $o] : ( pred_Tree_b @ P @ e_b ) ).
% 0.32/0.47
% 0.32/0.47 % Tree.pred_inject(1)
% 0.32/0.47 thf(fact_3_Tree_Oinject,axiom,
% 0.32/0.47 ! [X21: b,X22: tree_b,X23: tree_b,Y21: b,Y22: tree_b,Y23: tree_b] :
% 0.32/0.47 ( ( ( t_b @ X21 @ X22 @ X23 )
% 0.32/0.47 = ( t_b @ Y21 @ Y22 @ Y23 ) )
% 0.32/0.47 = ( ( X21 = Y21 )
% 0.32/0.47 & ( X22 = Y22 )
% 0.32/0.47 & ( X23 = Y23 ) ) ) ).
% 0.32/0.47
% 0.32/0.47 % Tree.inject
% 0.32/0.47 thf(fact_4_Tree_Opred__inject_I2_J,axiom,
% 0.32/0.47 ! [P: b > $o,A: b,Aa: tree_b,Ab: tree_b] :
% 0.32/0.47 ( ( pred_Tree_b @ P @ ( t_b @ A @ Aa @ Ab ) )
% 0.32/0.47 = ( ( P @ A )
% 0.32/0.47 & ( pred_Tree_b @ P @ Aa )
% 0.32/0.47 & ( pred_Tree_b @ P @ Ab ) ) ) ).
% 0.32/0.47
% 0.32/0.47 % Tree.pred_inject(2)
% 0.32/0.47 thf(fact_5_in__tree_Osimps_I2_J,axiom,
% 0.32/0.47 ! [V: b,V2: b,L: tree_b,R: tree_b] :
% 0.32/0.47 ( ( in_tree_b @ V @ ( t_b @ V2 @ L @ R ) )
% 0.32/0.47 = ( ( V = V2 )
% 0.32/0.47 | ( in_tree_b @ V @ L )
% 0.32/0.47 | ( in_tree_b @ V @ R ) ) ) ).
% 0.32/0.47
% 0.32/0.47 % in_tree.simps(2)
% 0.32/0.47 thf(fact_6_Tree_Oexhaust,axiom,
% 0.32/0.47 ! [Y: tree_b] :
% 0.32/0.47 ( ( Y != e_b )
% 0.32/0.47 => ~ ! [X212: b,X222: tree_b,X232: tree_b] :
% 0.32/0.47 ( Y
% 0.32/0.47 != ( t_b @ X212 @ X222 @ X232 ) ) ) ).
% 0.32/0.47
% 0.32/0.47 % Tree.exhaust
% 0.32/0.47 thf(fact_7_Tree_Oinduct,axiom,
% 0.32/0.47 ! [P: tree_b > $o,Tree: tree_b] :
% 0.32/0.47 ( ( P @ e_b )
% 0.32/0.47 => ( ! [X1: b,X2: tree_b,X3: tree_b] :
% 0.32/0.47 ( ( P @ X2 )
% 0.32/0.47 => ( ( P @ X3 )
% 0.32/0.47 => ( P @ ( t_b @ X1 @ X2 @ X3 ) ) ) )
% 0.32/0.47 => ( P @ Tree ) ) ) ).
% 0.32/0.47
% 0.32/0.47 % Tree.induct
% 0.32/0.47 thf(fact_8_Tree_Odistinct_I1_J,axiom,
% 0.32/0.47 ! [X21: b,X22: tree_b,X23: tree_b] :
% 0.32/0.47 ( e_b
% 0.32/0.47 != ( t_b @ X21 @ X22 @ X23 ) ) ).
% 0.32/0.47
% 0.32/0.47 % Tree.distinct(1)
% 0.32/0.47 thf(fact_9_left_Osimps,axiom,
% 0.32/0.47 ! [V: b,L: tree_b,R: tree_b] :
% 0.32/0.47 ( ( heapIm1140443834left_b @ ( t_b @ V @ L @ R ) )
% 0.32/0.47 = L ) ).
% 0.32/0.47
% 0.32/0.47 % left.simps
% 0.32/0.47 thf(fact_10_right_Osimps,axiom,
% 0.32/0.47 ! [V: b,L: tree_b,R: tree_b] :
% 0.32/0.47 ( ( heapIm1257206335ight_b @ ( t_b @ V @ L @ R ) )
% 0.32/0.47 = R ) ).
% 0.32/0.47
% 0.32/0.47 % right.simps
% 0.32/0.47 thf(fact_11_Tree_Opred__mono,axiom,
% 0.32/0.47 ! [P: b > $o,Pa: b > $o] :
% 0.32/0.47 ( ( ord_less_eq_b_o @ P @ Pa )
% 0.32/0.47 => ( ord_less_eq_Tree_b_o @ ( pred_Tree_b @ P ) @ ( pred_Tree_b @ Pa ) ) ) ).
% 0.32/0.47
% 0.32/0.47 % Tree.pred_mono
% 0.32/0.47 thf(fact_12_val_Osimps,axiom,
% 0.32/0.47 ! [V: b,Uu: tree_b,Uv: tree_b] :
% 0.32/0.47 ( ( val_b @ ( t_b @ V @ Uu @ Uv ) )
% 0.32/0.47 = V ) ).
% 0.32/0.47
% 0.32/0.47 % val.simps
% 0.32/0.47
% 0.32/0.47 % Conjectures (1)
% 0.32/0.47 thf(conj_0,conjecture,
% 0.32/0.47 heapIm229596387mpty_b @ e_b ).
% 0.32/0.47
% 0.32/0.47 %------------------------------------------------------------------------------
% 0.32/0.47 ------------------------
% 0.32/1.30 ---- Embedded in THF ---
% 0.32/1.30 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 0.32/1.30 %%% Generated on Tue Feb 24 08:23:57 EST 2026
% 0.32/1.30 %%% using '$$dhol' embedding, version 1.3.0.
% 0.32/1.30 %%% Logic specification used:
% 0.32/1.30 %%% thf(spec, logic, $$dhol).
% 0.32/1.30
% 0.32/1.30 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.GJjXH3hXcY/DTF2DTF5122.p
% See solution above
% 0.32/1.30 ------------------------
% 0.32/1.31 ---- Cleaned THF ---
% 0.32/1.31 thf(ty_n_t__Heap__OTree_Itf__b_J,type,
% 0.32/1.31 tree_b: $tType ).
% 0.32/1.31
% 0.32/1.31 thf(ty_n_tf__b,type,
% 0.32/1.31 b: $tType ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_HeapImperative__Mirabelle__ksbqzsoydx_Ohs__is__empty_001tf__b,type,
% 0.32/1.31 heapIm229596387mpty_b: tree_b > $o ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_HeapImperative__Mirabelle__ksbqzsoydx_Oleft_001tf__b,type,
% 0.32/1.31 heapIm1140443834left_b: tree_b > tree_b ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_HeapImperative__Mirabelle__ksbqzsoydx_Oright_001tf__b,type,
% 0.32/1.31 heapIm1257206335ight_b: tree_b > tree_b ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_Heap_OTree_OE_001tf__b,type,
% 0.32/1.31 e_b: tree_b ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_Heap_OTree_OT_001tf__b,type,
% 0.32/1.31 t_b: b > tree_b > tree_b > tree_b ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_Heap_OTree_Opred__Tree_001tf__b,type,
% 0.32/1.31 pred_Tree_b: ( b > $o ) > tree_b > $o ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_Heap_Oin__tree_001tf__b,type,
% 0.32/1.31 in_tree_b: b > tree_b > $o ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_Heap_Oval_001tf__b,type,
% 0.32/1.31 val_b: tree_b > b ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_Orderings_Oord__class_Oless__eq_001_062_It__Heap__OTree_Itf__b_J_M_Eo_J,type,
% 0.32/1.31 ord_less_eq_Tree_b_o: ( tree_b > $o ) > ( tree_b > $o ) > $o ).
% 0.32/1.31
% 0.32/1.31 thf(sy_c_Orderings_Oord__class_Oless__eq_001_062_Itf__b_M_Eo_J,type,
% 0.32/1.31 ord_less_eq_b_o: ( b > $o ) > ( b > $o ) > $o ).
% 0.32/1.31
% 0.32/1.31 thf(fact_0_hs__is__empty__def,axiom,
% 0.32/1.31 ( heapIm229596387mpty_b
% 0.32/1.31 = ( ^ [T: tree_b] : ( T = e_b ) ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_1_in__tree_Osimps_I1_J,axiom,
% 0.32/1.31 ! [V: b] :
% 0.32/1.31 ~ ( in_tree_b @ V @ e_b ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_2_Tree_Opred__inject_I1_J,axiom,
% 0.32/1.31 ! [P: b > $o] : ( pred_Tree_b @ P @ e_b ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_3_Tree_Oinject,axiom,
% 0.32/1.31 ! [X21: b,X22: tree_b,X23: tree_b,Y21: b,Y22: tree_b,Y23: tree_b] :
% 0.32/1.31 ( ( ( t_b @ X21 @ X22 @ X23 )
% 0.32/1.31 = ( t_b @ Y21 @ Y22 @ Y23 ) )
% 0.32/1.31 = ( ( X21 = Y21 )
% 0.32/1.31 & ( X22 = Y22 )
% 0.32/1.31 & ( X23 = Y23 ) ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_4_Tree_Opred__inject_I2_J,axiom,
% 0.32/1.31 ! [P: b > $o,A: b,Aa: tree_b,Ab: tree_b] :
% 0.32/1.31 ( ( pred_Tree_b @ P @ ( t_b @ A @ Aa @ Ab ) )
% 0.32/1.31 = ( ( P @ A )
% 0.32/1.31 & ( pred_Tree_b @ P @ Aa )
% 0.32/1.31 & ( pred_Tree_b @ P @ Ab ) ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_5_in__tree_Osimps_I2_J,axiom,
% 0.32/1.31 ! [V: b,V2: b,L: tree_b,R: tree_b] :
% 0.32/1.31 ( ( in_tree_b @ V @ ( t_b @ V2 @ L @ R ) )
% 0.32/1.31 = ( ( V = V2 )
% 0.32/1.31 | ( in_tree_b @ V @ L )
% 0.32/1.31 | ( in_tree_b @ V @ R ) ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_6_Tree_Oexhaust,axiom,
% 0.32/1.31 ! [Y: tree_b] :
% 0.32/1.31 ( ( Y != e_b )
% 0.32/1.31 => ~ ! [X212: b,X222: tree_b,X232: tree_b] :
% 0.32/1.31 ( Y
% 0.32/1.31 != ( t_b @ X212 @ X222 @ X232 ) ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_7_Tree_Oinduct,axiom,
% 0.32/1.31 ! [P: tree_b > $o,Tree: tree_b] :
% 0.32/1.31 ( ( P @ e_b )
% 0.32/1.31 => ( ! [X1: b,X2: tree_b,X3: tree_b] :
% 0.32/1.31 ( ( P @ X2 )
% 0.32/1.31 => ( ( P @ X3 )
% 0.32/1.31 => ( P @ ( t_b @ X1 @ X2 @ X3 ) ) ) )
% 0.32/1.31 => ( P @ Tree ) ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_8_Tree_Odistinct_I1_J,axiom,
% 0.32/1.31 ! [X21: b,X22: tree_b,X23: tree_b] :
% 0.32/1.31 ( e_b
% 0.32/1.31 != ( t_b @ X21 @ X22 @ X23 ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_9_left_Osimps,axiom,
% 0.32/1.31 ! [V: b,L: tree_b,R: tree_b] :
% 0.32/1.31 ( ( heapIm1140443834left_b @ ( t_b @ V @ L @ R ) )
% 0.32/1.31 = L ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_10_right_Osimps,axiom,
% 0.32/1.31 ! [V: b,L: tree_b,R: tree_b] :
% 0.32/1.31 ( ( heapIm1257206335ight_b @ ( t_b @ V @ L @ R ) )
% 0.32/1.31 = R ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_11_Tree_Opred__mono,axiom,
% 0.32/1.31 ! [P: b > $o,Pa: b > $o] :
% 0.32/1.31 ( ( ord_less_eq_b_o @ P @ Pa )
% 0.32/1.31 => ( ord_less_eq_Tree_b_o @ ( pred_Tree_b @ P ) @ ( pred_Tree_b @ Pa ) ) ) ).
% 0.32/1.31
% 0.32/1.31 thf(fact_12_val_Osimps,axiom,
% 0.32/1.31 ! [V: b,Uu: tree_b,Uv: tree_b] :
% 0.32/1.31 ( ( val_b @ ( t_b @ V @ Uu @ Uv ) )
% 0.32/1.31 = V ) ).
% 0.32/1.31
% 0.32/1.31 thf(conj_0,conjecture,
% 0.32/1.31 heapIm229596387mpty_b @ e_b ).
% 0.32/1.31 ------------------------
% 0.32/1.32 % (5455)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_5122 for (2999ds/275Mi)
% 0.32/1.33 % (5455)Refutation not found, incomplete strategy
% 0.32/1.33 % (5455)------------------------------
% 0.32/1.33 % (5455)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.32/1.33 % (5455)Termination reason: Refutation not found, incomplete strategy
% 0.32/1.33
% 0.32/1.33
% 0.32/1.33 % (5455)Memory used [KB]: 5500
% 0.32/1.33 % (5455)Time elapsed: 0.002 s
% 0.32/1.33 % (5455)Instructions burned: 2 (million)
% 0.32/1.33 % (5455)------------------------------
% 0.32/1.33 % (5455)------------------------------
% 0.32/1.33 % (5450)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_5122 for (2999ds/183Mi)
% 0.32/1.33 % (5451)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_5122 for (2999ds/4Mi)
% 0.32/1.33 % (5452)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_5122 for (2999ds/27Mi)
% 0.32/1.33 % (5453)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_5122 for (2999ds/2Mi)
% 0.32/1.33 % (5454)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_5122 for (2999ds/2Mi)
% 0.32/1.33 % (5456)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_5122 for (2999ds/18Mi)
% 0.32/1.33 % (5453)Instruction limit reached!
% 0.32/1.33 % (5453)------------------------------
% 0.32/1.33 % (5453)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.32/1.33 % (5453)Termination reason: Unknown
% 0.32/1.33 % (5453)Termination phase: Property scanning
% 0.32/1.33
% 0.32/1.33 % (5453)Memory used [KB]: 1023
% 0.32/1.33 % (5453)Time elapsed: 0.003 s
% 0.32/1.33 % (5453)Instructions burned: 2 (million)
% 0.32/1.33 % (5453)------------------------------
% 0.32/1.33 % (5453)------------------------------
% 0.32/1.33 % (5454)Instruction limit reached!
% 0.32/1.33 % (5454)------------------------------
% 0.32/1.33 % (5454)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.32/1.33 % (5454)Termination reason: Unknown
% 0.32/1.33 % (5454)Termination phase: shuffling
% 0.32/1.33
% 0.32/1.33 % (5454)Memory used [KB]: 1023
% 0.32/1.33 % (5454)Time elapsed: 0.003 s
% 0.32/1.33 % (5454)Instructions burned: 2 (million)
% 0.32/1.33 % (5454)------------------------------
% 0.32/1.33 % (5454)------------------------------
% 0.32/1.33 % (5451)Instruction limit reached!
% 0.32/1.33 % (5451)------------------------------
% 0.32/1.33 % (5451)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.32/1.33 % (5451)Termination reason: Unknown
% 0.32/1.33 % (5451)Termination phase: Property scanning
% 0.32/1.33
% 0.32/1.33 % (5451)Memory used [KB]: 1023
% 0.32/1.33 % (5451)Time elapsed: 0.004 s
% 0.32/1.33 % (5451)Instructions burned: 4 (million)
% 0.32/1.33 % (5451)------------------------------
% 0.32/1.33 % (5451)------------------------------
% 0.32/1.33 % (5450)First to succeed.
% 0.32/1.33 % (5452)Also succeeded, but the first one will report.
% 0.32/1.33 % (5450)Refutation found. Thanks to Tanya!
% 0.32/1.33 % SZS status Theorem for DTF2THF_5122
% 0.32/1.33 % SZS output start Proof for DTF2THF_5122
% 0.32/1.33 thf(type_def_5, type, tree_b: $tType).
% 0.32/1.33 thf(type_def_7, type, b: $tType).
% 0.32/1.33 thf(func_def_0, type, tree_b: $tType).
% 0.32/1.33 thf(func_def_1, type, b: $tType).
% 0.32/1.33 thf(func_def_2, type, heapIm229596387mpty_b: tree_b > $o).
% 0.32/1.33 thf(func_def_3, type, heapIm1140443834left_b: tree_b > tree_b).
% 0.32/1.33 thf(func_def_4, type, heapIm1257206335ight_b: tree_b > tree_b).
% 0.32/1.33 thf(func_def_5, type, e_b: tree_b).
% 0.32/1.33 thf(func_def_6, type, t_b: b > tree_b > tree_b > tree_b).
% 0.32/1.33 thf(func_def_7, type, pred_Tree_b: (b > $o) > tree_b > $o).
% 0.32/1.33 thf(func_def_8, type, in_tree_b: b > tree_b > $o).
% 0.32/1.33 thf(func_def_9, type, val_b: tree_b > b).
% 0.32/1.33 thf(func_def_10, type, ord_less_eq_Tree_b_o: (tree_b > $o) > (tree_b > $o) > $o).
% 0.32/1.33 thf(func_def_11, type, ord_less_eq_b_o: (b > $o) > (b > $o) > $o).
% 0.32/1.33 thf(func_def_20, type, sK0: (tree_b > $o) > tree_b).
% 0.32/1.33 thf(func_def_21, type, sK1: (tree_b > $o) > b).
% 0.32/1.33 thf(func_def_22, type, sK2: (tree_b > $o) > tree_b).
% 0.32/1.33 thf(func_def_23, type, sK3: tree_b > b).
% 0.32/1.33 thf(func_def_24, type, sK4: tree_b > tree_b).
% 0.32/1.33 thf(func_def_25, type, sK5: tree_b > tree_b).
% 0.32/1.33 thf(f68,plain,(
% 0.32/1.33 $false),
% 0.32/1.33 inference(trivial_inequality_removal,[status(thm)],[f67])).
% 0.32/1.33 thf(f67,plain,(
% 0.32/1.33 ($true != $true)),
% 0.32/1.33 inference(boolean_simplification,[status(thm)],[f66])).
% 0.32/1.33 thf(f66,plain,(
% 0.32/1.33 ((e_b = e_b) != $true)),
% 0.32/1.33 inference(beta_eta_normalization,[status(thm)],[f65])).
% 0.32/1.33 thf(f65,plain,(
% 0.32/1.33 (((^[Y0 : tree_b]: (e_b = Y0)) @ e_b) != $true)),
% 0.32/1.33 inference(definition_unfolding,[status(thm)],[f61,f63])).
% 0.32/1.33 thf(f63,plain,(
% 0.32/1.33 (heapIm229596387mpty_b = (^[Y0 : tree_b]: (e_b = Y0)))),
% 0.32/1.33 inference(cnf_transformation,[status(thm)],[f31])).
% 0.32/1.33 thf(f31,plain,(
% 0.32/1.33 (heapIm229596387mpty_b = (^[Y0 : tree_b]: (e_b = Y0)))),
% 0.32/1.33 inference(fool_elimination,[status(thm)],[f1])).
% 0.32/1.33 thf(f1,axiom,(
% 0.32/1.33 ((^[X0 : tree_b] : ((e_b = X0))) = heapIm229596387mpty_b)),
% 0.32/1.33 file('/export/starexec/sandbox/tmp/tmp.GJjXH3hXcY/DTF2THF_5122.p',fact_0_hs__is__empty__def)).
% 0.32/1.33 thf(f61,plain,(
% 0.32/1.33 ((heapIm229596387mpty_b @ e_b) != $true)),
% 0.32/1.33 inference(cnf_transformation,[status(thm)],[f40])).
% 0.32/1.33 thf(f40,plain,(
% 0.32/1.33 ((heapIm229596387mpty_b @ e_b) != $true)),
% 0.32/1.33 inference(flattening,[status(thm)],[f33])).
% 0.32/1.33 thf(f33,plain,(
% 0.32/1.33 ~((heapIm229596387mpty_b @ e_b) = $true)),
% 0.32/1.33 inference(fool_elimination,[status(thm)],[f32])).
% 0.32/1.33 thf(f32,plain,(
% 0.32/1.33 ~(heapIm229596387mpty_b @ e_b)),
% 0.32/1.33 inference(rectify,[status(thm)],[f15])).
% 0.32/1.33 thf(f15,negated_conjecture,(
% 0.32/1.33 ~(heapIm229596387mpty_b @ e_b)),
% 0.32/1.33 inference(negated_conjecture,[status(cth)],[f14])).
% 0.32/1.33 thf(f14,conjecture,(
% 0.32/1.33 (heapIm229596387mpty_b @ e_b)),
% 0.32/1.33 file('/export/starexec/sandbox/tmp/tmp.GJjXH3hXcY/DTF2THF_5122.p',conj_0)).
% 0.32/1.33 % SZS output end Proof for DTF2THF_5122
% 0.32/1.33 % (5450)------------------------------
% 0.32/1.33 % (5450)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 0.32/1.33 % (5450)Termination reason: Refutation
% 0.32/1.33
% 0.32/1.33 % (5450)Memory used [KB]: 5500
% 0.32/1.33 % (5450)Time elapsed: 0.004 s
% 0.32/1.33 % (5450)Instructions burned: 3 (million)
% 0.32/1.33 % (5450)------------------------------
% 0.32/1.33 % (5450)------------------------------
% 0.32/1.33 % (5449)Success in time 0.019 s
%------------------------------------------------------------------------------