%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : DAT319^1 : TPTP v9.2.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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:45:27 AM UTC 2026
% Result : Theorem 1.36s 1.16s
% Output : Refutation 1.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : DAT319^1 : TPTP v9.2.1. Released v7.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/0.32 % Computer : n005.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue Feb 24 06:14:44 EST 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.32 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.42 ---- Original DTF file ---
% 0.16/0.42 thf(spec,logic,$$dhol).
% 0.16/0.42 %------------------------------------------------------------------------------
% 0.16/0.42 % File : DAT319^1 : TPTP v9.2.1. Released v7.0.0.
% 0.16/0.42 % Domain : Analysis
% 0.16/0.42 % Problem : APPEND_SING
% 0.16/0.42 % Version : Especial.
% 0.16/0.42 % English :
% 0.16/0.42
% 0.16/0.42 % Refs : [Kal16] Kalisyk (2016), Email to Geoff Sutcliffe
% 0.16/0.42 % Source : [Kal16]
% 0.16/0.42 % Names : APPEND_SING_.p [Kal16]
% 0.16/0.42
% 0.16/0.42 % Status : Theorem
% 0.16/0.42 % Rating : 0.00 v7.1.0
% 0.16/0.42 % Syntax : Number of formulae : 7 ( 3 unt; 4 typ; 0 def)
% 0.16/0.42 % Number of atoms : 3 ( 3 equ; 0 cnn)
% 0.16/0.42 % Maximal formula atoms : 1 ( 1 avg)
% 0.16/0.42 % Number of connectives : 36 ( 0 ~; 0 |; 0 &; 36 @)
% 0.16/0.42 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.16/0.42 % Maximal formula depth : 5 ( 4 avg)
% 0.16/0.42 % Number of types : 0 ( 0 usr)
% 0.16/0.42 % Number of type conns : 5 ( 5 >; 0 *; 0 +; 0 <<)
% 0.16/0.42 % Number of symbols : 5 ( 4 usr; 0 con; 1-3 aty)
% 0.16/0.42 % Number of variables : 12 ( 0 ^; 9 !; 0 ?; 12 :)
% 0.16/0.42 % ( 3 !>; 0 ?*; 0 @-; 0 @+)
% 0.16/0.42 % SPC : TH1_THM_EQU_NAR
% 0.16/0.42
% 0.16/0.42 % Comments : Exported from core HOL Light.
% 0.16/0.42 %------------------------------------------------------------------------------
% 0.16/0.42 thf('thf_type_type/ind_types/list',type,
% 0.16/0.42 'type/ind_types/list': $tType > $tType ).
% 0.16/0.42
% 0.16/0.42 thf('thf_const_const/lists/APPEND',type,
% 0.16/0.42 'const/lists/APPEND':
% 0.16/0.42 !>[A: $tType] : ( ( 'type/ind_types/list' @ A ) > ( 'type/ind_types/list' @ A ) > ( 'type/ind_types/list' @ A ) ) ).
% 0.16/0.42
% 0.16/0.42 thf('thf_const_const/ind_types/NIL',type,
% 0.16/0.42 'const/ind_types/NIL':
% 0.16/0.42 !>[A: $tType] : ( 'type/ind_types/list' @ A ) ).
% 0.16/0.42
% 0.16/0.42 thf('thf_const_const/ind_types/CONS',type,
% 0.16/0.42 'const/ind_types/CONS':
% 0.16/0.42 !>[A: $tType] : ( A > ( 'type/ind_types/list' @ A ) > ( 'type/ind_types/list' @ A ) ) ).
% 0.16/0.42
% 0.16/0.42 thf('thm/lists/APPEND_0',axiom,
% 0.16/0.42 ! [A: $tType,A0: 'type/ind_types/list' @ A] :
% 0.16/0.42 ( ( 'const/lists/APPEND' @ A @ ( 'const/ind_types/NIL' @ A ) @ A0 )
% 0.16/0.42 = A0 ) ).
% 0.16/0.42
% 0.16/0.42 thf('thm/lists/APPEND_1',axiom,
% 0.16/0.42 ! [A: $tType,A0: A,A1: 'type/ind_types/list' @ A,A2: 'type/ind_types/list' @ A] :
% 0.16/0.42 ( ( 'const/lists/APPEND' @ A @ ( 'const/ind_types/CONS' @ A @ A0 @ A1 ) @ A2 )
% 0.16/0.42 = ( 'const/ind_types/CONS' @ A @ A0 @ ( 'const/lists/APPEND' @ A @ A1 @ A2 ) ) ) ).
% 0.16/0.42
% 0.16/0.42 thf('thm/lists/APPEND_SING_',conjecture,
% 0.16/0.42 ! [A: $tType,A0: A,A1: 'type/ind_types/list' @ A] :
% 0.16/0.42 ( ( 'const/lists/APPEND' @ A @ ( 'const/ind_types/CONS' @ A @ A0 @ ( 'const/ind_types/NIL' @ A ) ) @ A1 )
% 0.16/0.42 = ( 'const/ind_types/CONS' @ A @ A0 @ A1 ) ) ).
% 0.16/0.42
% 0.16/0.42 %------------------------------------------------------------------------------
% 0.16/0.42 ------------------------
% 1.36/1.14 ---- Embedded in THF ---
% 1.36/1.14 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.36/1.14 %%% Generated on Tue Feb 24 06:14:45 EST 2026
% 1.36/1.14 %%% using '$$dhol' embedding, version 1.3.0.
% 1.36/1.14 %%% Logic specification used:
% 1.36/1.14 %%% thf(spec, logic, $$dhol).
% 1.36/1.14
% 1.36/1.14 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.3fuzKfq7Js/DTF2DTF2251.p
% 1.36/1.14 thf('thf_type_type/ind_types/list', type, 'type/ind_types/list': ($tType > $tType)).
% 1.36/1.14 thf('thf_const_const/lists/APPEND', type, 'const/lists/APPEND': (!> [A:$tType]: ((('type/ind_types/list' @ A) > (('type/ind_types/list' @ A) > ('type/ind_types/list' @ A)))))).
% 1.36/1.14 thf('thf_const_const/ind_types/NIL', type, 'const/ind_types/NIL': (!> [A:$tType]: (('type/ind_types/list' @ A)))).
% 1.36/1.14 thf('thf_const_const/ind_types/CONS', type, 'const/ind_types/CONS': (!> [A:$tType]: ((A > (('type/ind_types/list' @ A) > ('type/ind_types/list' @ A)))))).
% 1.36/1.14 thf('thm/lists/APPEND_0', axiom, (! [A:$tType,A0:('type/ind_types/list' @ A)]: ((((('const/lists/APPEND' @ A) @ ('const/ind_types/NIL' @ A)) @ A0) = A0)))).
% 1.36/1.14 thf('thm/lists/APPEND_1', axiom, (! [A:$tType,A0:A,A1:('type/ind_types/list' @ A),A2:('type/ind_types/list' @ A)]: ((((('const/lists/APPEND' @ A) @ ((('const/ind_types/CONS' @ A) @ A0) @ A1)) @ A2) = ((('const/ind_types/CONS' @ A) @ A0) @ ((('const/lists/APPEND' @ A) @ A1) @ A2)))))).
% 1.36/1.14 thf('thm/lists/APPEND_SING_', conjecture, (! [A:$tType,A0:A,A1:('type/ind_types/list' @ A)]: ((((('const/lists/APPEND' @ A) @ ((('const/ind_types/CONS' @ A) @ A0) @ ('const/ind_types/NIL' @ A))) @ A1) = ((('const/ind_types/CONS' @ A) @ A0) @ A1))))).
% 1.36/1.14 % SZS output end ListOfTHF for /export/starexec/sandbox2/tmp/tmp.3fuzKfq7Js/DTF2DTF2251.p
% 1.36/1.14 ------------------------
% 1.36/1.15 ---- Cleaned THF ---
% 1.36/1.15 thf('thf_type_type/ind_types/list',type,
% 1.36/1.15 'type/ind_types/list': $tType > $tType ).
% 1.36/1.15
% 1.36/1.15 thf('thf_const_const/lists/APPEND',type,
% 1.36/1.15 'const/lists/APPEND':
% 1.36/1.15 !>[A: $tType] : ( ( 'type/ind_types/list' @ A ) > ( 'type/ind_types/list' @ A ) > ( 'type/ind_types/list' @ A ) ) ).
% 1.36/1.15
% 1.36/1.15 thf('thf_const_const/ind_types/NIL',type,
% 1.36/1.15 'const/ind_types/NIL':
% 1.36/1.15 !>[A: $tType] : ( 'type/ind_types/list' @ A ) ).
% 1.36/1.15
% 1.36/1.15 thf('thf_const_const/ind_types/CONS',type,
% 1.36/1.15 'const/ind_types/CONS':
% 1.36/1.15 !>[A: $tType] : ( A > ( 'type/ind_types/list' @ A ) > ( 'type/ind_types/list' @ A ) ) ).
% 1.36/1.15
% 1.36/1.15 thf('thm/lists/APPEND_0',axiom,
% 1.36/1.15 ! [A: $tType,A0: 'type/ind_types/list' @ A] :
% 1.36/1.15 ( ( 'const/lists/APPEND' @ A @ ( 'const/ind_types/NIL' @ A ) @ A0 )
% 1.36/1.15 = A0 ) ).
% 1.36/1.15
% 1.36/1.15 thf('thm/lists/APPEND_1',axiom,
% 1.36/1.15 ! [A: $tType,A0: A,A1: 'type/ind_types/list' @ A,A2: 'type/ind_types/list' @ A] :
% 1.36/1.15 ( ( 'const/lists/APPEND' @ A @ ( 'const/ind_types/CONS' @ A @ A0 @ A1 ) @ A2 )
% 1.36/1.15 = ( 'const/ind_types/CONS' @ A @ A0 @ ( 'const/lists/APPEND' @ A @ A1 @ A2 ) ) ) ).
% 1.36/1.15
% 1.36/1.15 thf('thm/lists/APPEND_SING_',conjecture,
% 1.36/1.15 ! [A: $tType,A0: A,A1: 'type/ind_types/list' @ A] :
% 1.36/1.15 ( ( 'const/lists/APPEND' @ A @ ( 'const/ind_types/CONS' @ A @ A0 @ ( 'const/ind_types/NIL' @ A ) ) @ A1 )
% 1.36/1.15 = ( 'const/ind_types/CONS' @ A @ A0 @ A1 ) ) ).
% 1.36/1.15 ------------------------
% 1.36/1.16 % (2351)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_2251 for (3000ds/183Mi)
% 1.36/1.16 % (2351)First to succeed.
% 1.36/1.16 % (2351)Refutation found. Thanks to Tanya!
% 1.36/1.16 % SZS status Theorem for DTF2THF_2251
% 1.36/1.16 % SZS output start Proof for DTF2THF_2251
% 1.36/1.16 thf(type_def_5, type, 'type/ind_types/list': ($tType) > $tType).
% 1.36/1.16 thf(type_def_7, type, sK0: $tType).
% 1.36/1.16 thf(func_def_0, type, 'type/ind_types/list': ($tType) > $tType).
% 1.36/1.16 thf(func_def_1, type, 'const/lists/APPEND': !>[X0: $tType]:('type/ind_types/list' @ X0 > 'type/ind_types/list' @ X0 > 'type/ind_types/list' @ X0)).
% 1.36/1.16 thf(func_def_2, type, 'const/ind_types/NIL': !>[X0: $tType]:('type/ind_types/list' @ X0)).
% 1.36/1.16 thf(func_def_3, type, 'const/ind_types/CONS': !>[X0: $tType]:(X0 > 'type/ind_types/list' @ X0 > 'type/ind_types/list' @ X0)).
% 1.36/1.16 thf(func_def_7, type, sK1: sK0).
% 1.36/1.16 thf(func_def_8, type, sK2: 'type/ind_types/list' @ sK0).
% 1.36/1.16 thf(f14,plain,(
% 1.36/1.16 $false),
% 1.36/1.16 inference(trivial_inequality_removal,[status(thm)],[f13])).
% 1.36/1.16 thf(f13,plain,(
% 1.36/1.16 (('const/ind_types/CONS' @ sK0 @ sK1 @ sK2) != ('const/ind_types/CONS' @ sK0 @ sK1 @ sK2))),
% 1.36/1.16 inference(superposition,[status(thm)],[f12,f9])).
% 1.36/1.16 thf(f9,plain,(
% 1.36/1.16 ( ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : ((('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ X1) = X1)) )),
% 1.36/1.16 inference(cnf_transformation,[status(thm)],[f1])).
% 1.36/1.16 thf(f1,axiom,(
% 1.36/1.16 ! [X0 : $tType,X1 : 'type/ind_types/list' @ X0] : (('const/lists/APPEND' @ X0 @ 'const/ind_types/NIL' @ X0 @ X1) = X1)),
% 1.36/1.16 file('/export/starexec/sandbox2/tmp/tmp.3fuzKfq7Js/DTF2THF_2251.p','thm/lists/APPEND_0')).
% 1.36/1.16 thf(f12,plain,(
% 1.36/1.16 (('const/ind_types/CONS' @ sK0 @ sK1 @ sK2) != ('const/ind_types/CONS' @ sK0 @ sK1 @ ('const/lists/APPEND' @ sK0 @ 'const/ind_types/NIL' @ sK0 @ sK2)))),
% 1.36/1.16 inference(superposition,[status(thm)],[f10,f11])).
% 1.36/1.16 thf(f11,plain,(
% 1.36/1.16 ( ! [X0 : $tType,X2 : 'type/ind_types/list' @ X0,X3 : 'type/ind_types/list' @ X0,X1 : X0] : ((('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ X2) @ X3) = ('const/ind_types/CONS' @ X0 @ X1 @ ('const/lists/APPEND' @ X0 @ X2 @ X3)))) )),
% 1.36/1.16 inference(cnf_transformation,[status(thm)],[f2])).
% 1.36/1.16 thf(f2,axiom,(
% 1.36/1.16 ! [X0 : $tType,X1 : X0,X2 : 'type/ind_types/list' @ X0,X3 : 'type/ind_types/list' @ X0] : (('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ X2) @ X3) = ('const/ind_types/CONS' @ X0 @ X1 @ ('const/lists/APPEND' @ X0 @ X2 @ X3)))),
% 1.36/1.16 file('/export/starexec/sandbox2/tmp/tmp.3fuzKfq7Js/DTF2THF_2251.p','thm/lists/APPEND_1')).
% 1.36/1.16 thf(f10,plain,(
% 1.36/1.16 (('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK1 @ 'const/ind_types/NIL' @ sK0) @ sK2) != ('const/ind_types/CONS' @ sK0 @ sK1 @ sK2))),
% 1.36/1.16 inference(cnf_transformation,[status(thm)],[f8])).
% 1.36/1.16 thf(f8,plain,(
% 1.36/1.16 (('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK1 @ 'const/ind_types/NIL' @ sK0) @ sK2) != ('const/ind_types/CONS' @ sK0 @ sK1 @ sK2))),
% 1.36/1.16 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2])],[f6,f7])).
% 1.36/1.16 thf(f7,plain,(
% 1.36/1.16 ? [X0 : $tType,X1 : X0,X2 : 'type/ind_types/list' @ X0] : (('const/ind_types/CONS' @ X0 @ X1 @ X2) != ('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ 'const/ind_types/NIL' @ X0) @ X2)) => (('const/lists/APPEND' @ sK0 @ ('const/ind_types/CONS' @ sK0 @ sK1 @ 'const/ind_types/NIL' @ sK0) @ sK2) != ('const/ind_types/CONS' @ sK0 @ sK1 @ sK2))),
% 1.36/1.16 introduced(definition,[],[choice_axiom])).
% 1.36/1.16 thf(f6,plain,(
% 1.36/1.16 ? [X0 : $tType,X1 : X0,X2 : 'type/ind_types/list' @ X0] : (('const/ind_types/CONS' @ X0 @ X1 @ X2) != ('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ 'const/ind_types/NIL' @ X0) @ X2))),
% 1.36/1.16 inference(ennf_transformation,[status(thm)],[f4])).
% 1.36/1.16 thf(f4,negated_conjecture,(
% 1.36/1.16 ~! [X0 : $tType,X1 : X0,X2 : 'type/ind_types/list' @ X0] : (('const/ind_types/CONS' @ X0 @ X1 @ X2) = ('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ 'const/ind_types/NIL' @ X0) @ X2))),
% 1.36/1.16 inference(negated_conjecture,[status(cth)],[f3])).
% 1.36/1.16 thf(f3,conjecture,(
% 1.36/1.16 ! [X0 : $tType,X1 : X0,X2 : 'type/ind_types/list' @ X0] : (('const/ind_types/CONS' @ X0 @ X1 @ X2) = ('const/lists/APPEND' @ X0 @ ('const/ind_types/CONS' @ X0 @ X1 @ 'const/ind_types/NIL' @ X0) @ X2))),
% 1.36/1.16 file('/export/starexec/sandbox2/tmp/tmp.3fuzKfq7Js/DTF2THF_2251.p','thm/lists/APPEND_SING_')).
% 1.36/1.16 % SZS output end Proof for DTF2THF_2251
% 1.36/1.16 % (2351)------------------------------
% 1.36/1.16 % (2351)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.36/1.16 % (2351)Termination reason: Refutation
% 1.36/1.16
% 1.36/1.16 % (2351)Memory used [KB]: 5500
% 1.36/1.16 % (2351)Time elapsed: 0.003 s
% 1.36/1.16 % (2351)Instructions burned: 1 (million)
% 1.36/1.16 % (2351)------------------------------
% 1.36/1.16 % (2351)------------------------------
% 1.36/1.16 % (2350)Success in time 0.012 s
%------------------------------------------------------------------------------