%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SEV260^5 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n028.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 09:40:41 AM UTC 2026
% Result : Theorem 1.57s 1.37s
% Output : Refutation 1.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 7
% Syntax : Number of formulae : 29 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 687 ( 338 equ; 0 cnn)
% Maximal formula atoms : 64 ( 23 avg)
% Number of connectives : 1108 ( 196 ~; 109 |; 214 &; 482 @)
% ( 0 <=>; 91 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 9 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 363 ( 363 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 11 usr; 5 con; 0-2 aty)
% ( 0 !!; 16 ??; 0 @@+; 0 @@-)
% Number of variables : 467 ( 178 ^; 235 !; 54 ?; 467 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
a: $tType ).
thf(type_def_7,type,
b: $tType ).
thf(func_def_0,type,
a: $tType ).
thf(func_def_1,type,
b: $tType ).
thf(func_def_11,type,
sK0: ( a > $o ) > $o ).
thf(func_def_12,type,
sK1: a > b ).
thf(func_def_13,type,
sK2: ( b > $o ) > $o ).
thf(func_def_14,type,
sK3: b > $o ).
thf(func_def_15,type,
sK4: a > $o ).
thf(func_def_16,type,
sK5: a > $o ).
thf(func_def_17,type,
sK6: ( ( b > $o ) > $o ) > b > $o ).
thf(func_def_18,type,
sK7: ( ( a > $o ) > $o ) > a > $o ).
thf(func_def_20,type,
ph9:
!>[X0: $tType] : X0 ).
thf(func_def_21,type,
sK10: a ).
thf(func_def_22,type,
sK11: a ).
thf(f62,plain,
$false,
inference(subsumption_resolution,[status(thm)],[f61,f34]) ).
thf(f34,plain,
( ( sK2
@ ^ [Y0: b] :
~ ( sK3 @ Y0 ) )
= $true ),
inference(equality_resolution,[status(thm)],[f28]) ).
thf(f28,plain,
! [X6: b > $o] :
( ( ( sK2 @ X6 )
= $true )
| ( ( ^ [Y0: b] :
~ ( sK3 @ Y0 ) )
!= X6 ) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
thf(f16,plain,
( ( ( ^ [Y0: a] : ( sK3 @ ( sK1 @ Y0 ) ) )
= sK4 )
& ( ( sK0 @ sK5 )
!= $true )
& ( sK5
= ( ^ [Y0: a] :
~ ( sK4 @ Y0 ) ) )
& ! [X6: b > $o] :
( ( ( sK2 @ X6 )
= $true )
| ( ( ^ [Y0: b] :
~ ( sK3 @ Y0 ) )
!= X6 ) )
& ! [X7: a > $o] :
( ( ( ^ [Y0: a] : $false )
!= X7 )
| ( ( sK0 @ X7 )
= $true ) )
& ! [X8: b > $o] :
( ( ( ^ [Y0: b] : $false )
!= X8 )
| ( ( sK2 @ X8 )
= $true ) )
& ! [X9: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
!= X9 )
| ( ( sK0 @ X9 )
= $true ) )
& ! [X10: b > $o,X11: ( b > $o ) > $o] :
( ( ( ( X11 @ ( sK6 @ X11 ) )
= $true )
& ( ( sK2 @ ( sK6 @ X11 ) )
!= $true ) )
| ( ( sK2 @ X10 )
= $true )
| ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X11 @ Y1 ) ) ) )
!= X10 ) )
& ! [X13: a > $o,X14: a > $o,X15: a > $o] :
( ( ( ^ [Y0: a] :
( ( X13 @ Y0 )
& ( X14 @ Y0 ) ) )
!= X15 )
| ( ( sK0 @ X15 )
= $true )
| ( ( sK0 @ X13 )
!= $true )
| ( ( sK0 @ X14 )
!= $true ) )
& ! [X16: ( a > $o ) > $o,X17: a > $o] :
( ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X16 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
!= X17 )
| ( ( sK0 @ X17 )
= $true )
| ( ( $true
= ( X16 @ ( sK7 @ X16 ) ) )
& ( ( sK0 @ ( sK7 @ X16 ) )
!= $true ) ) )
& ! [X19: b > $o,X20: b > $o,X21: b > $o] :
( ( ( sK2 @ X20 )
= $true )
| ( ( sK2 @ X19 )
!= $true )
| ( ( ^ [Y0: b] :
( ( X21 @ Y0 )
& ( X19 @ Y0 ) ) )
!= X20 )
| ( ( sK2 @ X21 )
!= $true ) )
& ! [X22: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
!= X22 )
| ( ( sK2 @ X22 )
= $true ) )
& ! [X23: b > $o] :
( ( ( sK2 @ X23 )
!= $true )
| ! [X24: a > $o] :
( ( ( ^ [Y0: a] : ( X23 @ ( sK1 @ Y0 ) ) )
!= X24 )
| ( ( sK0 @ X24 )
= $true ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7])],[f9,f15,f14,f13,f12,f11,f10]) ).
thf(f10,plain,
( ? [X0: ( a > $o ) > $o,X1: a > b,X2: ( b > $o ) > $o] :
( ? [X3: b > $o] :
( ? [X4: a > $o] :
( ( ( ^ [Y0: a] : ( X3 @ ( X1 @ Y0 ) ) )
= X4 )
& ? [X5: a > $o] :
( ( ( X0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X4 @ Y0 ) )
= X5 ) ) )
& ! [X6: b > $o] :
( ( ( X2 @ X6 )
= $true )
| ( ( ^ [Y0: b] :
~ ( X3 @ Y0 ) )
!= X6 ) ) )
& ! [X7: a > $o] :
( ( ( ^ [Y0: a] : $false )
!= X7 )
| ( ( X0 @ X7 )
= $true ) )
& ! [X8: b > $o] :
( ( ( ^ [Y0: b] : $false )
!= X8 )
| ( ( X2 @ X8 )
= $true ) )
& ! [X9: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
!= X9 )
| ( $true
= ( X0 @ X9 ) ) )
& ! [X10: b > $o,X11: ( b > $o ) > $o] :
( ? [X12: b > $o] :
( ( ( X11 @ X12 )
= $true )
& ( ( X2 @ X12 )
!= $true ) )
| ( ( X2 @ X10 )
= $true )
| ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X11 @ Y1 ) ) ) )
!= X10 ) )
& ! [X13: a > $o,X14: a > $o,X15: a > $o] :
( ( ( ^ [Y0: a] :
( ( X13 @ Y0 )
& ( X14 @ Y0 ) ) )
!= X15 )
| ( ( X0 @ X15 )
= $true )
| ( ( X0 @ X13 )
!= $true )
| ( ( X0 @ X14 )
!= $true ) )
& ! [X16: ( a > $o ) > $o,X17: a > $o] :
( ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X16 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
!= X17 )
| ( ( X0 @ X17 )
= $true )
| ? [X18: a > $o] :
( ( ( X16 @ X18 )
= $true )
& ( ( X0 @ X18 )
!= $true ) ) )
& ! [X19: b > $o,X20: b > $o,X21: b > $o] :
( ( ( X2 @ X20 )
= $true )
| ( ( X2 @ X19 )
!= $true )
| ( ( ^ [Y0: b] :
( ( X21 @ Y0 )
& ( X19 @ Y0 ) ) )
!= X20 )
| ( ( X2 @ X21 )
!= $true ) )
& ! [X22: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
!= X22 )
| ( ( X2 @ X22 )
= $true ) )
& ! [X23: b > $o] :
( ( ( X2 @ X23 )
!= $true )
| ! [X24: a > $o] :
( ( ( ^ [Y0: a] : ( X23 @ ( X1 @ Y0 ) ) )
!= X24 )
| ( ( X0 @ X24 )
= $true ) ) ) )
=> ( ? [X3: b > $o] :
( ? [X4: a > $o] :
( ( ( ^ [Y0: a] : ( X3 @ ( sK1 @ Y0 ) ) )
= X4 )
& ? [X5: a > $o] :
( ( ( sK0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X4 @ Y0 ) )
= X5 ) ) )
& ! [X6: b > $o] :
( ( ( sK2 @ X6 )
= $true )
| ( ( ^ [Y0: b] :
~ ( X3 @ Y0 ) )
!= X6 ) ) )
& ! [X7: a > $o] :
( ( ( ^ [Y0: a] : $false )
!= X7 )
| ( ( sK0 @ X7 )
= $true ) )
& ! [X8: b > $o] :
( ( ( ^ [Y0: b] : $false )
!= X8 )
| ( ( sK2 @ X8 )
= $true ) )
& ! [X9: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
!= X9 )
| ( ( sK0 @ X9 )
= $true ) )
& ! [X11: ( b > $o ) > $o,X10: b > $o] :
( ? [X12: b > $o] :
( ( ( X11 @ X12 )
= $true )
& ( ( sK2 @ X12 )
!= $true ) )
| ( ( sK2 @ X10 )
= $true )
| ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X11 @ Y1 ) ) ) )
!= X10 ) )
& ! [X15: a > $o,X14: a > $o,X13: a > $o] :
( ( ( ^ [Y0: a] :
( ( X13 @ Y0 )
& ( X14 @ Y0 ) ) )
!= X15 )
| ( ( sK0 @ X15 )
= $true )
| ( ( sK0 @ X13 )
!= $true )
| ( ( sK0 @ X14 )
!= $true ) )
& ! [X17: a > $o,X16: ( a > $o ) > $o] :
( ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X16 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
!= X17 )
| ( ( sK0 @ X17 )
= $true )
| ? [X18: a > $o] :
( ( ( X16 @ X18 )
= $true )
& ( ( sK0 @ X18 )
!= $true ) ) )
& ! [X21: b > $o,X20: b > $o,X19: b > $o] :
( ( ( sK2 @ X20 )
= $true )
| ( ( sK2 @ X19 )
!= $true )
| ( ( ^ [Y0: b] :
( ( X21 @ Y0 )
& ( X19 @ Y0 ) ) )
!= X20 )
| ( ( sK2 @ X21 )
!= $true ) )
& ! [X22: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
!= X22 )
| ( ( sK2 @ X22 )
= $true ) )
& ! [X23: b > $o] :
( ( ( sK2 @ X23 )
!= $true )
| ! [X24: a > $o] :
( ( ( ^ [Y0: a] : ( X23 @ ( sK1 @ Y0 ) ) )
!= X24 )
| ( ( sK0 @ X24 )
= $true ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f11,plain,
( ? [X3: b > $o] :
( ? [X4: a > $o] :
( ( ( ^ [Y0: a] : ( X3 @ ( sK1 @ Y0 ) ) )
= X4 )
& ? [X5: a > $o] :
( ( ( sK0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X4 @ Y0 ) )
= X5 ) ) )
& ! [X6: b > $o] :
( ( ( sK2 @ X6 )
= $true )
| ( ( ^ [Y0: b] :
~ ( X3 @ Y0 ) )
!= X6 ) ) )
=> ( ? [X4: a > $o] :
( ( ( ^ [Y0: a] : ( sK3 @ ( sK1 @ Y0 ) ) )
= X4 )
& ? [X5: a > $o] :
( ( ( sK0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X4 @ Y0 ) )
= X5 ) ) )
& ! [X6: b > $o] :
( ( ( sK2 @ X6 )
= $true )
| ( ( ^ [Y0: b] :
~ ( sK3 @ Y0 ) )
!= X6 ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f12,plain,
( ? [X4: a > $o] :
( ( ( ^ [Y0: a] : ( sK3 @ ( sK1 @ Y0 ) ) )
= X4 )
& ? [X5: a > $o] :
( ( ( sK0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X4 @ Y0 ) )
= X5 ) ) )
=> ( ( ( ^ [Y0: a] : ( sK3 @ ( sK1 @ Y0 ) ) )
= sK4 )
& ? [X5: a > $o] :
( ( ( sK0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( sK4 @ Y0 ) )
= X5 ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f13,plain,
( ? [X5: a > $o] :
( ( ( sK0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( sK4 @ Y0 ) )
= X5 ) )
=> ( ( ( sK0 @ sK5 )
!= $true )
& ( sK5
= ( ^ [Y0: a] :
~ ( sK4 @ Y0 ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f14,plain,
! [X11: ( b > $o ) > $o] :
( ? [X12: b > $o] :
( ( ( X11 @ X12 )
= $true )
& ( ( sK2 @ X12 )
!= $true ) )
=> ( ( ( X11 @ ( sK6 @ X11 ) )
= $true )
& ( ( sK2 @ ( sK6 @ X11 ) )
!= $true ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f15,plain,
! [X16: ( a > $o ) > $o] :
( ? [X18: a > $o] :
( ( ( X16 @ X18 )
= $true )
& ( ( sK0 @ X18 )
!= $true ) )
=> ( ( $true
= ( X16 @ ( sK7 @ X16 ) ) )
& ( ( sK0 @ ( sK7 @ X16 ) )
!= $true ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f9,plain,
? [X0: ( a > $o ) > $o,X1: a > b,X2: ( b > $o ) > $o] :
( ? [X3: b > $o] :
( ? [X4: a > $o] :
( ( ( ^ [Y0: a] : ( X3 @ ( X1 @ Y0 ) ) )
= X4 )
& ? [X5: a > $o] :
( ( ( X0 @ X5 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X4 @ Y0 ) )
= X5 ) ) )
& ! [X6: b > $o] :
( ( ( X2 @ X6 )
= $true )
| ( ( ^ [Y0: b] :
~ ( X3 @ Y0 ) )
!= X6 ) ) )
& ! [X7: a > $o] :
( ( ( ^ [Y0: a] : $false )
!= X7 )
| ( ( X0 @ X7 )
= $true ) )
& ! [X8: b > $o] :
( ( ( ^ [Y0: b] : $false )
!= X8 )
| ( ( X2 @ X8 )
= $true ) )
& ! [X9: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
!= X9 )
| ( $true
= ( X0 @ X9 ) ) )
& ! [X10: b > $o,X11: ( b > $o ) > $o] :
( ? [X12: b > $o] :
( ( ( X11 @ X12 )
= $true )
& ( ( X2 @ X12 )
!= $true ) )
| ( ( X2 @ X10 )
= $true )
| ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X11 @ Y1 ) ) ) )
!= X10 ) )
& ! [X13: a > $o,X14: a > $o,X15: a > $o] :
( ( ( ^ [Y0: a] :
( ( X13 @ Y0 )
& ( X14 @ Y0 ) ) )
!= X15 )
| ( ( X0 @ X15 )
= $true )
| ( ( X0 @ X13 )
!= $true )
| ( ( X0 @ X14 )
!= $true ) )
& ! [X16: ( a > $o ) > $o,X17: a > $o] :
( ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X16 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
!= X17 )
| ( ( X0 @ X17 )
= $true )
| ? [X18: a > $o] :
( ( ( X16 @ X18 )
= $true )
& ( ( X0 @ X18 )
!= $true ) ) )
& ! [X19: b > $o,X20: b > $o,X21: b > $o] :
( ( ( X2 @ X20 )
= $true )
| ( ( X2 @ X19 )
!= $true )
| ( ( ^ [Y0: b] :
( ( X21 @ Y0 )
& ( X19 @ Y0 ) ) )
!= X20 )
| ( ( X2 @ X21 )
!= $true ) )
& ! [X22: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
!= X22 )
| ( ( X2 @ X22 )
= $true ) )
& ! [X23: b > $o] :
( ( ( X2 @ X23 )
!= $true )
| ! [X24: a > $o] :
( ( ( ^ [Y0: a] : ( X23 @ ( X1 @ Y0 ) ) )
!= X24 )
| ( ( X0 @ X24 )
= $true ) ) ) ),
inference(rectify,[status(thm)],[f8]) ).
thf(f8,plain,
? [X0: ( a > $o ) > $o,X1: a > b,X2: ( b > $o ) > $o] :
( ? [X21: b > $o] :
( ? [X23: a > $o] :
( ( ( ^ [Y0: a] : ( X21 @ ( X1 @ Y0 ) ) )
= X23 )
& ? [X24: a > $o] :
( ( ( X0 @ X24 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X23 @ Y0 ) )
= X24 ) ) )
& ! [X22: b > $o] :
( ( ( X2 @ X22 )
= $true )
| ( ( ^ [Y0: b] :
~ ( X21 @ Y0 ) )
!= X22 ) ) )
& ! [X8: a > $o] :
( ( ( ^ [Y0: a] : $false )
!= X8 )
| ( ( X0 @ X8 )
= $true ) )
& ! [X17: b > $o] :
( ( ( ^ [Y0: b] : $false )
!= X17 )
| ( $true
= ( X2 @ X17 ) ) )
& ! [X7: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
!= X7 )
| ( ( X0 @ X7 )
= $true ) )
& ! [X11: b > $o,X12: ( b > $o ) > $o] :
( ? [X13: b > $o] :
( ( ( X12 @ X13 )
= $true )
& ( $true
!= ( X2 @ X13 ) ) )
| ( ( X2 @ X11 )
= $true )
| ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X12 @ Y1 ) ) ) )
!= X11 ) )
& ! [X14: a > $o,X15: a > $o,X16: a > $o] :
( ( ( ^ [Y0: a] :
( ( X14 @ Y0 )
& ( X15 @ Y0 ) ) )
!= X16 )
| ( ( X0 @ X16 )
= $true )
| ( ( X0 @ X14 )
!= $true )
| ( ( X0 @ X15 )
!= $true ) )
& ! [X3: ( a > $o ) > $o,X4: a > $o] :
( ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X3 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
!= X4 )
| ( ( X0 @ X4 )
= $true )
| ? [X5: a > $o] :
( ( ( X3 @ X5 )
= $true )
& ( ( X0 @ X5 )
!= $true ) ) )
& ! [X18: b > $o,X19: b > $o,X20: b > $o] :
( ( ( X2 @ X19 )
= $true )
| ( ( X2 @ X18 )
!= $true )
| ( ( ^ [Y0: b] :
( ( X20 @ Y0 )
& ( X18 @ Y0 ) ) )
!= X19 )
| ( ( X2 @ X20 )
!= $true ) )
& ! [X6: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
!= X6 )
| ( ( X2 @ X6 )
= $true ) )
& ! [X9: b > $o] :
( ( ( X2 @ X9 )
!= $true )
| ! [X10: a > $o] :
( ( ( ^ [Y0: a] : ( X9 @ ( X1 @ Y0 ) ) )
!= X10 )
| ( ( X0 @ X10 )
= $true ) ) ) ),
inference(flattening,[status(thm)],[f7]) ).
thf(f7,plain,
? [X0: ( a > $o ) > $o,X1: a > b,X2: ( b > $o ) > $o] :
( ? [X21: b > $o] :
( ? [X23: a > $o] :
( ( ( ^ [Y0: a] : ( X21 @ ( X1 @ Y0 ) ) )
= X23 )
& ? [X24: a > $o] :
( ( ( X0 @ X24 )
!= $true )
& ( ( ^ [Y0: a] :
~ ( X23 @ Y0 ) )
= X24 ) ) )
& ! [X22: b > $o] :
( ( ( X2 @ X22 )
= $true )
| ( ( ^ [Y0: b] :
~ ( X21 @ Y0 ) )
!= X22 ) ) )
& ! [X7: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
!= X7 )
| ( ( X0 @ X7 )
= $true ) )
& ! [X18: b > $o,X19: b > $o,X20: b > $o] :
( ( ( X2 @ X19 )
= $true )
| ( ( ^ [Y0: b] :
( ( X20 @ Y0 )
& ( X18 @ Y0 ) ) )
!= X19 )
| ( ( X2 @ X18 )
!= $true )
| ( ( X2 @ X20 )
!= $true ) )
& ! [X8: a > $o] :
( ( ( ^ [Y0: a] : $false )
!= X8 )
| ( ( X0 @ X8 )
= $true ) )
& ! [X3: ( a > $o ) > $o,X4: a > $o] :
( ( ( X0 @ X4 )
= $true )
| ? [X5: a > $o] :
( ( ( X3 @ X5 )
= $true )
& ( ( X0 @ X5 )
!= $true ) )
| ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X3 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
!= X4 ) )
& ! [X6: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
!= X6 )
| ( ( X2 @ X6 )
= $true ) )
& ! [X14: a > $o,X15: a > $o,X16: a > $o] :
( ( ( X0 @ X16 )
= $true )
| ( ( X0 @ X15 )
!= $true )
| ( ( ^ [Y0: a] :
( ( X14 @ Y0 )
& ( X15 @ Y0 ) ) )
!= X16 )
| ( ( X0 @ X14 )
!= $true ) )
& ! [X9: b > $o] :
( ( ( X2 @ X9 )
!= $true )
| ! [X10: a > $o] :
( ( ( ^ [Y0: a] : ( X9 @ ( X1 @ Y0 ) ) )
!= X10 )
| ( ( X0 @ X10 )
= $true ) ) )
& ! [X17: b > $o] :
( ( ( ^ [Y0: b] : $false )
!= X17 )
| ( $true
= ( X2 @ X17 ) ) )
& ! [X11: b > $o,X12: ( b > $o ) > $o] :
( ( ( X2 @ X11 )
= $true )
| ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X12 @ Y1 ) ) ) )
!= X11 )
| ? [X13: b > $o] :
( ( ( X12 @ X13 )
= $true )
& ( $true
!= ( X2 @ X13 ) ) ) ) ),
inference(ennf_transformation,[status(thm)],[f6]) ).
thf(f6,plain,
~ ! [X0: ( a > $o ) > $o,X1: a > b,X2: ( b > $o ) > $o] :
( ( ! [X7: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
= X7 )
=> ( ( X0 @ X7 )
= $true ) )
& ! [X18: b > $o,X19: b > $o,X20: b > $o] :
( ( ( ( ^ [Y0: b] :
( ( X20 @ Y0 )
& ( X18 @ Y0 ) ) )
= X19 )
& ( ( X2 @ X18 )
= $true )
& ( ( X2 @ X20 )
= $true ) )
=> ( ( X2 @ X19 )
= $true ) )
& ! [X8: a > $o] :
( ( ( ^ [Y0: a] : $false )
= X8 )
=> ( ( X0 @ X8 )
= $true ) )
& ! [X3: ( a > $o ) > $o,X4: a > $o] :
( ( ! [X5: a > $o] :
( ( ( X3 @ X5 )
= $true )
=> ( ( X0 @ X5 )
= $true ) )
& ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X3 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
= X4 ) )
=> ( ( X0 @ X4 )
= $true ) )
& ! [X6: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
= X6 )
=> ( ( X2 @ X6 )
= $true ) )
& ! [X14: a > $o,X15: a > $o,X16: a > $o] :
( ( ( ( X0 @ X15 )
= $true )
& ( ( ^ [Y0: a] :
( ( X14 @ Y0 )
& ( X15 @ Y0 ) ) )
= X16 )
& ( ( X0 @ X14 )
= $true ) )
=> ( ( X0 @ X16 )
= $true ) )
& ! [X9: b > $o] :
( ( ( X2 @ X9 )
= $true )
=> ! [X10: a > $o] :
( ( ( ^ [Y0: a] : ( X9 @ ( X1 @ Y0 ) ) )
= X10 )
=> ( ( X0 @ X10 )
= $true ) ) )
& ! [X17: b > $o] :
( ( ( ^ [Y0: b] : $false )
= X17 )
=> ( $true
= ( X2 @ X17 ) ) )
& ! [X11: b > $o,X12: ( b > $o ) > $o] :
( ( ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X12 @ Y1 ) ) ) )
= X11 )
& ! [X13: b > $o] :
( ( ( X12 @ X13 )
= $true )
=> ( $true
= ( X2 @ X13 ) ) ) )
=> ( ( X2 @ X11 )
= $true ) ) )
=> ! [X21: b > $o] :
( ! [X22: b > $o] :
( ( ( ^ [Y0: b] :
~ ( X21 @ Y0 ) )
= X22 )
=> ( ( X2 @ X22 )
= $true ) )
=> ! [X23: a > $o] :
( ( ( ^ [Y0: a] : ( X21 @ ( X1 @ Y0 ) ) )
= X23 )
=> ! [X24: a > $o] :
( ( ( ^ [Y0: a] :
~ ( X23 @ Y0 ) )
= X24 )
=> ( ( X0 @ X24 )
= $true ) ) ) ) ),
inference(rectify,[status(thm)],[f5]) ).
thf(f5,plain,
~ ! [X0: ( a > $o ) > $o,X1: a > b,X2: ( b > $o ) > $o] :
( ( ! [X3: ( a > $o ) > $o,X4: a > $o] :
( ( ( ( ^ [Y0: a] :
( ?? @ ( a > $o )
@ ^ [Y1: a > $o] :
( ( X3 @ Y1 )
& ( Y1 @ Y0 ) ) ) )
= X4 )
& ! [X7: a > $o] :
( ( ( X3 @ X7 )
= $true )
=> ( ( X0 @ X7 )
= $true ) ) )
=> ( ( X0 @ X4 )
= $true ) )
& ! [X8: b > $o] :
( ( ( ^ [Y0: b] : ~ $false )
= X8 )
=> ( ( X2 @ X8 )
= $true ) )
& ! [X10: a > $o] :
( ( ( ^ [Y0: a] : ~ $false )
= X10 )
=> ( ( X0 @ X10 )
= $true ) )
& ! [X12: a > $o] :
( ( ( ^ [Y0: a] : $false )
= X12 )
=> ( ( X0 @ X12 )
= $true ) )
& ! [X14: b > $o] :
( ( ( X2 @ X14 )
= $true )
=> ! [X15: a > $o] :
( ( ( ^ [Y0: a] : ( X14 @ ( X1 @ Y0 ) ) )
= X15 )
=> ( ( X0 @ X15 )
= $true ) ) )
& ! [X17: b > $o,X18: ( b > $o ) > $o] :
( ( ! [X19: b > $o] :
( ( ( X18 @ X19 )
= $true )
=> ( ( X2 @ X19 )
= $true ) )
& ( ( ^ [Y0: b] :
( ?? @ ( b > $o )
@ ^ [Y1: b > $o] :
( ( Y1 @ Y0 )
& ( X18 @ Y1 ) ) ) )
= X17 ) )
=> ( $true
= ( X2 @ X17 ) ) )
& ! [X22: a > $o,X23: a > $o,X24: a > $o] :
( ( ( ( X0 @ X23 )
= $true )
& ( ( ^ [Y0: a] :
( ( X22 @ Y0 )
& ( X23 @ Y0 ) ) )
= X24 )
& ( ( X0 @ X22 )
= $true ) )
=> ( ( X0 @ X24 )
= $true ) )
& ! [X26: b > $o] :
( ( ( ^ [Y0: b] : $false )
= X26 )
=> ( ( X2 @ X26 )
= $true ) )
& ! [X28: b > $o,X29: b > $o,X30: b > $o] :
( ( ( ( ^ [Y0: b] :
( ( X30 @ Y0 )
& ( X28 @ Y0 ) ) )
= X29 )
& ( $true
= ( X2 @ X28 ) )
& ( ( X2 @ X30 )
= $true ) )
=> ( ( X2 @ X29 )
= $true ) ) )
=> ! [X32: b > $o] :
( ! [X33: b > $o] :
( ( ( ^ [Y0: b] :
~ ( X32 @ Y0 ) )
= X33 )
=> ( ( X2 @ X33 )
= $true ) )
=> ! [X35: a > $o] :
( ( ( ^ [Y0: a] : ( X32 @ ( X1 @ Y0 ) ) )
= X35 )
=> ! [X37: a > $o] :
( ( ( ^ [Y0: a] :
~ ( X35 @ Y0 ) )
= X37 )
=> ( ( X0 @ X37 )
= $true ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f4]) ).
thf(f4,plain,
~ ! [X0: ( a > $o ) > $o,X1: a > b,X2: ( b > $o ) > $o] :
( ( ! [X3: ( a > $o ) > $o,X4: a > $o] :
( ( ( ( ^ [X5: a] :
? [X6: a > $o] :
( ( X6 @ X5 )
& ( X3 @ X6 ) ) )
= X4 )
& ! [X7: a > $o] :
( ( X3 @ X7 )
=> ( X0 @ X7 ) ) )
=> ( X0 @ X4 ) )
& ! [X8: b > $o] :
( ( ( ^ [X9: b] : ~ $false )
= X8 )
=> ( X2 @ X8 ) )
& ! [X10: a > $o] :
( ( ( ^ [X11: a] : ~ $false )
= X10 )
=> ( X0 @ X10 ) )
& ! [X12: a > $o] :
( ( ( ^ [X13: a] : $false )
= X12 )
=> ( X0 @ X12 ) )
& ! [X14: b > $o] :
( ( X2 @ X14 )
=> ! [X15: a > $o] :
( ( ( ^ [X16: a] : ( X14 @ ( X1 @ X16 ) ) )
= X15 )
=> ( X0 @ X15 ) ) )
& ! [X17: b > $o,X18: ( b > $o ) > $o] :
( ( ! [X19: b > $o] :
( ( X18 @ X19 )
=> ( X2 @ X19 ) )
& ( ( ^ [X20: b] :
? [X21: b > $o] :
( ( X18 @ X21 )
& ( X21 @ X20 ) ) )
= X17 ) )
=> ( X2 @ X17 ) )
& ! [X22: a > $o,X23: a > $o,X24: a > $o] :
( ( ( X0 @ X23 )
& ( X24
= ( ^ [X25: a] :
( ( X23 @ X25 )
& ( X22 @ X25 ) ) ) )
& ( X0 @ X22 ) )
=> ( X0 @ X24 ) )
& ! [X26: b > $o] :
( ( X26
= ( ^ [X27: b] : $false ) )
=> ( X2 @ X26 ) )
& ! [X28: b > $o,X29: b > $o,X30: b > $o] :
( ( ( ( ^ [X31: b] :
( ( X28 @ X31 )
& ( X30 @ X31 ) ) )
= X29 )
& ( X2 @ X28 )
& ( X2 @ X30 ) )
=> ( X2 @ X29 ) ) )
=> ! [X32: b > $o] :
( ! [X33: b > $o] :
( ( X33
= ( ^ [X34: b] :
~ ( X32 @ X34 ) ) )
=> ( X2 @ X33 ) )
=> ! [X35: a > $o] :
( ( ( ^ [X36: a] : ( X32 @ ( X1 @ X36 ) ) )
= X35 )
=> ! [X37: a > $o] :
( ( ( ^ [X38: a] :
~ ( X35 @ X38 ) )
= X37 )
=> ( X0 @ X37 ) ) ) ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,negated_conjecture,
~ ! [X0: ( a > $o ) > $o,X2: a > b,X1: ( b > $o ) > $o] :
( ( ! [X5: ( a > $o ) > $o,X3: a > $o] :
( ( ( ( ^ [X4: a] :
? [X6: a > $o] :
( ( X6 @ X4 )
& ( X5 @ X6 ) ) )
= X3 )
& ! [X4: a > $o] :
( ( X5 @ X4 )
=> ( X0 @ X4 ) ) )
=> ( X0 @ X3 ) )
& ! [X3: b > $o] :
( ( ( ^ [X4: b] : ~ $false )
= X3 )
=> ( X1 @ X3 ) )
& ! [X3: a > $o] :
( ( ( ^ [X4: a] : ~ $false )
= X3 )
=> ( X0 @ X3 ) )
& ! [X3: a > $o] :
( ( ( ^ [X4: a] : $false )
= X3 )
=> ( X0 @ X3 ) )
& ! [X9: b > $o] :
( ( X1 @ X9 )
=> ! [X7: a > $o] :
( ( ( ^ [X10: a] : ( X9 @ ( X2 @ X10 ) ) )
= X7 )
=> ( X0 @ X7 ) ) )
& ! [X3: b > $o,X5: ( b > $o ) > $o] :
( ( ! [X4: b > $o] :
( ( X5 @ X4 )
=> ( X1 @ X4 ) )
& ( ( ^ [X4: b] :
? [X6: b > $o] :
( ( X5 @ X6 )
& ( X6 @ X4 ) ) )
= X3 ) )
=> ( X1 @ X3 ) )
& ! [X7: a > $o,X8: a > $o,X6: a > $o] :
( ( ( X0 @ X8 )
& ( X6
= ( ^ [X4: a] :
( ( X8 @ X4 )
& ( X7 @ X4 ) ) ) )
& ( X0 @ X7 ) )
=> ( X0 @ X6 ) )
& ! [X3: b > $o] :
( ( X3
= ( ^ [X4: b] : $false ) )
=> ( X1 @ X3 ) )
& ! [X8: b > $o,X6: b > $o,X7: b > $o] :
( ( ( ( ^ [X4: b] :
( ( X8 @ X4 )
& ( X7 @ X4 ) ) )
= X6 )
& ( X1 @ X8 )
& ( X1 @ X7 ) )
=> ( X1 @ X6 ) ) )
=> ! [X9: b > $o] :
( ! [X3: b > $o] :
( ( X3
= ( ^ [X4: b] :
~ ( X9 @ X4 ) ) )
=> ( X1 @ X3 ) )
=> ! [X7: a > $o] :
( ( ( ^ [X10: a] : ( X9 @ ( X2 @ X10 ) ) )
= X7 )
=> ! [X3: a > $o] :
( ( ( ^ [X4: a] :
~ ( X7 @ X4 ) )
= X3 )
=> ( X0 @ X3 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f1,conjecture,
! [X0: ( a > $o ) > $o,X2: a > b,X1: ( b > $o ) > $o] :
( ( ! [X5: ( a > $o ) > $o,X3: a > $o] :
( ( ( ( ^ [X4: a] :
? [X6: a > $o] :
( ( X6 @ X4 )
& ( X5 @ X6 ) ) )
= X3 )
& ! [X4: a > $o] :
( ( X5 @ X4 )
=> ( X0 @ X4 ) ) )
=> ( X0 @ X3 ) )
& ! [X3: b > $o] :
( ( ( ^ [X4: b] : ~ $false )
= X3 )
=> ( X1 @ X3 ) )
& ! [X3: a > $o] :
( ( ( ^ [X4: a] : ~ $false )
= X3 )
=> ( X0 @ X3 ) )
& ! [X3: a > $o] :
( ( ( ^ [X4: a] : $false )
= X3 )
=> ( X0 @ X3 ) )
& ! [X9: b > $o] :
( ( X1 @ X9 )
=> ! [X7: a > $o] :
( ( ( ^ [X10: a] : ( X9 @ ( X2 @ X10 ) ) )
= X7 )
=> ( X0 @ X7 ) ) )
& ! [X3: b > $o,X5: ( b > $o ) > $o] :
( ( ! [X4: b > $o] :
( ( X5 @ X4 )
=> ( X1 @ X4 ) )
& ( ( ^ [X4: b] :
? [X6: b > $o] :
( ( X5 @ X6 )
& ( X6 @ X4 ) ) )
= X3 ) )
=> ( X1 @ X3 ) )
& ! [X7: a > $o,X8: a > $o,X6: a > $o] :
( ( ( X0 @ X8 )
& ( X6
= ( ^ [X4: a] :
( ( X8 @ X4 )
& ( X7 @ X4 ) ) ) )
& ( X0 @ X7 ) )
=> ( X0 @ X6 ) )
& ! [X3: b > $o] :
( ( X3
= ( ^ [X4: b] : $false ) )
=> ( X1 @ X3 ) )
& ! [X8: b > $o,X6: b > $o,X7: b > $o] :
( ( ( ( ^ [X4: b] :
( ( X8 @ X4 )
& ( X7 @ X4 ) ) )
= X6 )
& ( X1 @ X8 )
& ( X1 @ X7 ) )
=> ( X1 @ X6 ) ) )
=> ! [X9: b > $o] :
( ! [X3: b > $o] :
( ( X3
= ( ^ [X4: b] :
~ ( X9 @ X4 ) ) )
=> ( X1 @ X3 ) )
=> ! [X7: a > $o] :
( ( ( ^ [X10: a] : ( X9 @ ( X2 @ X10 ) ) )
= X7 )
=> ! [X3: a > $o] :
( ( ( ^ [X4: a] :
~ ( X7 @ X4 ) )
= X3 )
=> ( X0 @ X3 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.mBP11uJTB9/DTF2THF_29967.p',cCLOSED_THM1_pme) ).
thf(f61,plain,
( ( sK2
@ ^ [Y0: b] :
~ ( sK3 @ Y0 ) )
!= $true ),
inference(beta_eta_normalization,[status(thm)],[f60]) ).
thf(f60,plain,
( ( sK2
@ ^ [Y0: b] :
~ ( ^ [Y1: b] :
( sK3
@ ( ^ [Y2: b] : Y2
@ Y1 ) )
@ Y0 ) )
!= $true ),
inference(trivial_inequality_removal,[status(thm)],[f59]) ).
thf(f59,plain,
( ( $true != $true )
| ( ( sK2
@ ^ [Y0: b] :
~ ( ^ [Y1: b] :
( sK3
@ ( ^ [Y2: b] : Y2
@ Y1 ) )
@ Y0 ) )
!= $true ) ),
inference(superposition,[status(thm)],[f48,f45]) ).
thf(f45,plain,
! [X23: b > $o] :
( ( ( sK0
@ ^ [Y0: a] : ( X23 @ ( sK1 @ Y0 ) ) )
= $true )
| ( ( sK2 @ X23 )
!= $true ) ),
inference(equality_resolution,[status(thm)],[f17]) ).
thf(f17,plain,
! [X24: a > $o,X23: b > $o] :
( ( ( sK2 @ X23 )
!= $true )
| ( ( ^ [Y0: a] : ( X23 @ ( sK1 @ Y0 ) ) )
!= X24 )
| ( ( sK0 @ X24 )
= $true ) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
thf(f48,plain,
( ( sK0
@ ^ [Y0: a] :
~ ( sK3 @ ( sK1 @ Y0 ) ) )
!= $true ),
inference(beta_eta_normalization,[status(thm)],[f33]) ).
thf(f33,plain,
( ( sK0
@ ^ [Y0: a] :
~ ( ^ [Y1: a] : ( sK3 @ ( sK1 @ Y1 ) )
@ Y0 ) )
!= $true ),
inference(definition_unfolding,[status(thm)],[f30,f32]) ).
thf(f32,plain,
( ( ^ [Y0: a] :
~ ( ^ [Y1: a] : ( sK3 @ ( sK1 @ Y1 ) )
@ Y0 ) )
= sK5 ),
inference(definition_unfolding,[status(thm)],[f29,f31]) ).
thf(f31,plain,
( ( ^ [Y0: a] : ( sK3 @ ( sK1 @ Y0 ) ) )
= sK4 ),
inference(cnf_transformation,[status(thm)],[f16]) ).
thf(f29,plain,
( sK5
= ( ^ [Y0: a] :
~ ( sK4 @ Y0 ) ) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
thf(f30,plain,
( ( sK0 @ sK5 )
!= $true ),
inference(cnf_transformation,[status(thm)],[f16]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV260^5 : TPTP v9.2.1. Released v4.0.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 : n028.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 12:43:27 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.19/0.48 ---- Original DTF file ---
% 0.19/0.48 thf(spec,logic,$$dhol).
% 0.19/0.48 %------------------------------------------------------------------------------
% 0.19/0.48 % File : SEV260^5 : TPTP v9.2.1. Released v4.0.0.
% 0.19/0.48 % Domain : Set Theory (Sets of sets)
% 0.19/0.48 % Problem : TPS problem CLOSED-THM1
% 0.19/0.48 % Version : Especial.
% 0.19/0.48 % English : The inverse image of a closed set under a continuous function is
% 0.19/0.48 % closed.
% 0.19/0.48
% 0.19/0.48 % Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.19/0.48 % Source : [Bro09]
% 0.19/0.48 % Names : tps_0474 [Bro09]
% 0.19/0.48 % : CLOSED-THM1 [TPS]
% 0.19/0.48
% 0.19/0.48 % Status : Theorem
% 0.19/0.48 % Rating : 0.33 v9.1.0, 0.25 v9.0.0, 0.30 v8.2.0, 0.54 v8.1.0, 0.45 v7.5.0, 0.29 v7.4.0, 0.33 v7.2.0, 0.25 v7.1.0, 0.38 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.40 v6.2.0, 0.43 v5.5.0, 0.50 v5.4.0, 0.60 v4.1.0, 0.33 v4.0.1, 0.67 v4.0.0
% 0.19/0.48 % Syntax : Number of formulae : 3 ( 0 unt; 2 typ; 0 def)
% 0.19/0.48 % Number of atoms : 16 ( 12 equ; 0 cnn)
% 0.19/0.48 % Maximal formula atoms : 12 ( 16 avg)
% 0.19/0.48 % Number of connectives : 73 ( 4 ~; 0 |; 18 &; 34 @)
% 0.19/0.48 % ( 0 <=>; 17 =>; 0 <=; 0 <~>)
% 0.19/0.48 % Maximal formula depth : 20 ( 20 avg)
% 0.19/0.48 % Number of types : 3 ( 2 usr)
% 0.19/0.48 % Number of type conns : 31 ( 31 >; 0 *; 0 +; 0 <<)
% 0.19/0.48 % Number of symbols : 2 ( 0 usr; 1 con; 0-2 aty)
% 0.19/0.48 % Number of variables : 39 ( 12 ^; 25 !; 2 ?; 39 :)
% 0.19/0.48 % SPC : TH0_THM_EQU_NAR
% 0.19/0.48
% 0.19/0.48 % Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS
% 0.19/0.48 % project in the Department of Mathematical Sciences at Carnegie
% 0.19/0.48 % Mellon University. Distributed under the Creative Commons copyleft
% 0.19/0.48 % license: http://creativecommons.org/licenses/by-sa/3.0/
% 0.19/0.48 % : Polymorphic definitions expanded.
% 0.19/0.48 %------------------------------------------------------------------------------
% 0.19/0.48 thf(a_type,type,
% 0.19/0.48 a: $tType ).
% 0.19/0.48
% 0.19/0.48 thf(b_type,type,
% 0.19/0.48 b: $tType ).
% 0.19/0.48
% 0.19/0.48 thf(cCLOSED_THM1_pme,conjecture,
% 0.19/0.48 ! [T: ( a > $o ) > $o,S: ( b > $o ) > $o,Xf: a > b] :
% 0.19/0.48 ( ( ! [R: a > $o] :
% 0.19/0.48 ( ( R
% 0.19/0.48 = ( ^ [Xx: a] : $false ) )
% 0.19/0.48 => ( T @ R ) )
% 0.19/0.48 & ! [R: a > $o] :
% 0.19/0.48 ( ( R
% 0.19/0.48 = ( ^ [Xx: a] : ~ $false ) )
% 0.19/0.48 => ( T @ R ) )
% 0.19/0.48 & ! [K: ( a > $o ) > $o,R: a > $o] :
% 0.19/0.48 ( ( ! [Xx: a > $o] :
% 0.19/0.48 ( ( K @ Xx )
% 0.19/0.48 => ( T @ Xx ) )
% 0.19/0.48 & ( R
% 0.19/0.48 = ( ^ [Xx: a] :
% 0.19/0.48 ? [S0: a > $o] :
% 0.19/0.48 ( ( K @ S0 )
% 0.19/0.48 & ( S0 @ Xx ) ) ) ) )
% 0.19/0.48 => ( T @ R ) )
% 0.19/0.48 & ! [Y: a > $o,Z: a > $o,S0: a > $o] :
% 0.19/0.48 ( ( ( T @ Y )
% 0.19/0.48 & ( T @ Z )
% 0.19/0.48 & ( S0
% 0.19/0.48 = ( ^ [Xx: a] :
% 0.19/0.48 ( ( Y @ Xx )
% 0.19/0.48 & ( Z @ Xx ) ) ) ) )
% 0.19/0.48 => ( T @ S0 ) )
% 0.19/0.48 & ! [R: b > $o] :
% 0.19/0.48 ( ( R
% 0.19/0.48 = ( ^ [Xx: b] : $false ) )
% 0.19/0.48 => ( S @ R ) )
% 0.19/0.48 & ! [R: b > $o] :
% 0.19/0.48 ( ( R
% 0.19/0.48 = ( ^ [Xx: b] : ~ $false ) )
% 0.19/0.48 => ( S @ R ) )
% 0.19/0.48 & ! [K: ( b > $o ) > $o,R: b > $o] :
% 0.19/0.48 ( ( ! [Xx: b > $o] :
% 0.19/0.48 ( ( K @ Xx )
% 0.19/0.48 => ( S @ Xx ) )
% 0.19/0.48 & ( R
% 0.19/0.48 = ( ^ [Xx: b] :
% 0.19/0.48 ? [S0: b > $o] :
% 0.19/0.48 ( ( K @ S0 )
% 0.19/0.48 & ( S0 @ Xx ) ) ) ) )
% 0.19/0.48 => ( S @ R ) )
% 0.19/0.48 & ! [Y: b > $o,Z: b > $o,S0: b > $o] :
% 0.19/0.48 ( ( ( S @ Y )
% 0.19/0.48 & ( S @ Z )
% 0.19/0.48 & ( S0
% 0.19/0.48 = ( ^ [Xx: b] :
% 0.19/0.48 ( ( Y @ Xx )
% 0.19/0.48 & ( Z @ Xx ) ) ) ) )
% 0.19/0.48 => ( S @ S0 ) )
% 0.19/0.48 & ! [X: b > $o] :
% 0.19/0.48 ( ( S @ X )
% 0.19/0.48 => ! [Y: a > $o] :
% 0.19/0.48 ( ( Y
% 0.19/0.48 = ( ^ [Xb: a] : ( X @ ( Xf @ Xb ) ) ) )
% 0.19/0.48 => ( T @ Y ) ) ) )
% 0.19/0.48 => ! [X: b > $o] :
% 0.19/0.48 ( ! [R: b > $o] :
% 0.19/0.48 ( ( R
% 0.19/0.48 = ( ^ [Xx: b] :
% 0.19/0.48 ~ ( X @ Xx ) ) )
% 0.19/0.48 => ( S @ R ) )
% 0.19/0.48 => ! [Y: a > $o] :
% 0.19/0.48 ( ( Y
% 0.19/0.48 = ( ^ [Xb: a] : ( X @ ( Xf @ Xb ) ) ) )
% 0.19/0.48 => ! [R: a > $o] :
% 0.19/0.48 ( ( R
% 0.19/0.48 = ( ^ [Xx: a] :
% 0.19/0.48 ~ ( Y @ Xx ) ) )
% 0.19/0.48 => ( T @ R ) ) ) ) ) ).
% 0.19/0.48
% 0.19/0.48 %------------------------------------------------------------------------------
% 0.19/0.48 ------------------------
% 1.57/1.34 ---- Embedded in THF ---
% 1.57/1.34 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.57/1.34 %%% Generated on Tue Feb 24 12:43:28 EST 2026
% 1.57/1.34 %%% using '$$dhol' embedding, version 1.3.0.
% 1.57/1.34 %%% Logic specification used:
% 1.57/1.34 %%% thf(spec, logic, $$dhol).
% 1.57/1.34
% 1.57/1.34 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.mBP11uJTB9/DTF2DTF29967.p
% See solution above
% 1.57/1.34 ------------------------
% 1.57/1.34 ---- Cleaned THF ---
% 1.57/1.35 thf(a_type,type,
% 1.57/1.35 a: $tType ).
% 1.57/1.35
% 1.57/1.35 thf(b_type,type,
% 1.57/1.35 b: $tType ).
% 1.57/1.35
% 1.57/1.35 thf(cCLOSED_THM1_pme,conjecture,
% 1.57/1.35 ! [T: ( a > $o ) > $o,S: ( b > $o ) > $o,Xf: a > b] :
% 1.57/1.35 ( ( ! [R: a > $o] :
% 1.57/1.35 ( ( R
% 1.57/1.35 = ( ^ [Xx: a] : $false ) )
% 1.57/1.35 => ( T @ R ) )
% 1.57/1.35 & ! [R: a > $o] :
% 1.57/1.35 ( ( R
% 1.57/1.35 = ( ^ [Xx: a] : ~ $false ) )
% 1.57/1.35 => ( T @ R ) )
% 1.57/1.35 & ! [K: ( a > $o ) > $o,R: a > $o] :
% 1.57/1.35 ( ( ! [Xx: a > $o] :
% 1.57/1.35 ( ( K @ Xx )
% 1.57/1.35 => ( T @ Xx ) )
% 1.57/1.35 & ( R
% 1.57/1.35 = ( ^ [Xx: a] :
% 1.57/1.35 ? [S0: a > $o] :
% 1.57/1.35 ( ( K @ S0 )
% 1.57/1.35 & ( S0 @ Xx ) ) ) ) )
% 1.57/1.35 => ( T @ R ) )
% 1.57/1.35 & ! [Y: a > $o,Z: a > $o,S0: a > $o] :
% 1.57/1.35 ( ( ( T @ Y )
% 1.57/1.35 & ( T @ Z )
% 1.57/1.35 & ( S0
% 1.57/1.35 = ( ^ [Xx: a] :
% 1.57/1.35 ( ( Y @ Xx )
% 1.57/1.35 & ( Z @ Xx ) ) ) ) )
% 1.57/1.35 => ( T @ S0 ) )
% 1.57/1.35 & ! [R: b > $o] :
% 1.57/1.35 ( ( R
% 1.57/1.35 = ( ^ [Xx: b] : $false ) )
% 1.57/1.35 => ( S @ R ) )
% 1.57/1.35 & ! [R: b > $o] :
% 1.57/1.35 ( ( R
% 1.57/1.35 = ( ^ [Xx: b] : ~ $false ) )
% 1.57/1.35 => ( S @ R ) )
% 1.57/1.35 & ! [K: ( b > $o ) > $o,R: b > $o] :
% 1.57/1.35 ( ( ! [Xx: b > $o] :
% 1.57/1.35 ( ( K @ Xx )
% 1.57/1.35 => ( S @ Xx ) )
% 1.57/1.35 & ( R
% 1.57/1.35 = ( ^ [Xx: b] :
% 1.57/1.35 ? [S0: b > $o] :
% 1.57/1.35 ( ( K @ S0 )
% 1.57/1.35 & ( S0 @ Xx ) ) ) ) )
% 1.57/1.35 => ( S @ R ) )
% 1.57/1.35 & ! [Y: b > $o,Z: b > $o,S0: b > $o] :
% 1.57/1.35 ( ( ( S @ Y )
% 1.57/1.35 & ( S @ Z )
% 1.57/1.35 & ( S0
% 1.57/1.35 = ( ^ [Xx: b] :
% 1.57/1.35 ( ( Y @ Xx )
% 1.57/1.35 & ( Z @ Xx ) ) ) ) )
% 1.57/1.35 => ( S @ S0 ) )
% 1.57/1.35 & ! [X: b > $o] :
% 1.57/1.35 ( ( S @ X )
% 1.57/1.35 => ! [Y: a > $o] :
% 1.57/1.35 ( ( Y
% 1.57/1.35 = ( ^ [Xb: a] : ( X @ ( Xf @ Xb ) ) ) )
% 1.57/1.35 => ( T @ Y ) ) ) )
% 1.57/1.35 => ! [X: b > $o] :
% 1.57/1.35 ( ! [R: b > $o] :
% 1.57/1.35 ( ( R
% 1.57/1.35 = ( ^ [Xx: b] :
% 1.57/1.35 ~ ( X @ Xx ) ) )
% 1.57/1.35 => ( S @ R ) )
% 1.57/1.35 => ! [Y: a > $o] :
% 1.57/1.35 ( ( Y
% 1.57/1.35 = ( ^ [Xb: a] : ( X @ ( Xf @ Xb ) ) ) )
% 1.57/1.35 => ! [R: a > $o] :
% 1.57/1.35 ( ( R
% 1.57/1.35 = ( ^ [Xx: a] :
% 1.57/1.35 ~ ( Y @ Xx ) ) )
% 1.57/1.35 => ( T @ R ) ) ) ) ) ).
% 1.57/1.35 ------------------------
% 1.57/1.36 % (30064)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_29967 for (3000ds/183Mi)
% 1.57/1.36 % (30066)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_29967 for (3000ds/27Mi)
% 1.57/1.36 % (30064)First to succeed.
% 1.57/1.36 % (30069)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_29967 for (3000ds/275Mi)
% 1.57/1.36 % (30068)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_29967 for (3000ds/2Mi)
% 1.57/1.36 % (30067)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_29967 for (3000ds/2Mi)
% 1.57/1.36 % (30070)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_29967 for (3000ds/18Mi)
% 1.57/1.37 % (30067)Instruction limit reached!
% 1.57/1.37 % (30067)------------------------------
% 1.57/1.37 % (30067)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.57/1.37 % (30067)Termination reason: Unknown
% 1.57/1.37 % (30068)Instruction limit reached!
% 1.57/1.37 % (30068)------------------------------
% 1.57/1.37 % (30068)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.57/1.37 % (30068)Termination reason: Unknown
% 1.57/1.37 % (30068)Termination phase: Property scanning
% 1.57/1.37
% 1.57/1.37 % (30068)Memory used [KB]: 1023
% 1.57/1.37 % (30068)Time elapsed: 0.003 s
% 1.57/1.37 % (30068)Instructions burned: 3 (million)
% 1.57/1.37 % (30068)------------------------------
% 1.57/1.37 % (30068)------------------------------
% 1.57/1.37 % (30067)Termination phase: Preprocessing 2
% 1.57/1.37
% 1.57/1.37 % (30067)Memory used [KB]: 1023
% 1.57/1.37 % (30067)Time elapsed: 0.003 s
% 1.57/1.37 % (30067)Instructions burned: 2 (million)
% 1.57/1.37 % (30067)------------------------------
% 1.57/1.37 % (30067)------------------------------
% 1.57/1.37 % (30066)Also succeeded, but the first one will report.
% 1.57/1.37 % (30064)Refutation found. Thanks to Tanya!
% 1.57/1.37 % SZS status Theorem for DTF2THF_29967
% 1.57/1.37 % SZS output start Proof for DTF2THF_29967
% 1.57/1.37 thf(type_def_5, type, a: $tType).
% 1.57/1.37 thf(type_def_7, type, b: $tType).
% 1.57/1.37 thf(func_def_0, type, a: $tType).
% 1.57/1.37 thf(func_def_1, type, b: $tType).
% 1.57/1.37 thf(func_def_11, type, sK0: (a > $o) > $o).
% 1.57/1.37 thf(func_def_12, type, sK1: a > b).
% 1.57/1.37 thf(func_def_13, type, sK2: (b > $o) > $o).
% 1.57/1.37 thf(func_def_14, type, sK3: b > $o).
% 1.57/1.37 thf(func_def_15, type, sK4: a > $o).
% 1.57/1.37 thf(func_def_16, type, sK5: a > $o).
% 1.57/1.37 thf(func_def_17, type, sK6: ((b > $o) > $o) > b > $o).
% 1.57/1.37 thf(func_def_18, type, sK7: ((a > $o) > $o) > a > $o).
% 1.57/1.37 thf(func_def_20, type, ph9: !>[X0: $tType]:(X0)).
% 1.57/1.37 thf(func_def_21, type, sK10: a).
% 1.57/1.37 thf(func_def_22, type, sK11: a).
% 1.57/1.37 thf(f62,plain,(
% 1.57/1.37 $false),
% 1.57/1.37 inference(subsumption_resolution,[status(thm)],[f61,f34])).
% 1.57/1.37 thf(f34,plain,(
% 1.57/1.37 ((sK2 @ (^[Y0 : b]: (~ (sK3 @ Y0)))) = $true)),
% 1.57/1.37 inference(equality_resolution,[status(thm)],[f28])).
% 1.57/1.37 thf(f28,plain,(
% 1.57/1.37 ( ! [X6 : b > $o] : (((sK2 @ X6) = $true) | ((^[Y0 : b]: (~ (sK3 @ Y0))) != X6)) )),
% 1.57/1.37 inference(cnf_transformation,[status(thm)],[f16])).
% 1.57/1.37 thf(f16,plain,(
% 1.57/1.37 ((((^[Y0 : a]: (sK3 @ (sK1 @ Y0))) = sK4) & (((sK0 @ sK5) != $true) & (sK5 = (^[Y0 : a]: (~ (sK4 @ Y0)))))) & ! [X6 : b > $o] : (((sK2 @ X6) = $true) | ((^[Y0 : b]: (~ (sK3 @ Y0))) != X6))) & ! [X7 : a > $o] : (((^[Y0 : a]: ($false)) != X7) | ((sK0 @ X7) = $true)) & ! [X8 : b > $o] : (((^[Y0 : b]: ($false)) != X8) | ((sK2 @ X8) = $true)) & ! [X9 : a > $o] : (((^[Y0 : a]: (~ $false)) != X9) | ((sK0 @ X9) = $true)) & ! [X10 : b > $o,X11 : (b > $o) > $o] : ((((X11 @ (sK6 @ X11)) = $true) & ((sK2 @ (sK6 @ X11)) != $true)) | ((sK2 @ X10) = $true) | ((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X11 @ Y1))))) != X10)) & ! [X13 : a > $o,X14 : a > $o,X15 : a > $o] : (((^[Y0 : a]: ((X13 @ Y0) & (X14 @ Y0))) != X15) | ((sK0 @ X15) = $true) | ((sK0 @ X13) != $true) | ((sK0 @ X14) != $true)) & ! [X16 : (a > $o) > $o,X17 : a > $o] : (((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X16 @ Y1) & (Y1 @ Y0))))) != X17) | ((sK0 @ X17) = $true) | (($true = (X16 @ (sK7 @ X16))) & ((sK0 @ (sK7 @ X16)) != $true))) & ! [X19 : b > $o,X20 : b > $o,X21 : b > $o] : (((sK2 @ X20) = $true) | ((sK2 @ X19) != $true) | ((^[Y0 : b]: ((X21 @ Y0) & (X19 @ Y0))) != X20) | ((sK2 @ X21) != $true)) & ! [X22 : b > $o] : (((^[Y0 : b]: (~ $false)) != X22) | ((sK2 @ X22) = $true)) & ! [X23 : b > $o] : (((sK2 @ X23) != $true) | ! [X24 : a > $o] : (((^[Y0 : a]: (X23 @ (sK1 @ Y0))) != X24) | ((sK0 @ X24) = $true)))),
% 1.57/1.37 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7])],[f9,f15,f14,f13,f12,f11,f10])).
% 1.57/1.37 thf(f10,plain,(
% 1.57/1.37 ? [X0 : (a > $o) > $o,X1 : a > b,X2 : (b > $o) > $o] : (? [X3 : b > $o] : (? [X4 : a > $o] : (((^[Y0 : a]: (X3 @ (X1 @ Y0))) = X4) & ? [X5 : a > $o] : (((X0 @ X5) != $true) & ((^[Y0 : a]: (~ (X4 @ Y0))) = X5))) & ! [X6 : b > $o] : (((X2 @ X6) = $true) | ((^[Y0 : b]: (~ (X3 @ Y0))) != X6))) & ! [X7 : a > $o] : (((^[Y0 : a]: ($false)) != X7) | ((X0 @ X7) = $true)) & ! [X8 : b > $o] : (((^[Y0 : b]: ($false)) != X8) | ((X2 @ X8) = $true)) & ! [X9 : a > $o] : (((^[Y0 : a]: (~ $false)) != X9) | ($true = (X0 @ X9))) & ! [X10 : b > $o,X11 : (b > $o) > $o] : (? [X12 : b > $o] : (((X11 @ X12) = $true) & ((X2 @ X12) != $true)) | ((X2 @ X10) = $true) | ((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X11 @ Y1))))) != X10)) & ! [X13 : a > $o,X14 : a > $o,X15 : a > $o] : (((^[Y0 : a]: ((X13 @ Y0) & (X14 @ Y0))) != X15) | ((X0 @ X15) = $true) | ((X0 @ X13) != $true) | ((X0 @ X14) != $true)) & ! [X16 : (a > $o) > $o,X17 : a > $o] : (((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X16 @ Y1) & (Y1 @ Y0))))) != X17) | ((X0 @ X17) = $true) | ? [X18 : a > $o] : (((X16 @ X18) = $true) & ((X0 @ X18) != $true))) & ! [X19 : b > $o,X20 : b > $o,X21 : b > $o] : (((X2 @ X20) = $true) | ((X2 @ X19) != $true) | ((^[Y0 : b]: ((X21 @ Y0) & (X19 @ Y0))) != X20) | ((X2 @ X21) != $true)) & ! [X22 : b > $o] : (((^[Y0 : b]: (~ $false)) != X22) | ((X2 @ X22) = $true)) & ! [X23 : b > $o] : (((X2 @ X23) != $true) | ! [X24 : a > $o] : (((^[Y0 : a]: (X23 @ (X1 @ Y0))) != X24) | ((X0 @ X24) = $true)))) => (? [X3 : b > $o] : (? [X4 : a > $o] : (((^[Y0 : a]: (X3 @ (sK1 @ Y0))) = X4) & ? [X5 : a > $o] : (((sK0 @ X5) != $true) & ((^[Y0 : a]: (~ (X4 @ Y0))) = X5))) & ! [X6 : b > $o] : (((sK2 @ X6) = $true) | ((^[Y0 : b]: (~ (X3 @ Y0))) != X6))) & ! [X7 : a > $o] : (((^[Y0 : a]: ($false)) != X7) | ((sK0 @ X7) = $true)) & ! [X8 : b > $o] : (((^[Y0 : b]: ($false)) != X8) | ((sK2 @ X8) = $true)) & ! [X9 : a > $o] : (((^[Y0 : a]: (~ $false)) != X9) | ((sK0 @ X9) = $true)) & ! [X11 : (b > $o) > $o,X10 : b > $o] : (? [X12 : b > $o] : (((X11 @ X12) = $true) & ((sK2 @ X12) != $true)) | ((sK2 @ X10) = $true) | ((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X11 @ Y1))))) != X10)) & ! [X15 : a > $o,X14 : a > $o,X13 : a > $o] : (((^[Y0 : a]: ((X13 @ Y0) & (X14 @ Y0))) != X15) | ((sK0 @ X15) = $true) | ((sK0 @ X13) != $true) | ((sK0 @ X14) != $true)) & ! [X17 : a > $o,X16 : (a > $o) > $o] : (((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X16 @ Y1) & (Y1 @ Y0))))) != X17) | ((sK0 @ X17) = $true) | ? [X18 : a > $o] : (((X16 @ X18) = $true) & ((sK0 @ X18) != $true))) & ! [X21 : b > $o,X20 : b > $o,X19 : b > $o] : (((sK2 @ X20) = $true) | ((sK2 @ X19) != $true) | ((^[Y0 : b]: ((X21 @ Y0) & (X19 @ Y0))) != X20) | ((sK2 @ X21) != $true)) & ! [X22 : b > $o] : (((^[Y0 : b]: (~ $false)) != X22) | ((sK2 @ X22) = $true)) & ! [X23 : b > $o] : (((sK2 @ X23) != $true) | ! [X24 : a > $o] : (((^[Y0 : a]: (X23 @ (sK1 @ Y0))) != X24) | ((sK0 @ X24) = $true))))),
% 1.57/1.37 introduced(definition,[],[choice_axiom])).
% 1.57/1.37 thf(f11,plain,(
% 1.57/1.37 ? [X3 : b > $o] : (? [X4 : a > $o] : (((^[Y0 : a]: (X3 @ (sK1 @ Y0))) = X4) & ? [X5 : a > $o] : (((sK0 @ X5) != $true) & ((^[Y0 : a]: (~ (X4 @ Y0))) = X5))) & ! [X6 : b > $o] : (((sK2 @ X6) = $true) | ((^[Y0 : b]: (~ (X3 @ Y0))) != X6))) => (? [X4 : a > $o] : (((^[Y0 : a]: (sK3 @ (sK1 @ Y0))) = X4) & ? [X5 : a > $o] : (((sK0 @ X5) != $true) & ((^[Y0 : a]: (~ (X4 @ Y0))) = X5))) & ! [X6 : b > $o] : (((sK2 @ X6) = $true) | ((^[Y0 : b]: (~ (sK3 @ Y0))) != X6)))),
% 1.57/1.37 introduced(definition,[],[choice_axiom])).
% 1.57/1.37 thf(f12,plain,(
% 1.57/1.37 ? [X4 : a > $o] : (((^[Y0 : a]: (sK3 @ (sK1 @ Y0))) = X4) & ? [X5 : a > $o] : (((sK0 @ X5) != $true) & ((^[Y0 : a]: (~ (X4 @ Y0))) = X5))) => (((^[Y0 : a]: (sK3 @ (sK1 @ Y0))) = sK4) & ? [X5 : a > $o] : (((sK0 @ X5) != $true) & ((^[Y0 : a]: (~ (sK4 @ Y0))) = X5)))),
% 1.57/1.37 introduced(definition,[],[choice_axiom])).
% 1.57/1.37 thf(f13,plain,(
% 1.57/1.37 ? [X5 : a > $o] : (((sK0 @ X5) != $true) & ((^[Y0 : a]: (~ (sK4 @ Y0))) = X5)) => (((sK0 @ sK5) != $true) & (sK5 = (^[Y0 : a]: (~ (sK4 @ Y0)))))),
% 1.57/1.37 introduced(definition,[],[choice_axiom])).
% 1.57/1.37 thf(f14,plain,(
% 1.57/1.37 ! [X11 : (b > $o) > $o] : (? [X12 : b > $o] : (((X11 @ X12) = $true) & ((sK2 @ X12) != $true)) => (((X11 @ (sK6 @ X11)) = $true) & ((sK2 @ (sK6 @ X11)) != $true)))),
% 1.57/1.37 introduced(definition,[],[choice_axiom])).
% 1.57/1.37 thf(f15,plain,(
% 1.57/1.37 ! [X16 : (a > $o) > $o] : (? [X18 : a > $o] : (((X16 @ X18) = $true) & ((sK0 @ X18) != $true)) => (($true = (X16 @ (sK7 @ X16))) & ((sK0 @ (sK7 @ X16)) != $true)))),
% 1.57/1.37 introduced(definition,[],[choice_axiom])).
% 1.57/1.37 thf(f9,plain,(
% 1.57/1.37 ? [X0 : (a > $o) > $o,X1 : a > b,X2 : (b > $o) > $o] : (? [X3 : b > $o] : (? [X4 : a > $o] : (((^[Y0 : a]: (X3 @ (X1 @ Y0))) = X4) & ? [X5 : a > $o] : (((X0 @ X5) != $true) & ((^[Y0 : a]: (~ (X4 @ Y0))) = X5))) & ! [X6 : b > $o] : (((X2 @ X6) = $true) | ((^[Y0 : b]: (~ (X3 @ Y0))) != X6))) & ! [X7 : a > $o] : (((^[Y0 : a]: ($false)) != X7) | ((X0 @ X7) = $true)) & ! [X8 : b > $o] : (((^[Y0 : b]: ($false)) != X8) | ((X2 @ X8) = $true)) & ! [X9 : a > $o] : (((^[Y0 : a]: (~ $false)) != X9) | ($true = (X0 @ X9))) & ! [X10 : b > $o,X11 : (b > $o) > $o] : (? [X12 : b > $o] : (((X11 @ X12) = $true) & ((X2 @ X12) != $true)) | ((X2 @ X10) = $true) | ((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X11 @ Y1))))) != X10)) & ! [X13 : a > $o,X14 : a > $o,X15 : a > $o] : (((^[Y0 : a]: ((X13 @ Y0) & (X14 @ Y0))) != X15) | ((X0 @ X15) = $true) | ((X0 @ X13) != $true) | ((X0 @ X14) != $true)) & ! [X16 : (a > $o) > $o,X17 : a > $o] : (((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X16 @ Y1) & (Y1 @ Y0))))) != X17) | ((X0 @ X17) = $true) | ? [X18 : a > $o] : (((X16 @ X18) = $true) & ((X0 @ X18) != $true))) & ! [X19 : b > $o,X20 : b > $o,X21 : b > $o] : (((X2 @ X20) = $true) | ((X2 @ X19) != $true) | ((^[Y0 : b]: ((X21 @ Y0) & (X19 @ Y0))) != X20) | ((X2 @ X21) != $true)) & ! [X22 : b > $o] : (((^[Y0 : b]: (~ $false)) != X22) | ((X2 @ X22) = $true)) & ! [X23 : b > $o] : (((X2 @ X23) != $true) | ! [X24 : a > $o] : (((^[Y0 : a]: (X23 @ (X1 @ Y0))) != X24) | ((X0 @ X24) = $true))))),
% 1.57/1.37 inference(rectify,[status(thm)],[f8])).
% 1.57/1.37 thf(f8,plain,(
% 1.57/1.37 ? [X0 : (a > $o) > $o,X1 : a > b,X2 : (b > $o) > $o] : (? [X21 : b > $o] : (? [X23 : a > $o] : (((^[Y0 : a]: (X21 @ (X1 @ Y0))) = X23) & ? [X24 : a > $o] : (((X0 @ X24) != $true) & ((^[Y0 : a]: (~ (X23 @ Y0))) = X24))) & ! [X22 : b > $o] : (((X2 @ X22) = $true) | ((^[Y0 : b]: (~ (X21 @ Y0))) != X22))) & ! [X8 : a > $o] : (((^[Y0 : a]: ($false)) != X8) | ((X0 @ X8) = $true)) & ! [X17 : b > $o] : (((^[Y0 : b]: ($false)) != X17) | ($true = (X2 @ X17))) & ! [X7 : a > $o] : (((^[Y0 : a]: (~ $false)) != X7) | ((X0 @ X7) = $true)) & ! [X11 : b > $o,X12 : (b > $o) > $o] : (? [X13 : b > $o] : (((X12 @ X13) = $true) & ($true != (X2 @ X13))) | ((X2 @ X11) = $true) | ((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X12 @ Y1))))) != X11)) & ! [X14 : a > $o,X15 : a > $o,X16 : a > $o] : (((^[Y0 : a]: ((X14 @ Y0) & (X15 @ Y0))) != X16) | ((X0 @ X16) = $true) | ((X0 @ X14) != $true) | ((X0 @ X15) != $true)) & ! [X3 : (a > $o) > $o,X4 : a > $o] : (((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X3 @ Y1) & (Y1 @ Y0))))) != X4) | ((X0 @ X4) = $true) | ? [X5 : a > $o] : (((X3 @ X5) = $true) & ((X0 @ X5) != $true))) & ! [X18 : b > $o,X19 : b > $o,X20 : b > $o] : (((X2 @ X19) = $true) | ((X2 @ X18) != $true) | ((^[Y0 : b]: ((X20 @ Y0) & (X18 @ Y0))) != X19) | ((X2 @ X20) != $true)) & ! [X6 : b > $o] : (((^[Y0 : b]: (~ $false)) != X6) | ((X2 @ X6) = $true)) & ! [X9 : b > $o] : (((X2 @ X9) != $true) | ! [X10 : a > $o] : (((^[Y0 : a]: (X9 @ (X1 @ Y0))) != X10) | ((X0 @ X10) = $true))))),
% 1.57/1.37 inference(flattening,[status(thm)],[f7])).
% 1.57/1.37 thf(f7,plain,(
% 1.57/1.37 ? [X0 : (a > $o) > $o,X1 : a > b,X2 : (b > $o) > $o] : (? [X21 : b > $o] : (? [X23 : a > $o] : (((^[Y0 : a]: (X21 @ (X1 @ Y0))) = X23) & ? [X24 : a > $o] : (((X0 @ X24) != $true) & ((^[Y0 : a]: (~ (X23 @ Y0))) = X24))) & ! [X22 : b > $o] : (((X2 @ X22) = $true) | ((^[Y0 : b]: (~ (X21 @ Y0))) != X22))) & (! [X7 : a > $o] : (((^[Y0 : a]: (~ $false)) != X7) | ((X0 @ X7) = $true)) & ! [X18 : b > $o,X19 : b > $o,X20 : b > $o] : (((X2 @ X19) = $true) | (((^[Y0 : b]: ((X20 @ Y0) & (X18 @ Y0))) != X19) | ((X2 @ X18) != $true) | ((X2 @ X20) != $true))) & ! [X8 : a > $o] : (((^[Y0 : a]: ($false)) != X8) | ((X0 @ X8) = $true)) & ! [X3 : (a > $o) > $o,X4 : a > $o] : (((X0 @ X4) = $true) | (? [X5 : a > $o] : (((X3 @ X5) = $true) & ((X0 @ X5) != $true)) | ((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X3 @ Y1) & (Y1 @ Y0))))) != X4))) & ! [X6 : b > $o] : (((^[Y0 : b]: (~ $false)) != X6) | ((X2 @ X6) = $true)) & ! [X14 : a > $o,X15 : a > $o,X16 : a > $o] : (((X0 @ X16) = $true) | (((X0 @ X15) != $true) | ((^[Y0 : a]: ((X14 @ Y0) & (X15 @ Y0))) != X16) | ((X0 @ X14) != $true))) & ! [X9 : b > $o] : (((X2 @ X9) != $true) | ! [X10 : a > $o] : (((^[Y0 : a]: (X9 @ (X1 @ Y0))) != X10) | ((X0 @ X10) = $true))) & ! [X17 : b > $o] : (((^[Y0 : b]: ($false)) != X17) | ($true = (X2 @ X17))) & ! [X11 : b > $o,X12 : (b > $o) > $o] : (((X2 @ X11) = $true) | (((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X12 @ Y1))))) != X11) | ? [X13 : b > $o] : (((X12 @ X13) = $true) & ($true != (X2 @ X13)))))))),
% 1.57/1.37 inference(ennf_transformation,[status(thm)],[f6])).
% 1.57/1.37 thf(f6,plain,(
% 1.57/1.37 ~! [X0 : (a > $o) > $o,X1 : a > b,X2 : (b > $o) > $o] : ((! [X7 : a > $o] : (((^[Y0 : a]: (~ $false)) = X7) => ((X0 @ X7) = $true)) & ! [X18 : b > $o,X19 : b > $o,X20 : b > $o] : ((((^[Y0 : b]: ((X20 @ Y0) & (X18 @ Y0))) = X19) & ((X2 @ X18) = $true) & ((X2 @ X20) = $true)) => ((X2 @ X19) = $true)) & ! [X8 : a > $o] : (((^[Y0 : a]: ($false)) = X8) => ((X0 @ X8) = $true)) & ! [X3 : (a > $o) > $o,X4 : a > $o] : ((! [X5 : a > $o] : (((X3 @ X5) = $true) => ((X0 @ X5) = $true)) & ((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X3 @ Y1) & (Y1 @ Y0))))) = X4)) => ((X0 @ X4) = $true)) & ! [X6 : b > $o] : (((^[Y0 : b]: (~ $false)) = X6) => ((X2 @ X6) = $true)) & ! [X14 : a > $o,X15 : a > $o,X16 : a > $o] : ((((X0 @ X15) = $true) & ((^[Y0 : a]: ((X14 @ Y0) & (X15 @ Y0))) = X16) & ((X0 @ X14) = $true)) => ((X0 @ X16) = $true)) & ! [X9 : b > $o] : (((X2 @ X9) = $true) => ! [X10 : a > $o] : (((^[Y0 : a]: (X9 @ (X1 @ Y0))) = X10) => ((X0 @ X10) = $true))) & ! [X17 : b > $o] : (((^[Y0 : b]: ($false)) = X17) => ($true = (X2 @ X17))) & ! [X11 : b > $o,X12 : (b > $o) > $o] : ((((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X12 @ Y1))))) = X11) & ! [X13 : b > $o] : (((X12 @ X13) = $true) => ($true = (X2 @ X13)))) => ((X2 @ X11) = $true))) => ! [X21 : b > $o] : (! [X22 : b > $o] : (((^[Y0 : b]: (~ (X21 @ Y0))) = X22) => ((X2 @ X22) = $true)) => ! [X23 : a > $o] : (((^[Y0 : a]: (X21 @ (X1 @ Y0))) = X23) => ! [X24 : a > $o] : (((^[Y0 : a]: (~ (X23 @ Y0))) = X24) => ((X0 @ X24) = $true)))))),
% 1.57/1.37 inference(rectify,[status(thm)],[f5])).
% 1.57/1.37 thf(f5,plain,(
% 1.57/1.37 ~! [X0 : (a > $o) > $o,X1 : a > b,X2 : (b > $o) > $o] : ((! [X3 : (a > $o) > $o,X4 : a > $o] : ((((^[Y0 : a]: (?? @ (a > $o) @ (^[Y1 : a > $o]: ((X3 @ Y1) & (Y1 @ Y0))))) = X4) & ! [X7 : a > $o] : (((X3 @ X7) = $true) => ((X0 @ X7) = $true))) => ((X0 @ X4) = $true)) & ! [X8 : b > $o] : (((^[Y0 : b]: (~ $false)) = X8) => ((X2 @ X8) = $true)) & ! [X10 : a > $o] : (((^[Y0 : a]: (~ $false)) = X10) => ((X0 @ X10) = $true)) & ! [X12 : a > $o] : (((^[Y0 : a]: ($false)) = X12) => ((X0 @ X12) = $true)) & ! [X14 : b > $o] : (((X2 @ X14) = $true) => ! [X15 : a > $o] : (((^[Y0 : a]: (X14 @ (X1 @ Y0))) = X15) => ((X0 @ X15) = $true))) & ! [X17 : b > $o,X18 : (b > $o) > $o] : ((! [X19 : b > $o] : (((X18 @ X19) = $true) => ((X2 @ X19) = $true)) & ((^[Y0 : b]: (?? @ (b > $o) @ (^[Y1 : b > $o]: ((Y1 @ Y0) & (X18 @ Y1))))) = X17)) => ($true = (X2 @ X17))) & ! [X22 : a > $o,X23 : a > $o,X24 : a > $o] : ((((X0 @ X23) = $true) & ((^[Y0 : a]: ((X22 @ Y0) & (X23 @ Y0))) = X24) & ((X0 @ X22) = $true)) => ((X0 @ X24) = $true)) & ! [X26 : b > $o] : (((^[Y0 : b]: ($false)) = X26) => ((X2 @ X26) = $true)) & ! [X28 : b > $o,X29 : b > $o,X30 : b > $o] : ((((^[Y0 : b]: ((X30 @ Y0) & (X28 @ Y0))) = X29) & ($true = (X2 @ X28)) & ((X2 @ X30) = $true)) => ((X2 @ X29) = $true))) => ! [X32 : b > $o] : (! [X33 : b > $o] : (((^[Y0 : b]: (~ (X32 @ Y0))) = X33) => ((X2 @ X33) = $true)) => ! [X35 : a > $o] : (((^[Y0 : a]: (X32 @ (X1 @ Y0))) = X35) => ! [X37 : a > $o] : (((^[Y0 : a]: (~ (X35 @ Y0))) = X37) => ((X0 @ X37) = $true)))))),
% 1.57/1.37 inference(fool_elimination,[status(thm)],[f4])).
% 1.57/1.37 thf(f4,plain,(
% 1.57/1.37 ~! [X0 : (a > $o) > $o,X1 : a > b,X2 : (b > $o) > $o] : ((! [X3 : (a > $o) > $o,X4 : a > $o] : ((((^[X5 : a] : (? [X6 : a > $o] : ((X6 @ X5) & (X3 @ X6)))) = X4) & ! [X7 : a > $o] : ((X3 @ X7) => (X0 @ X7))) => (X0 @ X4)) & ! [X8 : b > $o] : (((^[X9 : b] : (~$false)) = X8) => (X2 @ X8)) & ! [X10 : a > $o] : (((^[X11 : a] : (~$false)) = X10) => (X0 @ X10)) & ! [X12 : a > $o] : (((^[X13 : a] : ($false)) = X12) => (X0 @ X12)) & ! [X14 : b > $o] : ((X2 @ X14) => ! [X15 : a > $o] : (((^[X16 : a] : (X14 @ (X1 @ X16))) = X15) => (X0 @ X15))) & ! [X17 : b > $o,X18 : (b > $o) > $o] : ((! [X19 : b > $o] : ((X18 @ X19) => (X2 @ X19)) & ((^[X20 : b] : (? [X21 : b > $o] : ((X18 @ X21) & (X21 @ X20)))) = X17)) => (X2 @ X17)) & ! [X22 : a > $o,X23 : a > $o,X24 : a > $o] : (((X0 @ X23) & (X24 = (^[X25 : a] : ((X23 @ X25) & (X22 @ X25)))) & (X0 @ X22)) => (X0 @ X24)) & ! [X26 : b > $o] : ((X26 = (^[X27 : b] : ($false))) => (X2 @ X26)) & ! [X28 : b > $o,X29 : b > $o,X30 : b > $o] : ((((^[X31 : b] : ((X28 @ X31) & (X30 @ X31))) = X29) & (X2 @ X28) & (X2 @ X30)) => (X2 @ X29))) => ! [X32 : b > $o] : (! [X33 : b > $o] : ((X33 = (^[X34 : b] : (~(X32 @ X34)))) => (X2 @ X33)) => ! [X35 : a > $o] : (((^[X36 : a] : (X32 @ (X1 @ X36))) = X35) => ! [X37 : a > $o] : (((^[X38 : a] : (~(X35 @ X38))) = X37) => (X0 @ X37)))))),
% 1.57/1.37 inference(rectify,[status(thm)],[f2])).
% 1.57/1.37 thf(f2,negated_conjecture,(
% 1.57/1.37 ~! [X0 : (a > $o) > $o,X2 : a > b,X1 : (b > $o) > $o] : ((! [X5 : (a > $o) > $o,X3 : a > $o] : ((((^[X4 : a] : (? [X6 : a > $o] : ((X6 @ X4) & (X5 @ X6)))) = X3) & ! [X4 : a > $o] : ((X5 @ X4) => (X0 @ X4))) => (X0 @ X3)) & ! [X3 : b > $o] : (((^[X4 : b] : (~$false)) = X3) => (X1 @ X3)) & ! [X3 : a > $o] : (((^[X4 : a] : (~$false)) = X3) => (X0 @ X3)) & ! [X3 : a > $o] : (((^[X4 : a] : ($false)) = X3) => (X0 @ X3)) & ! [X9 : b > $o] : ((X1 @ X9) => ! [X7 : a > $o] : (((^[X10 : a] : (X9 @ (X2 @ X10))) = X7) => (X0 @ X7))) & ! [X3 : b > $o,X5 : (b > $o) > $o] : ((! [X4 : b > $o] : ((X5 @ X4) => (X1 @ X4)) & ((^[X4 : b] : (? [X6 : b > $o] : ((X5 @ X6) & (X6 @ X4)))) = X3)) => (X1 @ X3)) & ! [X7 : a > $o,X8 : a > $o,X6 : a > $o] : (((X0 @ X8) & (X6 = (^[X4 : a] : ((X8 @ X4) & (X7 @ X4)))) & (X0 @ X7)) => (X0 @ X6)) & ! [X3 : b > $o] : ((X3 = (^[X4 : b] : ($false))) => (X1 @ X3)) & ! [X8 : b > $o,X6 : b > $o,X7 : b > $o] : ((((^[X4 : b] : ((X8 @ X4) & (X7 @ X4))) = X6) & (X1 @ X8) & (X1 @ X7)) => (X1 @ X6))) => ! [X9 : b > $o] : (! [X3 : b > $o] : ((X3 = (^[X4 : b] : (~(X9 @ X4)))) => (X1 @ X3)) => ! [X7 : a > $o] : (((^[X10 : a] : (X9 @ (X2 @ X10))) = X7) => ! [X3 : a > $o] : (((^[X4 : a] : (~(X7 @ X4))) = X3) => (X0 @ X3)))))),
% 1.57/1.37 inference(negated_conjecture,[status(cth)],[f1])).
% 1.57/1.37 thf(f1,conjecture,(
% 1.57/1.37 ! [X0 : (a > $o) > $o,X2 : a > b,X1 : (b > $o) > $o] : ((! [X5 : (a > $o) > $o,X3 : a > $o] : ((((^[X4 : a] : (? [X6 : a > $o] : ((X6 @ X4) & (X5 @ X6)))) = X3) & ! [X4 : a > $o] : ((X5 @ X4) => (X0 @ X4))) => (X0 @ X3)) & ! [X3 : b > $o] : (((^[X4 : b] : (~$false)) = X3) => (X1 @ X3)) & ! [X3 : a > $o] : (((^[X4 : a] : (~$false)) = X3) => (X0 @ X3)) & ! [X3 : a > $o] : (((^[X4 : a] : ($false)) = X3) => (X0 @ X3)) & ! [X9 : b > $o] : ((X1 @ X9) => ! [X7 : a > $o] : (((^[X10 : a] : (X9 @ (X2 @ X10))) = X7) => (X0 @ X7))) & ! [X3 : b > $o,X5 : (b > $o) > $o] : ((! [X4 : b > $o] : ((X5 @ X4) => (X1 @ X4)) & ((^[X4 : b] : (? [X6 : b > $o] : ((X5 @ X6) & (X6 @ X4)))) = X3)) => (X1 @ X3)) & ! [X7 : a > $o,X8 : a > $o,X6 : a > $o] : (((X0 @ X8) & (X6 = (^[X4 : a] : ((X8 @ X4) & (X7 @ X4)))) & (X0 @ X7)) => (X0 @ X6)) & ! [X3 : b > $o] : ((X3 = (^[X4 : b] : ($false))) => (X1 @ X3)) & ! [X8 : b > $o,X6 : b > $o,X7 : b > $o] : ((((^[X4 : b] : ((X8 @ X4) & (X7 @ X4))) = X6) & (X1 @ X8) & (X1 @ X7)) => (X1 @ X6))) => ! [X9 : b > $o] : (! [X3 : b > $o] : ((X3 = (^[X4 : b] : (~(X9 @ X4)))) => (X1 @ X3)) => ! [X7 : a > $o] : (((^[X10 : a] : (X9 @ (X2 @ X10))) = X7) => ! [X3 : a > $o] : (((^[X4 : a] : (~(X7 @ X4))) = X3) => (X0 @ X3)))))),
% 1.57/1.37 file('/export/starexec/sandbox/tmp/tmp.mBP11uJTB9/DTF2THF_29967.p',cCLOSED_THM1_pme)).
% 1.57/1.37 thf(f61,plain,(
% 1.57/1.37 ((sK2 @ (^[Y0 : b]: (~ (sK3 @ Y0)))) != $true)),
% 1.57/1.37 inference(beta_eta_normalization,[status(thm)],[f60])).
% 1.57/1.37 thf(f60,plain,(
% 1.57/1.37 ((sK2 @ (^[Y0 : b]: (~ ((^[Y1 : b]: (sK3 @ ((^[Y2 : b]: (Y2)) @ Y1))) @ Y0)))) != $true)),
% 1.57/1.37 inference(trivial_inequality_removal,[status(thm)],[f59])).
% 1.57/1.37 thf(f59,plain,(
% 1.57/1.37 ($true != $true) | ((sK2 @ (^[Y0 : b]: (~ ((^[Y1 : b]: (sK3 @ ((^[Y2 : b]: (Y2)) @ Y1))) @ Y0)))) != $true)),
% 1.57/1.37 inference(superposition,[status(thm)],[f48,f45])).
% 1.57/1.37 thf(f45,plain,(
% 1.57/1.37 ( ! [X23 : b > $o] : (((sK0 @ (^[Y0 : a]: (X23 @ (sK1 @ Y0)))) = $true) | ((sK2 @ X23) != $true)) )),
% 1.57/1.37 inference(equality_resolution,[status(thm)],[f17])).
% 1.57/1.37 thf(f17,plain,(
% 1.57/1.37 ( ! [X24 : a > $o,X23 : b > $o] : (((sK2 @ X23) != $true) | ((^[Y0 : a]: (X23 @ (sK1 @ Y0))) != X24) | ((sK0 @ X24) = $true)) )),
% 1.57/1.37 inference(cnf_transformation,[status(thm)],[f16])).
% 1.57/1.37 thf(f48,plain,(
% 1.57/1.37 ((sK0 @ (^[Y0 : a]: (~ (sK3 @ (sK1 @ Y0))))) != $true)),
% 1.57/1.37 inference(beta_eta_normalization,[status(thm)],[f33])).
% 1.57/1.37 thf(f33,plain,(
% 1.57/1.37 ((sK0 @ (^[Y0 : a]: (~ ((^[Y1 : a]: (sK3 @ (sK1 @ Y1))) @ Y0)))) != $true)),
% 1.57/1.37 inference(definition_unfolding,[status(thm)],[f30,f32])).
% 1.57/1.37 thf(f32,plain,(
% 1.57/1.37 ((^[Y0 : a]: (~ ((^[Y1 : a]: (sK3 @ (sK1 @ Y1))) @ Y0))) = sK5)),
% 1.57/1.37 inference(definition_unfolding,[status(thm)],[f29,f31])).
% 1.57/1.37 thf(f31,plain,(
% 1.57/1.37 ((^[Y0 : a]: (sK3 @ (sK1 @ Y0))) = sK4)),
% 1.57/1.37 inference(cnf_transformation,[status(thm)],[f16])).
% 1.57/1.37 thf(f29,plain,(
% 1.57/1.37 (sK5 = (^[Y0 : a]: (~ (sK4 @ Y0))))),
% 1.57/1.37 inference(cnf_transformation,[status(thm)],[f16])).
% 1.57/1.37 thf(f30,plain,(
% 1.57/1.37 ((sK0 @ sK5) != $true)),
% 1.57/1.37 inference(cnf_transformation,[status(thm)],[f16])).
% 1.57/1.37 % SZS output end Proof for DTF2THF_29967
% 1.57/1.37 % (30064)------------------------------
% 1.57/1.37 % (30064)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.57/1.37 % (30064)Termination reason: Refutation
% 1.57/1.37
% 1.57/1.37 % (30064)Memory used [KB]: 5628
% 1.57/1.37 % (30064)Time elapsed: 0.007 s
% 1.57/1.37 % (30064)Instructions burned: 8 (million)
% 1.57/1.37 % (30064)------------------------------
% 1.57/1.37 % (30064)------------------------------
% 1.57/1.37 % (30063)Success in time 0.017 s
%------------------------------------------------------------------------------