%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP013^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n023.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:53:33 AM UTC 2026
% Result : Theorem 1.80s 1.50s
% Output : Refutation 1.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : ITP013^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.11/0.14 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.36 % Computer : n023.cluster.edu
% 0.18/0.36 % Model : x86_64 x86_64
% 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.36 % Memory : 8042.1875MB
% 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.36 % CPULimit : 300
% 0.18/0.36 % WCLimit : 300
% 0.18/0.36 % DateTime : Tue Feb 24 08:20:49 EST 2026
% 0.18/0.36 % CPUTime :
% 0.18/0.36 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.27/0.52 ---- Original DTF file ---
% 0.27/0.52 thf(spec,logic,$$dhol).
% 0.27/0.52 %------------------------------------------------------------------------------
% 0.27/0.52 % File : ITP013^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.27/0.52 % Domain : Interactive Theorem Proving
% 0.27/0.52 % Problem : HOL4 syntactic export of thm_2Ewords_2En2w__sub.p, bushy mode
% 0.27/0.52 % Version : [BG+19] axioms.
% 0.27/0.52 % English :
% 0.27/0.52
% 0.27/0.52 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.27/0.52 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe
% 0.27/0.52 % Source : [BG+19]
% 0.27/0.52 % Names : thm_2Ewords_2En2w__sub.p [Gau19]
% 0.27/0.52 % : HL406001^3.p [TPAP]
% 0.27/0.52
% 0.27/0.52 % Status : Theorem
% 0.27/0.52 % Rating : 0.33 v8.1.0, 0.25 v7.5.0
% 0.27/0.52 % Syntax : Number of formulae : 40 ( 7 unt; 21 typ; 0 def)
% 0.27/0.52 % Number of atoms : 49 ( 20 equ; 5 cnn)
% 0.27/0.52 % Maximal formula atoms : 8 ( 2 avg)
% 0.27/0.52 % Number of connectives : 181 ( 5 ~; 1 |; 14 &; 124 @)
% 0.27/0.52 % ( 20 <=>; 17 =>; 0 <=; 0 <~>)
% 0.27/0.52 % Maximal formula depth : 13 ( 6 avg)
% 0.27/0.52 % Number of types : 3 ( 2 usr)
% 0.27/0.52 % Number of type conns : 34 ( 34 >; 0 *; 0 +; 0 <<)
% 0.27/0.52 % Number of symbols : 21 ( 19 usr; 3 con; 0-4 aty)
% 0.27/0.52 % Number of variables : 62 ( 0 ^; 53 !; 1 ?; 62 :)
% 0.27/0.52 % ( 8 !>; 0 ?*; 0 @-; 0 @+)
% 0.27/0.52 % SPC : TH1_THM_EQU_NAR
% 0.27/0.52
% 0.27/0.52 % Comments :
% 0.27/0.52 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.27/0.52 %------------------------------------------------------------------------------
% 0.27/0.52 thf(tyop_2Efcp_2Ecart,type,
% 0.27/0.52 tyop_2Efcp_2Ecart: $tType > $tType > $tType ).
% 0.27/0.52
% 0.27/0.52 thf(tyop_2Emin_2Ebool,type,
% 0.27/0.52 tyop_2Emin_2Ebool: $tType ).
% 0.27/0.52
% 0.27/0.52 thf(tyop_2Emin_2Efun,type,
% 0.27/0.52 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 0.27/0.52
% 0.27/0.52 thf(tyop_2Enum_2Enum,type,
% 0.27/0.52 tyop_2Enum_2Enum: $tType ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2E_21,type,
% 0.27/0.52 c_2Ebool_2E_21:
% 0.27/0.52 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Earithmetic_2E_2B,type,
% 0.27/0.52 c_2Earithmetic_2E_2B: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Earithmetic_2E_2D,type,
% 0.27/0.52 c_2Earithmetic_2E_2D: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2E_2F_5C,type,
% 0.27/0.52 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Earithmetic_2E_3C_3D,type,
% 0.27/0.52 c_2Earithmetic_2E_3C_3D: tyop_2Enum_2Enum > tyop_2Enum_2Enum > $o ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Emin_2E_3D,type,
% 0.27/0.52 c_2Emin_2E_3D:
% 0.27/0.52 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Emin_2E_3D_3D_3E,type,
% 0.27/0.52 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2E_3F,type,
% 0.27/0.52 c_2Ebool_2E_3F:
% 0.27/0.52 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2ECOND,type,
% 0.27/0.52 c_2Ebool_2ECOND:
% 0.27/0.52 !>[A_27a: $tType] : ( $o > A_27a > A_27a > A_27a ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2EF,type,
% 0.27/0.52 c_2Ebool_2EF: $o ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2ET,type,
% 0.27/0.52 c_2Ebool_2ET: $o ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2E_5C_2F,type,
% 0.27/0.52 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ewords_2En2w,type,
% 0.27/0.52 c_2Ewords_2En2w:
% 0.27/0.52 !>[A_27a: $tType] : ( tyop_2Enum_2Enum > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ewords_2Eword__2comp,type,
% 0.27/0.52 c_2Ewords_2Eword__2comp:
% 0.27/0.52 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ewords_2Eword__add,type,
% 0.27/0.52 c_2Ewords_2Eword__add:
% 0.27/0.52 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ewords_2Eword__sub,type,
% 0.27/0.52 c_2Ewords_2Eword__sub:
% 0.27/0.52 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(c_2Ebool_2E_7E,type,
% 0.27/0.52 c_2Ebool_2E_7E: $o > $o ).
% 0.27/0.52
% 0.27/0.52 thf(logicdef_2E_2F_5C,axiom,
% 0.27/0.52 ! [V0: $o,V1: $o] :
% 0.27/0.52 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 0.27/0.52 <=> ( V0
% 0.27/0.52 & V1 ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(logicdef_2E_5C_2F,axiom,
% 0.27/0.52 ! [V0: $o,V1: $o] :
% 0.27/0.52 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 0.27/0.52 <=> ( V0
% 0.27/0.52 | V1 ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(logicdef_2E_7E,axiom,
% 0.27/0.52 ! [V0: $o] :
% 0.27/0.52 ( ( c_2Ebool_2E_7E @ V0 )
% 0.27/0.52 <=> ( (~) @ V0 ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(logicdef_2E_3D_3D_3E,axiom,
% 0.27/0.52 ! [V0: $o,V1: $o] :
% 0.27/0.52 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 0.27/0.52 <=> ( V0
% 0.27/0.52 => V1 ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(logicdef_2E_3D,axiom,
% 0.27/0.52 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 0.27/0.52 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 0.27/0.52 <=> ( V0 = V1 ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(quantdef_2E_21,axiom,
% 0.27/0.52 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.27/0.52 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 0.27/0.52 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(quantdef_2E_3F,axiom,
% 0.27/0.52 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.27/0.52 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 0.27/0.52 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2ETRUTH,axiom,
% 0.27/0.52 c_2Ebool_2ET ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 0.27/0.52 ! [V0t: $o] :
% 0.27/0.52 ( ( ( c_2Ebool_2ET
% 0.27/0.52 => V0t )
% 0.27/0.52 <=> V0t )
% 0.27/0.52 & ( ( V0t
% 0.27/0.52 => c_2Ebool_2ET )
% 0.27/0.52 <=> c_2Ebool_2ET )
% 0.27/0.52 & ( ( c_2Ebool_2EF
% 0.27/0.52 => V0t )
% 0.27/0.52 <=> c_2Ebool_2ET )
% 0.27/0.52 & ( ( V0t
% 0.27/0.52 => V0t )
% 0.27/0.52 <=> c_2Ebool_2ET )
% 0.27/0.52 & ( ( V0t
% 0.27/0.52 => c_2Ebool_2EF )
% 0.27/0.52 <=> ( (~) @ V0t ) ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2EREFL__CLAUSE,axiom,
% 0.27/0.52 ! [A_27a: $tType,V0x: A_27a] :
% 0.27/0.52 ( ( V0x = V0x )
% 0.27/0.52 <=> c_2Ebool_2ET ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 0.27/0.52 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 0.27/0.52 ( ( V0x = V1y )
% 0.27/0.52 <=> ( V1y = V0x ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 0.27/0.52 ! [V0t: $o] :
% 0.27/0.52 ( ( ( c_2Ebool_2ET = V0t )
% 0.27/0.52 <=> V0t )
% 0.27/0.52 & ( ( V0t = c_2Ebool_2ET )
% 0.27/0.52 <=> V0t )
% 0.27/0.52 & ( ( c_2Ebool_2EF = V0t )
% 0.27/0.52 <=> ( (~) @ V0t ) )
% 0.27/0.52 & ( ( V0t = c_2Ebool_2EF )
% 0.27/0.52 <=> ( (~) @ V0t ) ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2EAND__IMP__INTRO,axiom,
% 0.27/0.52 ! [V0t1: $o,V1t2: $o,V2t3: $o] :
% 0.27/0.52 ( ( V0t1
% 0.27/0.52 => ( V1t2
% 0.27/0.52 => V2t3 ) )
% 0.27/0.52 <=> ( ( V0t1
% 0.27/0.52 & V1t2 )
% 0.27/0.52 => V2t3 ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2EIMP__CONG,axiom,
% 0.27/0.52 ! [V0x: $o,V1x_27: $o,V2y: $o,V3y_27: $o] :
% 0.27/0.52 ( ( ( V0x = V1x_27 )
% 0.27/0.52 & ( V1x_27
% 0.27/0.52 => ( V2y = V3y_27 ) ) )
% 0.27/0.52 => ( ( V0x
% 0.27/0.52 => V2y )
% 0.27/0.52 <=> ( V1x_27
% 0.27/0.52 => V3y_27 ) ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2ECOND__CONG,axiom,
% 0.27/0.52 ! [A_27a: $tType,V0P: $o,V1Q: $o,V2x: A_27a,V3x_27: A_27a,V4y: A_27a,V5y_27: A_27a] :
% 0.27/0.52 ( ( ( V0P = V1Q )
% 0.27/0.52 & ( V1Q
% 0.27/0.52 => ( V2x = V3x_27 ) )
% 0.27/0.52 & ( ( (~) @ V1Q )
% 0.27/0.52 => ( V4y = V5y_27 ) ) )
% 0.27/0.52 => ( ( c_2Ebool_2ECOND @ A_27a @ V0P @ V2x @ V4y )
% 0.27/0.52 = ( c_2Ebool_2ECOND @ A_27a @ V1Q @ V3x_27 @ V5y_27 ) ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ebool_2Ebool__case__thm,axiom,
% 0.27/0.52 ! [A_27a: $tType] :
% 0.27/0.52 ( ! [V0t1: A_27a,V1t2: A_27a] :
% 0.27/0.52 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2ET @ V0t1 @ V1t2 )
% 0.27/0.52 = V0t1 )
% 0.27/0.52 & ! [V2t1: A_27a,V3t2: A_27a] :
% 0.27/0.52 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2EF @ V2t1 @ V3t2 )
% 0.27/0.52 = V3t2 ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ewords_2Eword__sub__def,axiom,
% 0.27/0.52 ! [A_27a: $tType,V0v: tyop_2Efcp_2Ecart @ $o @ A_27a,V1w: tyop_2Efcp_2Ecart @ $o @ A_27a] :
% 0.27/0.52 ( ( c_2Ewords_2Eword__sub @ A_27a @ V0v @ V1w )
% 0.27/0.52 = ( c_2Ewords_2Eword__add @ A_27a @ V0v @ ( c_2Ewords_2Eword__2comp @ A_27a @ V1w ) ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ewords_2EWORD__LITERAL__ADD,axiom,
% 0.27/0.52 ! [A_27a: $tType,A_27b: $tType] :
% 0.27/0.52 ( ! [V0m: tyop_2Enum_2Enum,V1n: tyop_2Enum_2Enum] :
% 0.27/0.52 ( ( c_2Ewords_2Eword__add @ A_27a @ ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ V0m ) ) @ ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ V1n ) ) )
% 0.27/0.52 = ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ ( c_2Earithmetic_2E_2B @ V0m @ V1n ) ) ) )
% 0.27/0.52 & ! [V2m: tyop_2Enum_2Enum,V3n: tyop_2Enum_2Enum] :
% 0.27/0.52 ( ( c_2Ewords_2Eword__add @ A_27b @ ( c_2Ewords_2En2w @ A_27b @ V2m ) @ ( c_2Ewords_2Eword__2comp @ A_27b @ ( c_2Ewords_2En2w @ A_27b @ V3n ) ) )
% 0.27/0.52 = ( c_2Ebool_2ECOND @ ( tyop_2Efcp_2Ecart @ $o @ A_27b ) @ ( c_2Earithmetic_2E_3C_3D @ V3n @ V2m ) @ ( c_2Ewords_2En2w @ A_27b @ ( c_2Earithmetic_2E_2D @ V2m @ V3n ) ) @ ( c_2Ewords_2Eword__2comp @ A_27b @ ( c_2Ewords_2En2w @ A_27b @ ( c_2Earithmetic_2E_2D @ V3n @ V2m ) ) ) ) ) ) ).
% 0.27/0.52
% 0.27/0.52 thf(thm_2Ewords_2En2w__sub,conjecture,
% 0.27/0.52 ! [A_27a: $tType,V0a: tyop_2Enum_2Enum,V1b: tyop_2Enum_2Enum] :
% 0.27/0.52 ( ( c_2Earithmetic_2E_3C_3D @ V1b @ V0a )
% 0.27/0.52 => ( ( c_2Ewords_2En2w @ A_27a @ ( c_2Earithmetic_2E_2D @ V0a @ V1b ) )
% 0.27/0.52 = ( c_2Ewords_2Eword__sub @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ V0a ) @ ( c_2Ewords_2En2w @ A_27a @ V1b ) ) ) ) ).
% 0.27/0.52
% 0.27/0.52 %------------------------------------------------------------------------------
% 0.27/0.52 ------------------------
% 1.61/1.39 ---- Embedded in THF ---
% 1.61/1.39 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.61/1.39 %%% Generated on Tue Feb 24 08:20:50 EST 2026
% 1.61/1.39 %%% using '$$dhol' embedding, version 1.3.0.
% 1.61/1.39 %%% Logic specification used:
% 1.61/1.39 %%% thf(spec, logic, $$dhol).
% 1.61/1.39
% 1.61/1.39 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2DTF19694.p
% 1.61/1.39 thf(tyop_2Efcp_2Ecart, type, tyop_2Efcp_2Ecart: ($tType > ($tType > $tType))).
% 1.61/1.39 thf(tyop_2Emin_2Ebool, type, tyop_2Emin_2Ebool: $tType).
% 1.61/1.39 thf(tyop_2Emin_2Efun, type, tyop_2Emin_2Efun: ($tType > ($tType > $tType))).
% 1.61/1.39 thf(tyop_2Enum_2Enum, type, tyop_2Enum_2Enum: $tType).
% 1.61/1.39 thf(c_2Ebool_2E_21, type, c_2Ebool_2E_21: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.61/1.39 thf(c_2Earithmetic_2E_2B, type, c_2Earithmetic_2E_2B: (tyop_2Enum_2Enum > (tyop_2Enum_2Enum > tyop_2Enum_2Enum))).
% 1.61/1.39 thf(c_2Earithmetic_2E_2D, type, c_2Earithmetic_2E_2D: (tyop_2Enum_2Enum > (tyop_2Enum_2Enum > tyop_2Enum_2Enum))).
% 1.61/1.39 thf(c_2Ebool_2E_2F_5C, type, c_2Ebool_2E_2F_5C: ($o > ($o > $o))).
% 1.61/1.39 thf(c_2Earithmetic_2E_3C_3D, type, c_2Earithmetic_2E_3C_3D: (tyop_2Enum_2Enum > (tyop_2Enum_2Enum > $o))).
% 1.61/1.39 thf(c_2Emin_2E_3D, type, c_2Emin_2E_3D: (!> [A_27a:$tType]: ((A_27a > (A_27a > $o))))).
% 1.61/1.39 thf(c_2Emin_2E_3D_3D_3E, type, c_2Emin_2E_3D_3D_3E: ($o > ($o > $o))).
% 1.61/1.39 thf(c_2Ebool_2E_3F, type, c_2Ebool_2E_3F: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.61/1.39 thf(c_2Ebool_2ECOND, type, c_2Ebool_2ECOND: (!> [A_27a:$tType]: (($o > (A_27a > (A_27a > A_27a)))))).
% 1.61/1.39 thf(c_2Ebool_2EF, type, c_2Ebool_2EF: $o).
% 1.61/1.39 thf(c_2Ebool_2ET, type, c_2Ebool_2ET: $o).
% 1.61/1.39 thf(c_2Ebool_2E_5C_2F, type, c_2Ebool_2E_5C_2F: ($o > ($o > $o))).
% 1.61/1.39 thf(c_2Ewords_2En2w, type, c_2Ewords_2En2w: (!> [A_27a:$tType]: ((tyop_2Enum_2Enum > ((tyop_2Efcp_2Ecart @ $o) @ A_27a))))).
% 1.61/1.39 thf(c_2Ewords_2Eword__2comp, type, c_2Ewords_2Eword__2comp: (!> [A_27a:$tType]: ((((tyop_2Efcp_2Ecart @ $o) @ A_27a) > ((tyop_2Efcp_2Ecart @ $o) @ A_27a))))).
% 1.61/1.39 thf(c_2Ewords_2Eword__add, type, c_2Ewords_2Eword__add: (!> [A_27a:$tType]: ((((tyop_2Efcp_2Ecart @ $o) @ A_27a) > (((tyop_2Efcp_2Ecart @ $o) @ A_27a) > ((tyop_2Efcp_2Ecart @ $o) @ A_27a)))))).
% 1.61/1.39 thf(c_2Ewords_2Eword__sub, type, c_2Ewords_2Eword__sub: (!> [A_27a:$tType]: ((((tyop_2Efcp_2Ecart @ $o) @ A_27a) > (((tyop_2Efcp_2Ecart @ $o) @ A_27a) > ((tyop_2Efcp_2Ecart @ $o) @ A_27a)))))).
% 1.61/1.39 thf(c_2Ebool_2E_7E, type, c_2Ebool_2E_7E: ($o > $o)).
% 1.61/1.39 thf(logicdef_2E_2F_5C, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_2F_5C @ V0) @ V1) <=> (V0 & V1))))).
% 1.61/1.39 thf(logicdef_2E_5C_2F, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_5C_2F @ V0) @ V1) <=> (V0 | V1))))).
% 1.61/1.39 thf(logicdef_2E_7E, axiom, (! [V0:$o]: (((c_2Ebool_2E_7E @ V0) <=> ((~) @ V0))))).
% 1.61/1.39 thf(logicdef_2E_3D_3D_3E, axiom, (! [V0:$o,V1:$o]: ((((c_2Emin_2E_3D_3D_3E @ V0) @ V1) <=> (V0 => V1))))).
% 1.61/1.39 thf(logicdef_2E_3D, axiom, (! [A_27a:$tType,V0:A_27a,V1:A_27a]: (((((c_2Emin_2E_3D @ A_27a) @ V0) @ V1) <=> (V0 = V1))))).
% 1.61/1.39 thf(quantdef_2E_21, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_21 @ A_27a) @ V0f) <=> (! [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.61/1.39 thf(quantdef_2E_3F, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_3F @ A_27a) @ V0f) <=> (? [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.61/1.39 thf(thm_2Ebool_2ETRUTH, axiom, c_2Ebool_2ET).
% 1.61/1.39 thf(thm_2Ebool_2EIMP__CLAUSES, axiom, (! [V0t:$o]: ((((c_2Ebool_2ET => V0t) <=> V0t) & (((V0t => c_2Ebool_2ET) <=> c_2Ebool_2ET) & (((c_2Ebool_2EF => V0t) <=> c_2Ebool_2ET) & (((V0t => V0t) <=> c_2Ebool_2ET) & ((V0t => c_2Ebool_2EF) <=> ((~) @ V0t))))))))).
% 1.61/1.39 thf(thm_2Ebool_2EREFL__CLAUSE, axiom, (! [A_27a:$tType,V0x:A_27a]: (((V0x = V0x) <=> c_2Ebool_2ET)))).
% 1.61/1.39 thf(thm_2Ebool_2EEQ__SYM__EQ, axiom, (! [A_27a:$tType,V0x:A_27a,V1y:A_27a]: (((V0x = V1y) <=> (V1y = V0x))))).
% 1.61/1.39 thf(thm_2Ebool_2EEQ__CLAUSES, axiom, (! [V0t:$o]: ((((c_2Ebool_2ET = V0t) <=> V0t) & (((V0t = c_2Ebool_2ET) <=> V0t) & (((c_2Ebool_2EF = V0t) <=> ((~) @ V0t)) & ((V0t = c_2Ebool_2EF) <=> ((~) @ V0t)))))))).
% 1.61/1.39 thf(thm_2Ebool_2EAND__IMP__INTRO, axiom, (! [V0t1:$o,V1t2:$o,V2t3:$o]: (((V0t1 => (V1t2 => V2t3)) <=> ((V0t1 & V1t2) => V2t3))))).
% 1.61/1.39 thf(thm_2Ebool_2EIMP__CONG, axiom, (! [V0x:$o,V1x_27:$o,V2y:$o,V3y_27:$o]: ((((V0x = V1x_27) & (V1x_27 => (V2y = V3y_27))) => ((V0x => V2y) <=> (V1x_27 => V3y_27)))))).
% 1.61/1.39 thf(thm_2Ebool_2ECOND__CONG, axiom, (! [A_27a:$tType,V0P:$o,V1Q:$o,V2x:A_27a,V3x_27:A_27a,V4y:A_27a,V5y_27:A_27a]: ((((V0P = V1Q) & ((V1Q => (V2x = V3x_27)) & (((~) @ V1Q) => (V4y = V5y_27)))) => (((((c_2Ebool_2ECOND @ A_27a) @ V0P) @ V2x) @ V4y) = ((((c_2Ebool_2ECOND @ A_27a) @ V1Q) @ V3x_27) @ V5y_27)))))).
% 1.61/1.39 thf(thm_2Ebool_2Ebool__case__thm, axiom, (! [A_27a:$tType]: (((! [V0t1:A_27a,V1t2:A_27a]: ((((((c_2Ebool_2ECOND @ A_27a) @ c_2Ebool_2ET) @ V0t1) @ V1t2) = V0t1))) & (! [V2t1:A_27a,V3t2:A_27a]: ((((((c_2Ebool_2ECOND @ A_27a) @ c_2Ebool_2EF) @ V2t1) @ V3t2) = V3t2))))))).
% 1.61/1.39 thf(thm_2Ewords_2Eword__sub__def, axiom, (! [A_27a:$tType,V0v:((tyop_2Efcp_2Ecart @ $o) @ A_27a),V1w:((tyop_2Efcp_2Ecart @ $o) @ A_27a)]: (((((c_2Ewords_2Eword__sub @ A_27a) @ V0v) @ V1w) = (((c_2Ewords_2Eword__add @ A_27a) @ V0v) @ ((c_2Ewords_2Eword__2comp @ A_27a) @ V1w)))))).
% 1.61/1.39 thf(thm_2Ewords_2EWORD__LITERAL__ADD, axiom, (! [A_27a:$tType,A_27b:$tType]: (((! [V0m:tyop_2Enum_2Enum,V1n:tyop_2Enum_2Enum]: (((((c_2Ewords_2Eword__add @ A_27a) @ ((c_2Ewords_2Eword__2comp @ A_27a) @ ((c_2Ewords_2En2w @ A_27a) @ V0m))) @ ((c_2Ewords_2Eword__2comp @ A_27a) @ ((c_2Ewords_2En2w @ A_27a) @ V1n))) = ((c_2Ewords_2Eword__2comp @ A_27a) @ ((c_2Ewords_2En2w @ A_27a) @ ((c_2Earithmetic_2E_2B @ V0m) @ V1n)))))) & (! [V2m:tyop_2Enum_2Enum,V3n:tyop_2Enum_2Enum]: (((((c_2Ewords_2Eword__add @ A_27b) @ ((c_2Ewords_2En2w @ A_27b) @ V2m)) @ ((c_2Ewords_2Eword__2comp @ A_27b) @ ((c_2Ewords_2En2w @ A_27b) @ V3n))) = ((((c_2Ebool_2ECOND @ ((tyop_2Efcp_2Ecart @ $o) @ A_27b)) @ ((c_2Earithmetic_2E_3C_3D @ V3n) @ V2m)) @ ((c_2Ewords_2En2w @ A_27b) @ ((c_2Earithmetic_2E_2D @ V2m) @ V3n))) @ ((c_2Ewords_2Eword__2comp @ A_27b) @ ((c_2Ewords_2En2w @ A_27b) @ ((c_2Earithmetic_2E_2D @ V3n) @ V2m))))))))))).
% 1.61/1.39 thf(thm_2Ewords_2En2w__sub, conjecture, (! [A_27a:$tType,V0a:tyop_2Enum_2Enum,V1b:tyop_2Enum_2Enum]: ((((c_2Earithmetic_2E_3C_3D @ V1b) @ V0a) => (((c_2Ewords_2En2w @ A_27a) @ ((c_2Earithmetic_2E_2D @ V0a) @ V1b)) = (((c_2Ewords_2Eword__sub @ A_27a) @ ((c_2Ewords_2En2w @ A_27a) @ V0a)) @ ((c_2Ewords_2En2w @ A_27a) @ V1b))))))).
% 1.61/1.39 % SZS output end ListOfTHF for /export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2DTF19694.p
% 1.61/1.39 ------------------------
% 1.80/1.40 ---- Cleaned THF ---
% 1.80/1.40 thf(tyop_2Efcp_2Ecart,type,
% 1.80/1.40 tyop_2Efcp_2Ecart: $tType > $tType > $tType ).
% 1.80/1.40
% 1.80/1.40 thf(tyop_2Emin_2Ebool,type,
% 1.80/1.40 tyop_2Emin_2Ebool: $tType ).
% 1.80/1.40
% 1.80/1.40 thf(tyop_2Emin_2Efun,type,
% 1.80/1.40 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 1.80/1.40
% 1.80/1.40 thf(tyop_2Enum_2Enum,type,
% 1.80/1.40 tyop_2Enum_2Enum: $tType ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2E_21,type,
% 1.80/1.40 c_2Ebool_2E_21:
% 1.80/1.40 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Earithmetic_2E_2B,type,
% 1.80/1.40 c_2Earithmetic_2E_2B: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Earithmetic_2E_2D,type,
% 1.80/1.40 c_2Earithmetic_2E_2D: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2E_2F_5C,type,
% 1.80/1.40 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Earithmetic_2E_3C_3D,type,
% 1.80/1.40 c_2Earithmetic_2E_3C_3D: tyop_2Enum_2Enum > tyop_2Enum_2Enum > $o ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Emin_2E_3D,type,
% 1.80/1.40 c_2Emin_2E_3D:
% 1.80/1.40 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Emin_2E_3D_3D_3E,type,
% 1.80/1.40 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2E_3F,type,
% 1.80/1.40 c_2Ebool_2E_3F:
% 1.80/1.40 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2ECOND,type,
% 1.80/1.40 c_2Ebool_2ECOND:
% 1.80/1.40 !>[A_27a: $tType] : ( $o > A_27a > A_27a > A_27a ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2EF,type,
% 1.80/1.40 c_2Ebool_2EF: $o ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2ET,type,
% 1.80/1.40 c_2Ebool_2ET: $o ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2E_5C_2F,type,
% 1.80/1.40 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ewords_2En2w,type,
% 1.80/1.40 c_2Ewords_2En2w:
% 1.80/1.40 !>[A_27a: $tType] : ( tyop_2Enum_2Enum > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ewords_2Eword__2comp,type,
% 1.80/1.40 c_2Ewords_2Eword__2comp:
% 1.80/1.40 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ewords_2Eword__add,type,
% 1.80/1.40 c_2Ewords_2Eword__add:
% 1.80/1.40 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ewords_2Eword__sub,type,
% 1.80/1.40 c_2Ewords_2Eword__sub:
% 1.80/1.40 !>[A_27a: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) > ( tyop_2Efcp_2Ecart @ $o @ A_27a ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(c_2Ebool_2E_7E,type,
% 1.80/1.40 c_2Ebool_2E_7E: $o > $o ).
% 1.80/1.40
% 1.80/1.40 thf(logicdef_2E_2F_5C,axiom,
% 1.80/1.40 ! [V0: $o,V1: $o] :
% 1.80/1.40 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 1.80/1.40 <=> ( V0
% 1.80/1.40 & V1 ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(logicdef_2E_5C_2F,axiom,
% 1.80/1.40 ! [V0: $o,V1: $o] :
% 1.80/1.40 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 1.80/1.40 <=> ( V0
% 1.80/1.40 | V1 ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(logicdef_2E_7E,axiom,
% 1.80/1.40 ! [V0: $o] :
% 1.80/1.40 ( ( c_2Ebool_2E_7E @ V0 )
% 1.80/1.40 <=> ( (~) @ V0 ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(logicdef_2E_3D_3D_3E,axiom,
% 1.80/1.40 ! [V0: $o,V1: $o] :
% 1.80/1.40 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 1.80/1.40 <=> ( V0
% 1.80/1.40 => V1 ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(logicdef_2E_3D,axiom,
% 1.80/1.40 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 1.80/1.40 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 1.80/1.40 <=> ( V0 = V1 ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(quantdef_2E_21,axiom,
% 1.80/1.40 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.80/1.40 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 1.80/1.40 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(quantdef_2E_3F,axiom,
% 1.80/1.40 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.80/1.40 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 1.80/1.40 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2ETRUTH,axiom,
% 1.80/1.40 c_2Ebool_2ET ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 1.80/1.40 ! [V0t: $o] :
% 1.80/1.40 ( ( ( c_2Ebool_2ET
% 1.80/1.40 => V0t )
% 1.80/1.40 <=> V0t )
% 1.80/1.40 & ( ( V0t
% 1.80/1.40 => c_2Ebool_2ET )
% 1.80/1.40 <=> c_2Ebool_2ET )
% 1.80/1.40 & ( ( c_2Ebool_2EF
% 1.80/1.40 => V0t )
% 1.80/1.40 <=> c_2Ebool_2ET )
% 1.80/1.40 & ( ( V0t
% 1.80/1.40 => V0t )
% 1.80/1.40 <=> c_2Ebool_2ET )
% 1.80/1.40 & ( ( V0t
% 1.80/1.40 => c_2Ebool_2EF )
% 1.80/1.40 <=> ( (~) @ V0t ) ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2EREFL__CLAUSE,axiom,
% 1.80/1.40 ! [A_27a: $tType,V0x: A_27a] :
% 1.80/1.40 ( ( V0x = V0x )
% 1.80/1.40 <=> c_2Ebool_2ET ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2EEQ__SYM__EQ,axiom,
% 1.80/1.40 ! [A_27a: $tType,V0x: A_27a,V1y: A_27a] :
% 1.80/1.40 ( ( V0x = V1y )
% 1.80/1.40 <=> ( V1y = V0x ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 1.80/1.40 ! [V0t: $o] :
% 1.80/1.40 ( ( ( c_2Ebool_2ET = V0t )
% 1.80/1.40 <=> V0t )
% 1.80/1.40 & ( ( V0t = c_2Ebool_2ET )
% 1.80/1.40 <=> V0t )
% 1.80/1.40 & ( ( c_2Ebool_2EF = V0t )
% 1.80/1.40 <=> ( (~) @ V0t ) )
% 1.80/1.40 & ( ( V0t = c_2Ebool_2EF )
% 1.80/1.40 <=> ( (~) @ V0t ) ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2EAND__IMP__INTRO,axiom,
% 1.80/1.40 ! [V0t1: $o,V1t2: $o,V2t3: $o] :
% 1.80/1.40 ( ( V0t1
% 1.80/1.40 => ( V1t2
% 1.80/1.40 => V2t3 ) )
% 1.80/1.40 <=> ( ( V0t1
% 1.80/1.40 & V1t2 )
% 1.80/1.40 => V2t3 ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2EIMP__CONG,axiom,
% 1.80/1.40 ! [V0x: $o,V1x_27: $o,V2y: $o,V3y_27: $o] :
% 1.80/1.40 ( ( ( V0x = V1x_27 )
% 1.80/1.40 & ( V1x_27
% 1.80/1.40 => ( V2y = V3y_27 ) ) )
% 1.80/1.40 => ( ( V0x
% 1.80/1.40 => V2y )
% 1.80/1.40 <=> ( V1x_27
% 1.80/1.40 => V3y_27 ) ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2ECOND__CONG,axiom,
% 1.80/1.40 ! [A_27a: $tType,V0P: $o,V1Q: $o,V2x: A_27a,V3x_27: A_27a,V4y: A_27a,V5y_27: A_27a] :
% 1.80/1.40 ( ( ( V0P = V1Q )
% 1.80/1.40 & ( V1Q
% 1.80/1.40 => ( V2x = V3x_27 ) )
% 1.80/1.40 & ( ( (~) @ V1Q )
% 1.80/1.40 => ( V4y = V5y_27 ) ) )
% 1.80/1.40 => ( ( c_2Ebool_2ECOND @ A_27a @ V0P @ V2x @ V4y )
% 1.80/1.40 = ( c_2Ebool_2ECOND @ A_27a @ V1Q @ V3x_27 @ V5y_27 ) ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ebool_2Ebool__case__thm,axiom,
% 1.80/1.40 ! [A_27a: $tType] :
% 1.80/1.40 ( ! [V0t1: A_27a,V1t2: A_27a] :
% 1.80/1.40 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2ET @ V0t1 @ V1t2 )
% 1.80/1.40 = V0t1 )
% 1.80/1.40 & ! [V2t1: A_27a,V3t2: A_27a] :
% 1.80/1.40 ( ( c_2Ebool_2ECOND @ A_27a @ c_2Ebool_2EF @ V2t1 @ V3t2 )
% 1.80/1.40 = V3t2 ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ewords_2Eword__sub__def,axiom,
% 1.80/1.40 ! [A_27a: $tType,V0v: tyop_2Efcp_2Ecart @ $o @ A_27a,V1w: tyop_2Efcp_2Ecart @ $o @ A_27a] :
% 1.80/1.40 ( ( c_2Ewords_2Eword__sub @ A_27a @ V0v @ V1w )
% 1.80/1.40 = ( c_2Ewords_2Eword__add @ A_27a @ V0v @ ( c_2Ewords_2Eword__2comp @ A_27a @ V1w ) ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ewords_2EWORD__LITERAL__ADD,axiom,
% 1.80/1.40 ! [A_27a: $tType,A_27b: $tType] :
% 1.80/1.40 ( ! [V0m: tyop_2Enum_2Enum,V1n: tyop_2Enum_2Enum] :
% 1.80/1.40 ( ( c_2Ewords_2Eword__add @ A_27a @ ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ V0m ) ) @ ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ V1n ) ) )
% 1.80/1.40 = ( c_2Ewords_2Eword__2comp @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ ( c_2Earithmetic_2E_2B @ V0m @ V1n ) ) ) )
% 1.80/1.40 & ! [V2m: tyop_2Enum_2Enum,V3n: tyop_2Enum_2Enum] :
% 1.80/1.40 ( ( c_2Ewords_2Eword__add @ A_27b @ ( c_2Ewords_2En2w @ A_27b @ V2m ) @ ( c_2Ewords_2Eword__2comp @ A_27b @ ( c_2Ewords_2En2w @ A_27b @ V3n ) ) )
% 1.80/1.40 = ( c_2Ebool_2ECOND @ ( tyop_2Efcp_2Ecart @ $o @ A_27b ) @ ( c_2Earithmetic_2E_3C_3D @ V3n @ V2m ) @ ( c_2Ewords_2En2w @ A_27b @ ( c_2Earithmetic_2E_2D @ V2m @ V3n ) ) @ ( c_2Ewords_2Eword__2comp @ A_27b @ ( c_2Ewords_2En2w @ A_27b @ ( c_2Earithmetic_2E_2D @ V3n @ V2m ) ) ) ) ) ) ).
% 1.80/1.40
% 1.80/1.40 thf(thm_2Ewords_2En2w__sub,conjecture,
% 1.80/1.40 ! [A_27a: $tType,V0a: tyop_2Enum_2Enum,V1b: tyop_2Enum_2Enum] :
% 1.80/1.40 ( ( c_2Earithmetic_2E_3C_3D @ V1b @ V0a )
% 1.80/1.40 => ( ( c_2Ewords_2En2w @ A_27a @ ( c_2Earithmetic_2E_2D @ V0a @ V1b ) )
% 1.80/1.40 = ( c_2Ewords_2Eword__sub @ A_27a @ ( c_2Ewords_2En2w @ A_27a @ V0a ) @ ( c_2Ewords_2En2w @ A_27a @ V1b ) ) ) ) ).
% 1.80/1.40 ------------------------
% 1.80/1.42 % (19805)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_19694 for (2999ds/2Mi)
% 1.80/1.42 % (19805)Instruction limit reached!
% 1.80/1.42 % (19805)------------------------------
% 1.80/1.42 % (19805)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.42 % (19805)Termination reason: Unknown
% 1.80/1.42 % (19805)Termination phase: shuffling
% 1.80/1.42
% 1.80/1.42 % (19805)Memory used [KB]: 1023
% 1.80/1.42 % (19803)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_19694 for (2999ds/27Mi)
% 1.80/1.42 % (19805)Time elapsed: 0.002 s
% 1.80/1.42 % (19805)Instructions burned: 3 (million)
% 1.80/1.42 % (19805)------------------------------
% 1.80/1.42 % (19805)------------------------------
% 1.80/1.42 % (19801)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/183Mi)
% 1.80/1.42 % (19802)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_19694 for (2999ds/4Mi)
% 1.80/1.42 % (19804)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/2Mi)
% 1.80/1.43 % (19806)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_19694 for (2999ds/275Mi)
% 1.80/1.43 % (19807)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/18Mi)
% 1.80/1.43 % (19804)Instruction limit reached!
% 1.80/1.43 % (19804)------------------------------
% 1.80/1.43 % (19804)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.43 % (19804)Termination reason: Unknown
% 1.80/1.43 % (19804)Termination phase: Property scanning
% 1.80/1.43
% 1.80/1.43 % (19804)Memory used [KB]: 1023
% 1.80/1.43 % (19804)Time elapsed: 0.003 s
% 1.80/1.43 % (19804)Instructions burned: 2 (million)
% 1.80/1.43 % (19804)------------------------------
% 1.80/1.43 % (19804)------------------------------
% 1.80/1.43 % (19802)Instruction limit reached!
% 1.80/1.43 % (19802)------------------------------
% 1.80/1.43 % (19802)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.43 % (19802)Termination reason: Unknown
% 1.80/1.43 % (19802)Termination phase: shuffling
% 1.80/1.43
% 1.80/1.43 % (19802)Memory used [KB]: 1023
% 1.80/1.43 % (19802)Time elapsed: 0.004 s
% 1.80/1.43 % (19802)Instructions burned: 4 (million)
% 1.80/1.43 % (19802)------------------------------
% 1.80/1.43 % (19802)------------------------------
% 1.80/1.43 % (19808)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/3Mi)
% 1.80/1.43 % (19806)Refutation not found, incomplete strategy
% 1.80/1.43 % (19806)------------------------------
% 1.80/1.43 % (19806)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.43 % (19806)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.43
% 1.80/1.43
% 1.80/1.43 % (19806)Memory used [KB]: 5500
% 1.80/1.43 % (19806)Time elapsed: 0.004 s
% 1.80/1.43 % (19806)Instructions burned: 3 (million)
% 1.80/1.43 % (19806)------------------------------
% 1.80/1.43 % (19806)------------------------------
% 1.80/1.43 % (19808)Instruction limit reached!
% 1.80/1.43 % (19808)------------------------------
% 1.80/1.43 % (19808)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.43 % (19808)Termination reason: Unknown
% 1.80/1.43 % (19808)Termination phase: Clausification
% 1.80/1.43
% 1.80/1.43 % (19808)Memory used [KB]: 1023
% 1.80/1.43 % (19808)Time elapsed: 0.002 s
% 1.80/1.43 % (19808)Instructions burned: 4 (million)
% 1.80/1.43 % (19808)------------------------------
% 1.80/1.43 % (19808)------------------------------
% 1.80/1.43 % (19803)Instruction limit reached!
% 1.80/1.43 % (19803)------------------------------
% 1.80/1.43 % (19803)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.43 % (19803)Termination reason: Unknown
% 1.80/1.43 % (19803)Termination phase: Saturation
% 1.80/1.43
% 1.80/1.43 % (19803)Memory used [KB]: 5756
% 1.80/1.43 % (19803)Time elapsed: 0.012 s
% 1.80/1.43 % (19803)Instructions burned: 27 (million)
% 1.80/1.43 % (19803)------------------------------
% 1.80/1.43 % (19803)------------------------------
% 1.80/1.44 % (19811)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/3Mi)
% 1.80/1.44 % (19807)Instruction limit reached!
% 1.80/1.44 % (19807)------------------------------
% 1.80/1.44 % (19807)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.44 % (19807)Termination reason: Unknown
% 1.80/1.44 % (19807)Termination phase: Saturation
% 1.80/1.44
% 1.80/1.44 % (19807)Memory used [KB]: 5756
% 1.80/1.44 % (19807)Time elapsed: 0.014 s
% 1.80/1.44 % (19807)Instructions burned: 19 (million)
% 1.80/1.44 % (19807)------------------------------
% 1.80/1.44 % (19807)------------------------------
% 1.80/1.44 % (19811)Instruction limit reached!
% 1.80/1.44 % (19811)------------------------------
% 1.80/1.44 % (19811)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.44 % (19811)Termination reason: Unknown
% 1.80/1.44 % (19811)Termination phase: Property scanning
% 1.80/1.44
% 1.80/1.44 % (19811)Memory used [KB]: 1023
% 1.80/1.44 % (19811)Time elapsed: 0.002 s
% 1.80/1.44 % (19811)Instructions burned: 4 (million)
% 1.80/1.44 % (19811)------------------------------
% 1.80/1.44 % (19811)------------------------------
% 1.80/1.44 % (19813)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/7Mi)
% 1.80/1.44 % (19813)Instruction limit reached!
% 1.80/1.44 % (19813)------------------------------
% 1.80/1.44 % (19813)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.44 % (19813)Termination reason: Unknown
% 1.80/1.44 % (19813)Termination phase: Saturation
% 1.80/1.44
% 1.80/1.44 % (19813)Memory used [KB]: 1151
% 1.80/1.44 % (19813)Time elapsed: 0.004 s
% 1.80/1.44 % (19813)Instructions burned: 7 (million)
% 1.80/1.44 % (19813)------------------------------
% 1.80/1.44 % (19813)------------------------------
% 1.80/1.44 % (19809)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/37Mi)
% 1.80/1.44 % (19810)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/15Mi)
% 1.80/1.44 % Exception at run slice level
% 1.80/1.44 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.80/1.45 % (19812)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/1041Mi)
% 1.80/1.45 % (19815)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/3Mi)
% 1.80/1.45 % Exception at run slice level
% 1.80/1.45 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.80/1.45 % (19815)Instruction limit reached!
% 1.80/1.45 % (19815)------------------------------
% 1.80/1.45 % (19815)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.45 % (19815)Termination reason: Unknown
% 1.80/1.45 % (19815)Termination phase: Preprocessing 3
% 1.80/1.45
% 1.80/1.45 % (19815)Memory used [KB]: 1023
% 1.80/1.45 % (19815)Time elapsed: 0.002 s
% 1.80/1.45 % (19815)Instructions burned: 4 (million)
% 1.80/1.45 % (19815)------------------------------
% 1.80/1.45 % (19815)------------------------------
% 1.80/1.45 % (19816)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/3Mi)
% 1.80/1.45 % (19814)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/16Mi)
% 1.80/1.45 % (19816)Instruction limit reached!
% 1.80/1.45 % (19816)------------------------------
% 1.80/1.45 % (19816)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.45 % (19816)Termination reason: Unknown
% 1.80/1.45 % (19816)Termination phase: Preprocessing 3
% 1.80/1.45
% 1.80/1.45 % (19816)Memory used [KB]: 1023
% 1.80/1.45 % (19816)Time elapsed: 0.003 s
% 1.80/1.45 % (19816)Instructions burned: 3 (million)
% 1.80/1.45 % (19816)------------------------------
% 1.80/1.45 % (19816)------------------------------
% 1.80/1.45 % (19810)Instruction limit reached!
% 1.80/1.45 % (19810)------------------------------
% 1.80/1.45 % (19810)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.45 % (19810)Termination reason: Unknown
% 1.80/1.45 % (19810)Termination phase: Saturation
% 1.80/1.45
% 1.80/1.45 % (19810)Memory used [KB]: 5756
% 1.80/1.45 % (19810)Time elapsed: 0.012 s
% 1.80/1.45 % (19810)Instructions burned: 15 (million)
% 1.80/1.45 % (19810)------------------------------
% 1.80/1.45 % (19810)------------------------------
% 1.80/1.46 % (19814)Instruction limit reached!
% 1.80/1.46 % (19814)------------------------------
% 1.80/1.46 % (19814)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.46 % (19814)Termination reason: Unknown
% 1.80/1.46 % (19814)Termination phase: Saturation
% 1.80/1.46
% 1.80/1.46 % (19814)Memory used [KB]: 5756
% 1.80/1.46 % (19814)Time elapsed: 0.008 s
% 1.80/1.46 % (19814)Instructions burned: 16 (million)
% 1.80/1.46 % (19814)------------------------------
% 1.80/1.46 % (19814)------------------------------
% 1.80/1.46 % (19819)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/4Mi)
% 1.80/1.46 % (19819)Instruction limit reached!
% 1.80/1.46 % (19819)------------------------------
% 1.80/1.46 % (19819)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.46 % (19819)Termination reason: Unknown
% 1.80/1.46 % (19819)Termination phase: Property scanning
% 1.80/1.46
% 1.80/1.46 % (19819)Memory used [KB]: 1023
% 1.80/1.46 % (19819)Time elapsed: 0.002 s
% 1.80/1.46 % (19819)Instructions burned: 4 (million)
% 1.80/1.46 % (19819)------------------------------
% 1.80/1.46 % (19819)------------------------------
% 1.80/1.46 % (19817)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/7Mi)
% 1.80/1.46 % (19823)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/18Mi)
% 1.80/1.47 % (19817)Instruction limit reached!
% 1.80/1.47 % (19817)------------------------------
% 1.80/1.47 % (19817)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.47 % (19817)Termination reason: Unknown
% 1.80/1.47 % (19817)Termination phase: Saturation
% 1.80/1.47
% 1.80/1.47 % (19817)Memory used [KB]: 5628
% 1.80/1.47 % (19817)Time elapsed: 0.007 s
% 1.80/1.47 % (19817)Instructions burned: 7 (million)
% 1.80/1.47 % (19817)------------------------------
% 1.80/1.47 % (19817)------------------------------
% 1.80/1.47 % (19825)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/6Mi)
% 1.80/1.47 % (19826)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/902Mi)
% 1.80/1.47 % (19824)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/710Mi)
% 1.80/1.47 % (19823)Instruction limit reached!
% 1.80/1.47 % (19823)------------------------------
% 1.80/1.47 % (19823)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.47 % (19823)Termination reason: Unknown
% 1.80/1.47 % (19823)Termination phase: Saturation
% 1.80/1.47
% 1.80/1.47 % (19823)Memory used [KB]: 5756
% 1.80/1.47 % (19823)Time elapsed: 0.008 s
% 1.80/1.47 % (19823)Instructions burned: 19 (million)
% 1.80/1.47 % (19823)------------------------------
% 1.80/1.47 % (19823)------------------------------
% 1.80/1.47 % (19825)Instruction limit reached!
% 1.80/1.47 % (19825)------------------------------
% 1.80/1.47 % (19825)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.47 % (19825)Termination reason: Unknown
% 1.80/1.47 % (19825)Termination phase: Saturation
% 1.80/1.47
% 1.80/1.47 % (19825)Memory used [KB]: 5628
% 1.80/1.47 % (19825)Time elapsed: 0.004 s
% 1.80/1.47 % (19825)Instructions burned: 7 (million)
% 1.80/1.47 % (19825)------------------------------
% 1.80/1.47 % (19825)------------------------------
% 1.80/1.48 % (19818)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/3Mi)
% 1.80/1.48 % (19824)Refutation not found, incomplete strategy
% 1.80/1.48 % (19824)------------------------------
% 1.80/1.48 % (19824)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.48 % (19824)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.48
% 1.80/1.48
% 1.80/1.48 % (19824)Memory used [KB]: 5628
% 1.80/1.48 % (19824)Time elapsed: 0.009 s
% 1.80/1.48 % (19824)Instructions burned: 17 (million)
% 1.80/1.48 % (19818)Instruction limit reached!
% 1.80/1.48 % (19818)------------------------------
% 1.80/1.48 % (19818)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.48 % (19824)------------------------------
% 1.80/1.48 % (19824)------------------------------
% 1.80/1.48 % (19818)Termination reason: Unknown
% 1.80/1.48 % (19818)Termination phase: shuffling
% 1.80/1.48
% 1.80/1.48 % (19818)Memory used [KB]: 1023
% 1.80/1.48 % (19818)Time elapsed: 0.005 s
% 1.80/1.48 % (19818)Instructions burned: 3 (million)
% 1.80/1.48 % (19818)------------------------------
% 1.80/1.48 % (19818)------------------------------
% 1.80/1.48 % (19828)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/5Mi)
% 1.80/1.48 % (19829)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/6Mi)
% 1.80/1.48 % Exception at run slice level
% 1.80/1.48 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.80/1.48 % Exception at run slice level
% 1.80/1.48 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.80/1.48 % (19827)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/21Mi)
% 1.80/1.49 % (19830)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/377Mi)
% 1.80/1.49 % (19832)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/19Mi)
% 1.80/1.49 % Exception at run slice level% (19833)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_19694 for (2999ds/879Mi)
% 1.80/1.49
% 1.80/1.49 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.80/1.50 % (19826)First to succeed.
% 1.80/1.50 % (19826)Refutation found. Thanks to Tanya!
% 1.80/1.50 % SZS status Theorem for DTF2THF_19694
% 1.80/1.50 % SZS output start Proof for DTF2THF_19694
% 1.80/1.50 thf(type_def_6, type, tyop_2Enum_2Enum: $tType).
% 1.80/1.50 thf(type_def_7, type, tyop_2Efcp_2Ecart: ($tType * $tType) > $tType).
% 1.80/1.50 thf(type_def_8, type, sK2: $tType).
% 1.80/1.50 thf(func_def_0, type, tyop_2Efcp_2Ecart: ($tType * $tType) > $tType).
% 1.80/1.50 thf(func_def_1, type, tyop_2Emin_2Ebool: $tType).
% 1.80/1.50 thf(func_def_2, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 1.80/1.50 thf(func_def_3, type, tyop_2Enum_2Enum: $tType).
% 1.80/1.50 thf(func_def_4, type, c_2Ebool_2E_21: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.80/1.50 thf(func_def_5, type, c_2Earithmetic_2E_2B: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum).
% 1.80/1.50 thf(func_def_6, type, c_2Earithmetic_2E_2D: tyop_2Enum_2Enum > tyop_2Enum_2Enum > tyop_2Enum_2Enum).
% 1.80/1.50 thf(func_def_7, type, c_2Ebool_2E_2F_5C: $o > $o > $o).
% 1.80/1.50 thf(func_def_8, type, c_2Earithmetic_2E_3C_3D: tyop_2Enum_2Enum > tyop_2Enum_2Enum > $o).
% 1.80/1.50 thf(func_def_9, type, c_2Emin_2E_3D: !>[X0: $tType]:(X0 > X0 > $o)).
% 1.80/1.50 thf(func_def_10, type, c_2Emin_2E_3D_3D_3E: $o > $o > $o).
% 1.80/1.50 thf(func_def_11, type, c_2Ebool_2E_3F: !>[X0: $tType]:((X0 > $o) > $o)).
% 1.80/1.50 thf(func_def_12, type, c_2Ebool_2ECOND: !>[X0: $tType]:($o > X0 > X0 > X0)).
% 1.80/1.50 thf(func_def_15, type, c_2Ebool_2E_5C_2F: $o > $o > $o).
% 1.80/1.50 thf(func_def_16, type, c_2Ewords_2En2w: !>[X0: $tType]:(tyop_2Enum_2Enum > tyop_2Efcp_2Ecart @ $o @ X0)).
% 1.80/1.50 thf(func_def_17, type, c_2Ewords_2Eword__2comp: !>[X0: $tType]:(tyop_2Efcp_2Ecart @ $o @ X0 > tyop_2Efcp_2Ecart @ $o @ X0)).
% 1.80/1.50 thf(func_def_18, type, c_2Ewords_2Eword__add: !>[X0: $tType]:(tyop_2Efcp_2Ecart @ $o @ X0 > tyop_2Efcp_2Ecart @ $o @ X0 > tyop_2Efcp_2Ecart @ $o @ X0)).
% 1.80/1.50 thf(func_def_19, type, c_2Ewords_2Eword__sub: !>[X0: $tType]:(tyop_2Efcp_2Ecart @ $o @ X0 > tyop_2Efcp_2Ecart @ $o @ X0 > tyop_2Efcp_2Ecart @ $o @ X0)).
% 1.80/1.50 thf(func_def_20, type, c_2Ebool_2E_7E: $o > $o).
% 1.80/1.50 thf(func_def_25, type, sK0: !>[X0: $tType]:((X0 > $o) > X0)).
% 1.80/1.50 thf(func_def_26, type, sK1: !>[X0: $tType]:((X0 > $o) > X0)).
% 1.80/1.50 thf(func_def_27, type, sK3: tyop_2Enum_2Enum).
% 1.80/1.50 thf(func_def_28, type, sK4: tyop_2Enum_2Enum).
% 1.80/1.50 thf(func_def_30, type, ph6: !>[X0: $tType]:(X0)).
% 1.80/1.50 thf(f664,plain,(
% 1.80/1.50 $false),
% 1.80/1.50 inference(avatar_sat_refutation,[status(thm)],[f414,f438,f663])).
% 1.80/1.50 thf(f663,plain,(
% 1.80/1.50 ~spl5_3),
% 1.80/1.50 inference(avatar_contradiction_clause,[status(thm)],[f662])).
% 1.80/1.50 thf(f662,plain,(
% 1.80/1.50 $false | ~spl5_3),
% 1.80/1.50 inference(trivial_inequality_removal,[status(thm)],[f661])).
% 1.80/1.50 thf(f661,plain,(
% 1.80/1.50 ((c_2Ewords_2En2w @ sK2 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) != (c_2Ewords_2En2w @ sK2 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4))) | ~spl5_3),
% 1.80/1.50 inference(superposition,[status(thm)],[f146,f660])).
% 1.80/1.50 thf(f660,plain,(
% 1.80/1.50 ( ! [X0 : $tType] : (((c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) = (c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)))) ) | ~spl5_3),
% 1.80/1.50 inference(forward_demodulation,[status(thm)],[f340,f494])).
% 1.80/1.50 thf(f494,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((c_2Ebool_2ECOND @ X0 @ $true @ X1 @ X2) = X1)) ) | ~spl5_3),
% 1.80/1.50 inference(superposition,[status(thm)],[f106,f314])).
% 1.80/1.50 thf(f314,plain,(
% 1.80/1.50 (c_2Ebool_2ET = $true) | ~spl5_3),
% 1.80/1.50 inference(avatar_component_clause,[status(thm)],[f313])).
% 1.80/1.50 thf(f313,definition,(
% 1.80/1.50 spl5_3 <=> (c_2Ebool_2ET = $true)),
% 1.80/1.50 introduced(definition,[new_symbols(naming,[spl5_3])],[avatar_definition])).
% 1.80/1.50 thf(f106,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : X0,X1 : X0] : (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X1 @ X2) = X1)) )),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f54])).
% 1.80/1.50 thf(f54,plain,(
% 1.80/1.50 ! [X0 : $tType] : (! [X1 : X0,X2 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X1 @ X2) = X1) & ! [X3 : X0,X4 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X3 @ X4) = X4))),
% 1.80/1.50 inference(rectify,[status(thm)],[f16])).
% 1.80/1.50 thf(f16,axiom,(
% 1.80/1.50 ! [X0 : $tType] : (! [X8 : X0,X9 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X8 @ X9) = X8) & ! [X20 : X0,X21 : X0] : ((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X20 @ X21) = X21))),
% 1.80/1.50 file('/export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2THF_19694.p',thm_2Ebool_2Ebool__case__thm)).
% 1.80/1.50 thf(f340,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : tyop_2Efcp_2Ecart @ $o @ X0] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ X2))) )),
% 1.80/1.50 inference(trivial_inequality_removal,[status(thm)],[f339])).
% 1.80/1.50 thf(f339,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : tyop_2Efcp_2Ecart @ $o @ X0] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ X2)) | ($true = $false)) )),
% 1.80/1.50 inference(boolean_simplification,[status(thm)],[f334])).
% 1.80/1.50 thf(f334,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : tyop_2Efcp_2Ecart @ $o @ X0] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ X2)) | ((~ $true) = $true)) )),
% 1.80/1.50 inference(superposition,[status(thm)],[f216,f277])).
% 1.80/1.50 thf(f277,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X1 : tyop_2Efcp_2Ecart @ $o @ X0] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ X1))) )),
% 1.80/1.50 inference(trivial_inequality_removal,[status(thm)],[f276])).
% 1.80/1.50 thf(f276,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X1 : tyop_2Efcp_2Ecart @ $o @ X0] : (($true = $false) | ((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ X1))) )),
% 1.80/1.50 inference(boolean_simplification,[status(thm)],[f274])).
% 1.80/1.50 thf(f274,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X1 : tyop_2Efcp_2Ecart @ $o @ X0] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ X1)) | ((~ $true) = $true)) )),
% 1.80/1.50 inference(superposition,[status(thm)],[f216,f257])).
% 1.80/1.50 thf(f257,plain,(
% 1.80/1.50 ( ! [X0 : $tType] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2En2w @ X0 @ sK4)) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK4 @ sK3)))))) )),
% 1.80/1.50 inference(forward_demodulation,[status(thm)],[f256,f99])).
% 1.80/1.50 thf(f99,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : tyop_2Efcp_2Ecart @ $o @ X0,X1 : tyop_2Efcp_2Ecart @ $o @ X0] : (((c_2Ewords_2Eword__add @ X0 @ X1 @ (c_2Ewords_2Eword__2comp @ X0 @ X2)) = (c_2Ewords_2Eword__sub @ X0 @ X1 @ X2))) )),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f55])).
% 1.80/1.50 thf(f55,plain,(
% 1.80/1.50 ! [X0 : $tType,X1 : tyop_2Efcp_2Ecart @ $o @ X0,X2 : tyop_2Efcp_2Ecart @ $o @ X0] : ((c_2Ewords_2Eword__add @ X0 @ X1 @ (c_2Ewords_2Eword__2comp @ X0 @ X2)) = (c_2Ewords_2Eword__sub @ X0 @ X1 @ X2))),
% 1.80/1.50 inference(rectify,[status(thm)],[f17])).
% 1.80/1.50 thf(f17,axiom,(
% 1.80/1.50 ! [X0 : $tType,X22 : tyop_2Efcp_2Ecart @ $o @ X0,X23 : tyop_2Efcp_2Ecart @ $o @ X0] : ((c_2Ewords_2Eword__sub @ X0 @ X22 @ X23) = (c_2Ewords_2Eword__add @ X0 @ X22 @ (c_2Ewords_2Eword__2comp @ X0 @ X23)))),
% 1.80/1.50 file('/export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2THF_19694.p',thm_2Ewords_2Eword__sub__def)).
% 1.80/1.50 thf(f256,plain,(
% 1.80/1.50 ( ! [X0 : $tType] : (((c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X0 @ $true @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ sK4 @ sK3)))) = (c_2Ewords_2Eword__add @ X0 @ (c_2Ewords_2En2w @ X0 @ sK3) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ sK4))))) )),
% 1.80/1.50 inference(superposition,[status(thm)],[f142,f145])).
% 1.80/1.50 thf(f145,plain,(
% 1.80/1.50 ($true = (c_2Earithmetic_2E_3C_3D @ sK4 @ sK3))),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f86])).
% 1.80/1.50 thf(f86,plain,(
% 1.80/1.50 ((c_2Ewords_2Eword__sub @ sK2 @ (c_2Ewords_2En2w @ sK2 @ sK3) @ (c_2Ewords_2En2w @ sK2 @ sK4)) != (c_2Ewords_2En2w @ sK2 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4))) & ($true = (c_2Earithmetic_2E_3C_3D @ sK4 @ sK3))),
% 1.80/1.50 inference(skolemisation,[status(esa),new_symbols(skolem,[sK2,sK3,sK4])],[f61,f85])).
% 1.80/1.50 thf(f85,plain,(
% 1.80/1.50 ? [X0 : $tType,X1 : tyop_2Enum_2Enum,X2 : tyop_2Enum_2Enum] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ X1) @ (c_2Ewords_2En2w @ X0 @ X2)) != (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ X1 @ X2))) & ($true = (c_2Earithmetic_2E_3C_3D @ X2 @ X1))) => (((c_2Ewords_2Eword__sub @ sK2 @ (c_2Ewords_2En2w @ sK2 @ sK3) @ (c_2Ewords_2En2w @ sK2 @ sK4)) != (c_2Ewords_2En2w @ sK2 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4))) & ($true = (c_2Earithmetic_2E_3C_3D @ sK4 @ sK3)))),
% 1.80/1.50 introduced(definition,[],[choice_axiom])).
% 1.80/1.50 thf(f61,plain,(
% 1.80/1.50 ? [X0 : $tType,X1 : tyop_2Enum_2Enum,X2 : tyop_2Enum_2Enum] : (((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ X1) @ (c_2Ewords_2En2w @ X0 @ X2)) != (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ X1 @ X2))) & ($true = (c_2Earithmetic_2E_3C_3D @ X2 @ X1)))),
% 1.80/1.50 inference(ennf_transformation,[status(thm)],[f39])).
% 1.80/1.50 thf(f39,plain,(
% 1.80/1.50 ~! [X0 : $tType,X1 : tyop_2Enum_2Enum,X2 : tyop_2Enum_2Enum] : (($true = (c_2Earithmetic_2E_3C_3D @ X2 @ X1)) => ((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ X1) @ (c_2Ewords_2En2w @ X0 @ X2)) = (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ X1 @ X2))))),
% 1.80/1.50 inference(fool_elimination,[status(thm)],[f38])).
% 1.80/1.50 thf(f38,plain,(
% 1.80/1.50 ~! [X0 : $tType,X1 : tyop_2Enum_2Enum,X2 : tyop_2Enum_2Enum] : ((c_2Earithmetic_2E_3C_3D @ X2 @ X1) => ((c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ X1) @ (c_2Ewords_2En2w @ X0 @ X2)) = (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ X1 @ X2))))),
% 1.80/1.50 inference(rectify,[status(thm)],[f20])).
% 1.80/1.50 thf(f20,negated_conjecture,(
% 1.80/1.50 ~! [X0 : $tType,X29 : tyop_2Enum_2Enum,X30 : tyop_2Enum_2Enum] : ((c_2Earithmetic_2E_3C_3D @ X30 @ X29) => ((c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ X29 @ X30)) = (c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ X29) @ (c_2Ewords_2En2w @ X0 @ X30))))),
% 1.80/1.50 inference(negated_conjecture,[status(cth)],[f19])).
% 1.80/1.50 thf(f19,conjecture,(
% 1.80/1.50 ! [X0 : $tType,X29 : tyop_2Enum_2Enum,X30 : tyop_2Enum_2Enum] : ((c_2Earithmetic_2E_3C_3D @ X30 @ X29) => ((c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2D @ X29 @ X30)) = (c_2Ewords_2Eword__sub @ X0 @ (c_2Ewords_2En2w @ X0 @ X29) @ (c_2Ewords_2En2w @ X0 @ X30))))),
% 1.80/1.50 file('/export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2THF_19694.p',thm_2Ewords_2En2w__sub)).
% 1.80/1.50 thf(f142,plain,(
% 1.80/1.50 ( ! [X1 : $tType,X2 : tyop_2Enum_2Enum,X3 : tyop_2Enum_2Enum] : (((c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X1 @ (c_2Earithmetic_2E_3C_3D @ X3 @ X2) @ (c_2Ewords_2En2w @ X1 @ (c_2Earithmetic_2E_2D @ X2 @ X3)) @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ (c_2Earithmetic_2E_2D @ X3 @ X2)))) = (c_2Ewords_2Eword__add @ X1 @ (c_2Ewords_2En2w @ X1 @ X2) @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ X3))))) )),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f80])).
% 1.80/1.50 thf(f80,plain,(
% 1.80/1.50 ! [X0 : $tType,X1 : $tType] : (! [X2 : tyop_2Enum_2Enum,X3 : tyop_2Enum_2Enum] : ((c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X1 @ (c_2Earithmetic_2E_3C_3D @ X3 @ X2) @ (c_2Ewords_2En2w @ X1 @ (c_2Earithmetic_2E_2D @ X2 @ X3)) @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ (c_2Earithmetic_2E_2D @ X3 @ X2)))) = (c_2Ewords_2Eword__add @ X1 @ (c_2Ewords_2En2w @ X1 @ X2) @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ X3)))) & ! [X4 : tyop_2Enum_2Enum,X5 : tyop_2Enum_2Enum] : ((c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2B @ X4 @ X5))) = (c_2Ewords_2Eword__add @ X0 @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ X4)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ X5)))))),
% 1.80/1.50 inference(rectify,[status(thm)],[f52])).
% 1.80/1.50 thf(f52,plain,(
% 1.80/1.50 ! [X0 : $tType,X1 : $tType] : (! [X4 : tyop_2Enum_2Enum,X5 : tyop_2Enum_2Enum] : ((c_2Ewords_2Eword__add @ X1 @ (c_2Ewords_2En2w @ X1 @ X4) @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ X5))) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X1 @ (c_2Earithmetic_2E_3C_3D @ X5 @ X4) @ (c_2Ewords_2En2w @ X1 @ (c_2Earithmetic_2E_2D @ X4 @ X5)) @ (c_2Ewords_2Eword__2comp @ X1 @ (c_2Ewords_2En2w @ X1 @ (c_2Earithmetic_2E_2D @ X5 @ X4))))) & ! [X2 : tyop_2Enum_2Enum,X3 : tyop_2Enum_2Enum] : ((c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2B @ X2 @ X3))) = (c_2Ewords_2Eword__add @ X0 @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ X2)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ X3)))))),
% 1.80/1.50 inference(rectify,[status(thm)],[f18])).
% 1.80/1.50 thf(f18,axiom,(
% 1.80/1.50 ! [X0 : $tType,X24 : $tType] : (! [X25 : tyop_2Enum_2Enum,X26 : tyop_2Enum_2Enum] : ((c_2Ewords_2Eword__add @ X0 @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ X25)) @ (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ X26))) = (c_2Ewords_2Eword__2comp @ X0 @ (c_2Ewords_2En2w @ X0 @ (c_2Earithmetic_2E_2B @ X25 @ X26)))) & ! [X27 : tyop_2Enum_2Enum,X28 : tyop_2Enum_2Enum] : ((c_2Ewords_2Eword__add @ X24 @ (c_2Ewords_2En2w @ X24 @ X27) @ (c_2Ewords_2Eword__2comp @ X24 @ (c_2Ewords_2En2w @ X24 @ X28))) = (c_2Ebool_2ECOND @ tyop_2Efcp_2Ecart @ $o @ X24 @ (c_2Earithmetic_2E_3C_3D @ X28 @ X27) @ (c_2Ewords_2En2w @ X24 @ (c_2Earithmetic_2E_2D @ X27 @ X28)) @ (c_2Ewords_2Eword__2comp @ X24 @ (c_2Ewords_2En2w @ X24 @ (c_2Earithmetic_2E_2D @ X28 @ X27))))))),
% 1.80/1.50 file('/export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2THF_19694.p',thm_2Ewords_2EWORD__LITERAL__ADD)).
% 1.80/1.50 thf(f216,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : $o,X6 : X0,X4 : X0,X5 : X0] : (((c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X6) = (c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X5)) | ((~ X2) = $true)) )),
% 1.80/1.50 inference(equality_resolution,[status(thm)],[f215])).
% 1.80/1.50 thf(f215,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : $o,X1 : $o,X6 : X0,X4 : X0,X5 : X0] : (((c_2Ebool_2ECOND @ X0 @ X1 @ X4 @ X5) = (c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X6)) | ((~ X2) = $true) | (X1 != X2)) )),
% 1.80/1.50 inference(equality_resolution,[status(thm)],[f155])).
% 1.80/1.50 thf(f155,plain,(
% 1.80/1.50 ( ! [X0 : $tType,X2 : $o,X3 : X0,X1 : $o,X6 : X0,X4 : X0,X5 : X0] : ((X3 != X4) | ((c_2Ebool_2ECOND @ X0 @ X1 @ X3 @ X5) = (c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X6)) | ((~ X2) = $true) | (X1 != X2)) )),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f58])).
% 1.80/1.50 thf(f58,plain,(
% 1.80/1.50 ! [X0 : $tType,X1 : $o,X2 : $o,X3 : X0,X4 : X0,X5 : X0,X6 : X0] : ((($true = X2) & (X3 != X4)) | ((c_2Ebool_2ECOND @ X0 @ X1 @ X3 @ X5) = (c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X6)) | ((X5 != X6) & ((~ X2) = $true)) | (X1 != X2))),
% 1.80/1.50 inference(flattening,[status(thm)],[f57])).
% 1.80/1.50 thf(f57,plain,(
% 1.80/1.50 ! [X0 : $tType,X1 : $o,X2 : $o,X3 : X0,X4 : X0,X5 : X0,X6 : X0] : (((c_2Ebool_2ECOND @ X0 @ X1 @ X3 @ X5) = (c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X6)) | ((($true = X2) & (X3 != X4)) | ((X5 != X6) & ((~ X2) = $true)) | (X1 != X2)))),
% 1.80/1.50 inference(ennf_transformation,[status(thm)],[f49])).
% 1.80/1.50 thf(f49,plain,(
% 1.80/1.50 ! [X0 : $tType,X1 : $o,X2 : $o,X3 : X0,X4 : X0,X5 : X0,X6 : X0] : (((($true = X2) => (X3 = X4)) & (((~ X2) = $true) => (X5 = X6)) & (X1 = X2)) => ((c_2Ebool_2ECOND @ X0 @ X1 @ X3 @ X5) = (c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X6)))),
% 1.80/1.50 inference(fool_elimination,[status(thm)],[f48])).
% 1.80/1.50 thf(f48,plain,(
% 1.80/1.50 ! [X0 : $tType,X1 : $o,X2 : $o,X3 : X0,X4 : X0,X5 : X0,X6 : X0] : (((X2 => (X3 = X4)) & ((~ X2) => (X5 = X6)) & (X1 = X2)) => ((c_2Ebool_2ECOND @ X0 @ X1 @ X3 @ X5) = (c_2Ebool_2ECOND @ X0 @ X2 @ X4 @ X6)))),
% 1.80/1.50 inference(rectify,[status(thm)],[f15])).
% 1.80/1.50 thf(f15,axiom,(
% 1.80/1.50 ! [X0 : $tType,X14 : $o,X15 : $o,X16 : X0,X17 : X0,X18 : X0,X19 : X0] : (((X15 => (X16 = X17)) & ((~ X15) => (X18 = X19)) & (X14 = X15)) => ((c_2Ebool_2ECOND @ X0 @ X14 @ X16 @ X18) = (c_2Ebool_2ECOND @ X0 @ X15 @ X17 @ X19)))),
% 1.80/1.50 file('/export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2THF_19694.p',thm_2Ebool_2ECOND__CONG)).
% 1.80/1.50 thf(f146,plain,(
% 1.80/1.50 ((c_2Ewords_2Eword__sub @ sK2 @ (c_2Ewords_2En2w @ sK2 @ sK3) @ (c_2Ewords_2En2w @ sK2 @ sK4)) != (c_2Ewords_2En2w @ sK2 @ (c_2Earithmetic_2E_2D @ sK3 @ sK4)))),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f86])).
% 1.80/1.50 thf(f438,plain,(
% 1.80/1.50 spl5_3 | spl5_1),
% 1.80/1.50 inference(avatar_split_clause,[status(thm)],[f425,f287,f313])).
% 1.80/1.50 thf(f287,definition,(
% 1.80/1.50 spl5_1 <=> (c_2Ebool_2EF = $true)),
% 1.80/1.50 introduced(definition,[new_symbols(naming,[spl5_1])],[avatar_definition])).
% 1.80/1.50 thf(f425,plain,(
% 1.80/1.50 (c_2Ebool_2ET = $true) | spl5_1),
% 1.80/1.50 inference(trivial_inequality_removal,[status(thm)],[f421])).
% 1.80/1.50 thf(f421,plain,(
% 1.80/1.50 (c_2Ebool_2ET = $true) | ($true != $true) | spl5_1),
% 1.80/1.50 inference(superposition,[status(thm)],[f289,f111])).
% 1.80/1.50 thf(f111,plain,(
% 1.80/1.50 ( ! [X0 : $o] : (($true = X0) | (c_2Ebool_2ET = $true)) )),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f76])).
% 1.80/1.50 thf(f76,plain,(
% 1.80/1.50 ! [X0 : $o] : (((c_2Ebool_2ET = $true) | (($true != X0) & ($true = X0))) & (($true = X0) | ($true != X0) | (c_2Ebool_2ET != $true)) & ((c_2Ebool_2ET = $true) | ($true != X0) | (c_2Ebool_2ET != $true)) & ((c_2Ebool_2ET = $true) | ((c_2Ebool_2ET != $true) & ($true = X0))) & ((c_2Ebool_2ET = $true) | ((c_2Ebool_2EF = $true) & ($true != X0))) & ((c_2Ebool_2EF != $true) | ($true = X0) | (c_2Ebool_2ET != $true)) & ((c_2Ebool_2ET != $true) | ($true = X0) | ($true != X0)) & (($true = X0) | ((c_2Ebool_2ET = $true) & ($true != X0))) & (($true = (~ X0)) | (($true = X0) & (c_2Ebool_2EF != $true))) & (($true != X0) | (c_2Ebool_2EF = $true) | ($true != (~ X0))))),
% 1.80/1.50 inference(flattening,[status(thm)],[f75])).
% 1.80/1.50 thf(f75,plain,(
% 1.80/1.50 ! [X0 : $o] : ((((c_2Ebool_2ET = $true) | (($true != X0) & ($true = X0))) & ((($true = X0) | ($true != X0)) | (c_2Ebool_2ET != $true))) & ((((c_2Ebool_2ET = $true) | ($true != X0)) | (c_2Ebool_2ET != $true)) & ((c_2Ebool_2ET = $true) | ((c_2Ebool_2ET != $true) & ($true = X0)))) & (((c_2Ebool_2ET = $true) | ((c_2Ebool_2EF = $true) & ($true != X0))) & (((c_2Ebool_2EF != $true) | ($true = X0)) | (c_2Ebool_2ET != $true))) & ((((c_2Ebool_2ET != $true) | ($true = X0)) | ($true != X0)) & (($true = X0) | ((c_2Ebool_2ET = $true) & ($true != X0)))) & ((($true = (~ X0)) | (($true = X0) & (c_2Ebool_2EF != $true))) & ((($true != X0) | (c_2Ebool_2EF = $true)) | ($true != (~ X0)))))),
% 1.80/1.50 inference(nnf_transformation,[status(thm)],[f56])).
% 1.80/1.50 thf(f56,plain,(
% 1.80/1.50 ! [X0 : $o] : (((c_2Ebool_2ET = $true) <=> (($true = X0) | ($true != X0))) & (((c_2Ebool_2ET = $true) | ($true != X0)) <=> (c_2Ebool_2ET = $true)) & ((c_2Ebool_2ET = $true) <=> ((c_2Ebool_2EF != $true) | ($true = X0))) & (((c_2Ebool_2ET != $true) | ($true = X0)) <=> ($true = X0)) & (($true = (~ X0)) <=> (($true != X0) | (c_2Ebool_2EF = $true))))),
% 1.80/1.50 inference(ennf_transformation,[status(thm)],[f23])).
% 1.80/1.50 thf(f23,plain,(
% 1.80/1.50 ! [X0 : $o] : ((($true = X0) <=> ((c_2Ebool_2ET = $true) => ($true = X0))) & ((c_2Ebool_2ET = $true) <=> (($true = X0) => (c_2Ebool_2ET = $true))) & ((($true = X0) => (c_2Ebool_2EF = $true)) <=> ($true = (~ X0))) & ((($true = X0) => ($true = X0)) <=> (c_2Ebool_2ET = $true)) & (((c_2Ebool_2EF = $true) => ($true = X0)) <=> (c_2Ebool_2ET = $true)))),
% 1.80/1.50 inference(fool_elimination,[status(thm)],[f22])).
% 1.80/1.50 thf(f22,plain,(
% 1.80/1.50 ! [X0 : $o] : ((c_2Ebool_2ET <=> (c_2Ebool_2EF => X0)) & ((~ X0) <=> (X0 => c_2Ebool_2EF)) & (c_2Ebool_2ET <=> (X0 => X0)) & (X0 <=> (c_2Ebool_2ET => X0)) & ((X0 => c_2Ebool_2ET) <=> c_2Ebool_2ET))),
% 1.80/1.50 inference(rectify,[status(thm)],[f9])).
% 1.80/1.50 thf(f9,axiom,(
% 1.80/1.50 ! [X5 : $o] : ((c_2Ebool_2ET <=> (c_2Ebool_2EF => X5)) & ((~ X5) <=> (X5 => c_2Ebool_2EF)) & (c_2Ebool_2ET <=> (X5 => X5)) & (X5 <=> (c_2Ebool_2ET => X5)) & ((X5 => c_2Ebool_2ET) <=> c_2Ebool_2ET))),
% 1.80/1.50 file('/export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2THF_19694.p',thm_2Ebool_2EIMP__CLAUSES)).
% 1.80/1.50 thf(f289,plain,(
% 1.80/1.50 (c_2Ebool_2EF != $true) | spl5_1),
% 1.80/1.50 inference(avatar_component_clause,[status(thm)],[f287])).
% 1.80/1.50 thf(f414,plain,(
% 1.80/1.50 ~spl5_1),
% 1.80/1.50 inference(avatar_contradiction_clause,[status(thm)],[f413])).
% 1.80/1.50 thf(f413,plain,(
% 1.80/1.50 $false | ~spl5_1),
% 1.80/1.50 inference(trivial_inequality_removal,[status(thm)],[f410])).
% 1.80/1.50 thf(f410,plain,(
% 1.80/1.50 ($true != $true) | ~spl5_1),
% 1.80/1.50 inference(superposition,[status(thm)],[f247,f288])).
% 1.80/1.50 thf(f288,plain,(
% 1.80/1.50 (c_2Ebool_2EF = $true) | ~spl5_1),
% 1.80/1.50 inference(avatar_component_clause,[status(thm)],[f287])).
% 1.80/1.50 thf(f247,plain,(
% 1.80/1.50 (c_2Ebool_2EF != $true)),
% 1.80/1.50 inference(trivial_inequality_removal,[status(thm)],[f246])).
% 1.80/1.50 thf(f246,plain,(
% 1.80/1.50 ($true = $false) | (c_2Ebool_2EF != $true)),
% 1.80/1.50 inference(boolean_simplification,[status(thm)],[f186])).
% 1.80/1.50 thf(f186,plain,(
% 1.80/1.50 ((~ $true) = $true) | (c_2Ebool_2EF != $true)),
% 1.80/1.50 inference(equality_resolution,[status(thm)],[f133])).
% 1.80/1.50 thf(f133,plain,(
% 1.80/1.50 ( ! [X0 : $o] : (($true = (~ X0)) | ($true != X0) | (c_2Ebool_2EF != $true)) )),
% 1.80/1.50 inference(cnf_transformation,[status(thm)],[f79])).
% 1.80/1.50 thf(f79,plain,(
% 1.80/1.50 ! [X0 : $o] : ((($true = (~ X0)) | (((c_2Ebool_2EF != $true) | ($true != X0)) & ((c_2Ebool_2EF = $true) | ($true = X0)))) & (((($true = X0) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | ($true != X0))) | ($true != (~ X0))) & ((((c_2Ebool_2EF = $true) | ($true != X0)) & (($true = X0) | (c_2Ebool_2EF != $true))) | ($true != (~ X0))) & (($true = (~ X0)) | ((($true != X0) | (c_2Ebool_2EF != $true)) & (($true = X0) | (c_2Ebool_2EF = $true)))) & ((((c_2Ebool_2ET = $true) | ($true != X0)) & (($true = X0) | (c_2Ebool_2ET != $true))) | ($true != X0)) & (($true = X0) | ((($true != X0) | (c_2Ebool_2ET != $true)) & (($true = X0) | (c_2Ebool_2ET = $true)))) & (((($true = X0) | (c_2Ebool_2ET != $true)) & ((c_2Ebool_2ET = $true) | ($true != X0))) | ($true != X0)) & (($true = X0) | (((c_2Ebool_2ET != $true) | ($true != X0)) & ((c_2Ebool_2ET = $true) | ($true = X0)))))),
% 1.80/1.50 inference(flattening,[status(thm)],[f78])).
% 1.80/1.50 thf(f78,plain,(
% 1.80/1.50 ! [X0 : $o] : (((($true = (~ X0)) | (((c_2Ebool_2EF != $true) | ($true != X0)) & ((c_2Ebool_2EF = $true) | ($true = X0)))) & (((($true = X0) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | ($true != X0))) | ($true != (~ X0)))) & (((((c_2Ebool_2EF = $true) | ($true != X0)) & (($true = X0) | (c_2Ebool_2EF != $true))) | ($true != (~ X0))) & (($true = (~ X0)) | ((($true != X0) | (c_2Ebool_2EF != $true)) & (($true = X0) | (c_2Ebool_2EF = $true))))) & (((((c_2Ebool_2ET = $true) | ($true != X0)) & (($true = X0) | (c_2Ebool_2ET != $true))) | ($true != X0)) & (($true = X0) | ((($true != X0) | (c_2Ebool_2ET != $true)) & (($true = X0) | (c_2Ebool_2ET = $true))))) & ((((($true = X0) | (c_2Ebool_2ET != $true)) & ((c_2Ebool_2ET = $true) | ($true != X0))) | ($true != X0)) & (($true = X0) | (((c_2Ebool_2ET != $true) | ($true != X0)) & ((c_2Ebool_2ET = $true) | ($true = X0))))))),
% 1.80/1.50 inference(nnf_transformation,[status(thm)],[f31])).
% 1.80/1.50 thf(f31,plain,(
% 1.80/1.50 ! [X0 : $o] : ((($true = (~ X0)) <=> (($true = X0) <=> (c_2Ebool_2EF = $true))) & (((c_2Ebool_2EF = $true) <=> ($true = X0)) <=> ($true = (~ X0))) & (((c_2Ebool_2ET = $true) <=> ($true = X0)) <=> ($true = X0)) & ((($true = X0) <=> (c_2Ebool_2ET = $true)) <=> ($true = X0)))),
% 1.80/1.50 inference(fool_elimination,[status(thm)],[f30])).
% 1.80/1.50 thf(f30,plain,(
% 1.80/1.50 ! [X0 : $o] : ((X0 <=> (c_2Ebool_2ET = X0)) & ((c_2Ebool_2ET = X0) <=> X0) & ((c_2Ebool_2EF = X0) <=> (~ X0)) & ((c_2Ebool_2EF = X0) <=> (~ X0)))),
% 1.80/1.50 inference(rectify,[status(thm)],[f12])).
% 1.80/1.50 thf(f12,axiom,(
% 1.80/1.50 ! [X5 : $o] : ((X5 <=> (c_2Ebool_2ET = X5)) & ((c_2Ebool_2ET = X5) <=> X5) & ((c_2Ebool_2EF = X5) <=> (~ X5)) & ((c_2Ebool_2EF = X5) <=> (~ X5)))),
% 1.80/1.50 file('/export/starexec/sandbox/tmp/tmp.DZjFp9JrJM/DTF2THF_19694.p',thm_2Ebool_2EEQ__CLAUSES)).
% 1.80/1.50 % SZS output end Proof for DTF2THF_19694
% 1.80/1.50 % (19826)------------------------------
% 1.80/1.50 % (19826)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (19826)Termination reason: Refutation
% 1.80/1.50
% 1.80/1.50 % (19826)Memory used [KB]: 5884
% 1.80/1.50 % (19826)Time elapsed: 0.029 s
% 1.80/1.50 % (19826)Instructions burned: 92 (million)
% 1.80/1.50 % (19826)------------------------------
% 1.80/1.50 % (19826)------------------------------
% 1.80/1.50 % (19800)Success in time 0.07 s
%------------------------------------------------------------------------------