%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n025.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 : Tue May 5 06:58:55 PM UTC 2026
% Result : Theorem 1.91s 1.84s
% Output : Refutation 1.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 9
% Syntax : Number of formulae : 102 ( 24 unt; 0 typ; 6 def)
% Number of atoms : 1587 ( 345 equ; 0 cnn)
% Maximal formula atoms : 24 ( 15 avg)
% Number of connectives : 3097 ( 471 ~; 510 |; 208 &;1651 @)
% ( 6 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Number of types : 4 ( 2 usr)
% Number of type conns : 245 ( 245 >; 0 *; 0 +; 0 <<)
% Number of symbols : 42 ( 38 usr; 15 con; 0-3 aty)
% ( 245 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 756 ( 620 ^; 128 !; 8 ?; 756 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_6,type,
d_unsorted: $tType ).
thf(func_def_0,type,
unsorted: $tType ).
thf(func_def_1,type,
irel: $i > $i > $o ).
thf(func_def_2,type,
mnot: ( $i > $o ) > $i > $o ).
thf(func_def_3,type,
mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_4,type,
mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_5,type,
mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_6,type,
mbox_s4: ( $i > $o ) > $i > $o ).
thf(func_def_7,type,
iatom: ( $i > $o ) > $i > $o ).
thf(func_def_8,type,
inot: ( $i > $o ) > $i > $o ).
thf(func_def_9,type,
itrue: $i > $o ).
thf(func_def_10,type,
ifalse: $i > $o ).
thf(func_def_11,type,
iand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_12,type,
ior: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_13,type,
iimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_14,type,
iimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_15,type,
iequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_16,type,
ixor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_17,type,
ivalid: ( $i > $o ) > $o ).
thf(func_def_18,type,
isatisfiable: ( $i > $o ) > $o ).
thf(func_def_19,type,
icountersatisfiable: ( $i > $o ) > $o ).
thf(func_def_20,type,
iinvalid: ( $i > $o ) > $o ).
thf(func_def_21,type,
d_unsorted: $tType ).
thf(func_def_22,type,
d2unsorted: d_unsorted > $i ).
thf(func_def_23,type,
d_unsorted_0: d_unsorted ).
thf(func_def_25,type,
vEPSILON:
!>[X0: $tType] : ( ( X0 > $o ) > X0 ) ).
thf(func_def_42,type,
sK0: $i > d_unsorted ).
thf(func_def_44,type,
ph2:
!>[X0: $tType] : X0 ).
thf(func_def_45,type,
sK3: $i > $o ).
thf(func_def_46,type,
sK4: $i > $o ).
thf(f321,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f160,f179,f217,f264,f280,f291,f320]) ).
thf(f320,plain,
( ~ spl1_2
| ~ spl1_6 ),
inference(avatar_contradiction_clause,[status(thm)],[f319]) ).
thf(f319,plain,
( $false
| ~ spl1_2
| ~ spl1_6 ),
inference(trivial_inequality_removal,[status(thm)],[f315]) ).
thf(f315,plain,
( ( $true = $false )
| ~ spl1_2
| ~ spl1_6 ),
inference(superposition,[status(thm)],[f178,f298]) ).
thf(f298,plain,
( ! [X0: $i] :
( ( sK3 @ X0 )
= $true )
| ~ spl1_2 ),
inference(superposition,[status(thm)],[f296,f49]) ).
thf(f49,plain,
! [X0: $i,X1: $i] : ( X0 = X1 ),
inference(superposition,[status(thm)],[f45,f45]) ).
thf(f45,plain,
! [X3: $i] :
( ( d2unsorted @ d_unsorted_0 )
= X3 ),
inference(forward_demodulation,[status(thm)],[f24,f27]) ).
thf(f27,plain,
! [X2: d_unsorted] : ( d_unsorted_0 = X2 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f15,plain,
( ( ixor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
~ ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( ~ ( irel @ Y6 @ Y4 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y4 @ Y8 )
| ( Y0 @ Y8 ) ) )
| ( Y1 @ Y7 )
| ~ ( irel @ Y4 @ Y7 ) )
& ( ~ ( irel @ Y6 @ Y3 )
| ~ ( irel @ Y3 @ Y5 )
| ( Y0 @ Y5 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y3 @ Y8 )
| ( Y1 @ Y8 ) ) ) ) )
| ~ ( irel @ Y2 @ Y6 ) ) ) ) ) ) ) ) )
& ( inot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( !! @ $i
@ ^ [Y2: $i] :
( ( Y0 @ Y2 )
| ~ ( irel @ Y1 @ Y2 ) ) ) ) )
& ( ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
!= $true )
& ( icountersatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( isatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) )
& ( ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
& ( Y0 @ Y2 ) ) ) )
& ! [X0: d_unsorted,X1: d_unsorted] :
( ( X0 = X1 )
| ( ( d2unsorted @ X1 )
!= ( d2unsorted @ X0 ) ) )
& ( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y4 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y4 @ Y5 )
| ( Y0 @ Y5 ) ) )
| ~ ( irel @ Y2 @ Y4 )
| ( Y1 @ Y3 ) ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y3 @ Y5 )
| ( Y1 @ Y5 ) ) )
| ( Y0 @ Y4 )
| ~ ( irel @ Y3 @ Y4 ) ) ) ) ) ) )
& ( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ~ ( Y0 @ Y2 ) ) ) )
& ( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ! [X2: d_unsorted] : ( d_unsorted_0 = X2 )
& ( iatom
= ( ^ [Y0: $i > $o,Y1: $i] : ( Y0 @ Y1 ) ) )
& ( iinvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ! [X3: $i] :
( ( d2unsorted @ ( sK0 @ X3 ) )
= X3 )
& ( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) ) ) ) )
& ( ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iimplied
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) )
| ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) )
& ( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) )
& ( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0])],[f13,f14]) ).
thf(f14,plain,
! [X3: $i] :
( ? [X4: d_unsorted] :
( ( d2unsorted @ X4 )
= X3 )
=> ( ( d2unsorted @ ( sK0 @ X3 ) )
= X3 ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f13,plain,
( ( ixor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
~ ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( ~ ( irel @ Y6 @ Y4 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y4 @ Y8 )
| ( Y0 @ Y8 ) ) )
| ( Y1 @ Y7 )
| ~ ( irel @ Y4 @ Y7 ) )
& ( ~ ( irel @ Y6 @ Y3 )
| ~ ( irel @ Y3 @ Y5 )
| ( Y0 @ Y5 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y3 @ Y8 )
| ( Y1 @ Y8 ) ) ) ) )
| ~ ( irel @ Y2 @ Y6 ) ) ) ) ) ) ) ) )
& ( inot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( !! @ $i
@ ^ [Y2: $i] :
( ( Y0 @ Y2 )
| ~ ( irel @ Y1 @ Y2 ) ) ) ) )
& ( ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
!= $true )
& ( icountersatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( isatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) )
& ( ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
& ( Y0 @ Y2 ) ) ) )
& ! [X0: d_unsorted,X1: d_unsorted] :
( ( X0 = X1 )
| ( ( d2unsorted @ X1 )
!= ( d2unsorted @ X0 ) ) )
& ( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y4 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y4 @ Y5 )
| ( Y0 @ Y5 ) ) )
| ~ ( irel @ Y2 @ Y4 )
| ( Y1 @ Y3 ) ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y3 @ Y5 )
| ( Y1 @ Y5 ) ) )
| ( Y0 @ Y4 )
| ~ ( irel @ Y3 @ Y4 ) ) ) ) ) ) )
& ( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ~ ( Y0 @ Y2 ) ) ) )
& ( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ! [X2: d_unsorted] : ( d_unsorted_0 = X2 )
& ( iatom
= ( ^ [Y0: $i > $o,Y1: $i] : ( Y0 @ Y1 ) ) )
& ( iinvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ! [X3: $i] :
? [X4: d_unsorted] :
( ( d2unsorted @ X4 )
= X3 )
& ( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) ) ) ) )
& ( ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iimplied
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) )
| ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) )
& ( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) )
& ( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ) ),
inference(rectify,[status(thm)],[f12]) ).
thf(f12,plain,
( ( ixor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
~ ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( ~ ( irel @ Y6 @ Y4 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y4 @ Y8 )
| ( Y0 @ Y8 ) ) )
| ( Y1 @ Y7 )
| ~ ( irel @ Y4 @ Y7 ) )
& ( ~ ( irel @ Y6 @ Y3 )
| ~ ( irel @ Y3 @ Y5 )
| ( Y0 @ Y5 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y3 @ Y8 )
| ( Y1 @ Y8 ) ) ) ) )
| ~ ( irel @ Y2 @ Y6 ) ) ) ) ) ) ) ) )
& ( inot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( !! @ $i
@ ^ [Y2: $i] :
( ( Y0 @ Y2 )
| ~ ( irel @ Y1 @ Y2 ) ) ) ) )
& ( ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
!= $true )
& ( icountersatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( isatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) )
& ( ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
& ( Y0 @ Y2 ) ) ) )
& ! [X2: d_unsorted,X3: d_unsorted] :
( ( X2 = X3 )
| ( ( d2unsorted @ X2 )
!= ( d2unsorted @ X3 ) ) )
& ( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y4 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y4 @ Y5 )
| ( Y0 @ Y5 ) ) )
| ~ ( irel @ Y2 @ Y4 )
| ( Y1 @ Y3 ) ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y3 @ Y5 )
| ( Y1 @ Y5 ) ) )
| ( Y0 @ Y4 )
| ~ ( irel @ Y3 @ Y4 ) ) ) ) ) ) )
& ( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ~ ( Y0 @ Y2 ) ) ) )
& ( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ! [X4: d_unsorted] : ( d_unsorted_0 = X4 )
& ( iatom
= ( ^ [Y0: $i > $o,Y1: $i] : ( Y0 @ Y1 ) ) )
& ( iinvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ! [X0: $i] :
? [X1: d_unsorted] :
( ( d2unsorted @ X1 )
= X0 )
& ( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) ) ) ) )
& ( ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iimplied
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) )
| ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) )
& ( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) )
& ( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ) ),
inference(ennf_transformation,[status(thm)],[f10]) ).
thf(f10,plain,
( ( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) )
& ! [X4: d_unsorted] : ( d_unsorted_0 = X4 )
& ( ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
!= $true )
& ( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
& ( Y0 @ Y2 ) ) ) )
& ( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) ) ) ) )
& ( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y4 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y4 @ Y5 )
| ( Y0 @ Y5 ) ) )
| ~ ( irel @ Y2 @ Y4 )
| ( Y1 @ Y3 ) ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y3 @ Y5 )
| ( Y1 @ Y5 ) ) )
| ( Y0 @ Y4 )
| ~ ( irel @ Y3 @ Y4 ) ) ) ) ) ) )
& ! [X0: $i] :
? [X1: d_unsorted] :
( ( d2unsorted @ X1 )
= X0 )
& ( inot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( !! @ $i
@ ^ [Y2: $i] :
( ( Y0 @ Y2 )
| ~ ( irel @ Y1 @ Y2 ) ) ) ) )
& ( iinvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ( iimplied
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) )
| ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( icountersatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) )
& ( iatom
= ( ^ [Y0: $i > $o,Y1: $i] : ( Y0 @ Y1 ) ) )
& ( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ~ ( Y0 @ Y2 ) ) ) )
& ( ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) )
& ( ixor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
~ ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( ~ ( irel @ Y6 @ Y4 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y4 @ Y8 )
| ( Y0 @ Y8 ) ) )
| ( Y1 @ Y7 )
| ~ ( irel @ Y4 @ Y7 ) )
& ( ~ ( irel @ Y6 @ Y3 )
| ~ ( irel @ Y3 @ Y5 )
| ( Y0 @ Y5 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y3 @ Y8 )
| ( Y1 @ Y8 ) ) ) ) )
| ~ ( irel @ Y2 @ Y6 ) ) ) ) ) ) ) ) )
& ! [X2: d_unsorted,X3: d_unsorted] :
( ( ( d2unsorted @ X2 )
= ( d2unsorted @ X3 ) )
=> ( X2 = X3 ) )
& ( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( isatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ) ),
inference(flattening,[status(thm)],[f9]) ).
thf(f9,plain,
( ( iatom
= ( ^ [Y0: $i > $o,Y1: $i] : ( Y0 @ Y1 ) ) )
& ( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y4 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y4 @ Y5 )
| ( Y0 @ Y5 ) ) )
| ~ ( irel @ Y2 @ Y4 )
| ( Y1 @ Y3 ) ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y3 @ Y5 )
| ( Y1 @ Y5 ) ) )
| ( Y0 @ Y4 )
| ~ ( irel @ Y3 @ Y4 ) ) ) ) ) ) )
& ( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) )
& ( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ~ ( Y0 @ Y2 ) ) ) )
& ( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( isatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ! [X0: $i] :
? [X1: d_unsorted] :
( ( d2unsorted @ X1 )
= X0 )
& ! [X2: d_unsorted,X3: d_unsorted] :
( ( ( d2unsorted @ X2 )
= ( d2unsorted @ X3 ) )
=> ( X2 = X3 ) )
& ( icountersatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) )
& ( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( ixor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
~ ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( ~ ( irel @ Y6 @ Y4 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y4 @ Y8 )
| ( Y0 @ Y8 ) ) )
| ( Y1 @ Y7 )
| ~ ( irel @ Y4 @ Y7 ) )
& ( ~ ( irel @ Y6 @ Y3 )
| ~ ( irel @ Y3 @ Y5 )
| ( Y0 @ Y5 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y3 @ Y8 )
| ( Y1 @ Y8 ) ) ) ) )
| ~ ( irel @ Y2 @ Y6 ) ) ) ) ) ) ) ) )
& ( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
& ( Y0 @ Y2 ) ) ) )
& ( inot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( !! @ $i
@ ^ [Y2: $i] :
( ( Y0 @ Y2 )
| ~ ( irel @ Y1 @ Y2 ) ) ) ) )
& ! [X4: d_unsorted] : ( d_unsorted_0 = X4 )
& ( iimplied
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) )
| ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iinvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) ) ) ) )
& ( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) )
& ( ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
!= $true )
& ( ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
= $true ) ),
inference(rectify,[status(thm)],[f6]) ).
thf(f6,plain,
( ( iatom
= ( ^ [Y0: $i > $o,Y1: $i] : ( Y0 @ Y1 ) ) )
& ( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y4 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y4 @ Y5 )
| ( Y0 @ Y5 ) ) )
| ~ ( irel @ Y2 @ Y4 )
| ( Y1 @ Y3 ) ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ~ ( !! @ $i
@ ^ [Y5: $i] :
( ~ ( irel @ Y3 @ Y5 )
| ( Y1 @ Y5 ) ) )
| ( Y0 @ Y4 )
| ~ ( irel @ Y3 @ Y4 ) ) ) ) ) ) )
& ( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) )
& ( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ~ ( Y0 @ Y2 ) ) ) )
& ( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( isatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ! [X24: $i] :
? [X25: d_unsorted] :
( ( d2unsorted @ X25 )
= X24 )
& ! [X26: d_unsorted,X27: d_unsorted] :
( ( ( d2unsorted @ X26 )
= ( d2unsorted @ X27 ) )
=> ( X26 = X27 ) )
& ( icountersatisfiable
= ( ^ [Y0: $i > $o] :
~ ( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) )
& ( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) )
& ( ixor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
~ ( !! @ $i
@ ^ [Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( !! @ $i
@ ^ [Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( !! @ $i
@ ^ [Y7: $i] :
( ( ( ~ ( irel @ Y6 @ Y4 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y4 @ Y8 )
| ( Y0 @ Y8 ) ) )
| ( Y1 @ Y7 )
| ~ ( irel @ Y4 @ Y7 ) )
& ( ~ ( irel @ Y6 @ Y3 )
| ~ ( irel @ Y3 @ Y5 )
| ( Y0 @ Y5 )
| ~ ( !! @ $i
@ ^ [Y8: $i] :
( ~ ( irel @ Y3 @ Y8 )
| ( Y1 @ Y8 ) ) ) ) )
| ~ ( irel @ Y2 @ Y6 ) ) ) ) ) ) ) ) )
& ( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
& ( Y0 @ Y2 ) ) ) )
& ( inot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( !! @ $i
@ ^ [Y2: $i] :
( ( Y0 @ Y2 )
| ~ ( irel @ Y1 @ Y2 ) ) ) ) )
& ! [X51: d_unsorted] : ( d_unsorted_0 = X51 )
& ( iimplied
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ( Y0 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) )
| ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iinvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] :
~ ( Y0 @ Y1 ) ) ) )
& ( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ~ ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) )
& ( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
& ( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( irel @ Y2 @ Y3 ) ) ) ) ) )
& ( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) )
& ( ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
= $true )
& ( ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
!= $true )
& ( ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
= $true ) ),
inference(fool_elimination,[status(thm)],[f5]) ).
thf(f5,plain,
( ( ( ^ [X0: $i > $o,X1: $i] : ( X0 @ X1 ) )
= iatom )
& ( iequiv
= ( ^ [X2: $i > $o,X3: $i > $o,X4: $i] :
( ! [X5: $i,X6: $i] :
( ~ ( irel @ X6 @ X5 )
| ( X2 @ X5 )
| ~ ! [X7: $i] :
( ( X3 @ X7 )
| ~ ( irel @ X6 @ X7 ) )
| ~ ( irel @ X4 @ X6 ) )
& ! [X8: $i,X9: $i] :
( ( X3 @ X9 )
| ~ ( irel @ X4 @ X8 )
| ~ ! [X10: $i] :
( ( X2 @ X10 )
| ~ ( irel @ X8 @ X10 ) )
| ~ ( irel @ X8 @ X9 ) ) ) ) )
& ( mbox_s4
= ( ^ [X11: $i > $o,X12: $i] :
! [X13: $i] :
( ( X11 @ X13 )
| ~ ( irel @ X12 @ X13 ) ) ) )
& ( ( ^ [X14: $i > $o,X15: $i > $o,X16: $i] :
( ~ ( X14 @ X16 )
| ( X15 @ X16 ) ) )
= mimplies )
& ( ( ^ [X17: $i > $o,X18: $i > $o,X19: $i] :
( ! [X20: $i] :
( ( X18 @ X20 )
| ~ ( irel @ X19 @ X20 ) )
| ! [X21: $i] :
( ( X17 @ X21 )
| ~ ( irel @ X19 @ X21 ) ) ) )
= ior )
& ( ( ^ [X22: $i > $o] :
~ ! [X23: $i] :
~ ( X22 @ X23 ) )
= isatisfiable )
& ! [X24: $i] :
? [X25: d_unsorted] :
( ( d2unsorted @ X25 )
= X24 )
& ! [X26: d_unsorted,X27: d_unsorted] :
( ( ( d2unsorted @ X26 )
= ( d2unsorted @ X27 ) )
=> ( X26 = X27 ) )
& ( icountersatisfiable
= ( ^ [X28: $i > $o] :
~ ! [X29: $i] : ( X28 @ X29 ) ) )
& ( ( ^ [X30: $i > $o,X31: $i > $o,X32: $i] :
( ( X30 @ X32 )
| ( X31 @ X32 ) ) )
= mor )
& ( ivalid
= ( ^ [X33: $i > $o] :
! [X34: $i] : ( X33 @ X34 ) ) )
& ( ( ^ [X35: $i > $o,X36: $i > $o,X37: $i] :
~ ! [X38: $i,X39: $i,X40: $i,X41: $i,X42: $i] :
( ~ ( irel @ X37 @ X39 )
| ( ( ~ ! [X43: $i] :
( ( X36 @ X43 )
| ~ ( irel @ X42 @ X43 ) )
| ( X35 @ X40 )
| ~ ( irel @ X42 @ X40 )
| ~ ( irel @ X39 @ X42 ) )
& ( ~ ( irel @ X41 @ X38 )
| ( X36 @ X38 )
| ~ ! [X44: $i] :
( ( X35 @ X44 )
| ~ ( irel @ X41 @ X44 ) )
| ~ ( irel @ X39 @ X41 ) ) ) ) )
= ixor )
& ( mand
= ( ^ [X45: $i > $o,X46: $i > $o,X47: $i] :
( ( X45 @ X47 )
& ( X46 @ X47 ) ) ) )
& ( ( ^ [X48: $i > $o,X49: $i] :
~ ! [X50: $i] :
( ~ ( irel @ X49 @ X50 )
| ( X48 @ X50 ) ) )
= inot )
& ! [X51: d_unsorted] : ( d_unsorted_0 = X51 )
& ( iimplied
= ( ^ [X52: $i > $o,X53: $i > $o,X54: $i] :
( ~ ! [X55: $i] :
( ( X53 @ X55 )
| ~ ( irel @ X54 @ X55 ) )
| ! [X56: $i] :
( ~ ( irel @ X54 @ X56 )
| ( X52 @ X56 ) ) ) ) )
& ( ( ^ [X57: $i > $o] :
! [X58: $i] :
~ ( X57 @ X58 ) )
= iinvalid )
& ( ( ^ [X59: $i > $o,X60: $i > $o,X61: $i] :
( ! [X62: $i] :
( ( X60 @ X62 )
| ~ ( irel @ X61 @ X62 ) )
| ~ ! [X63: $i] :
( ( X59 @ X63 )
| ~ ( irel @ X61 @ X63 ) ) ) )
= iimplies )
& ( iand
= ( ^ [X64: $i > $o,X65: $i > $o,X66: $i] :
( ! [X67: $i] :
( ~ ( irel @ X66 @ X67 )
| ( X65 @ X67 ) )
& ! [X68: $i] :
( ( X64 @ X68 )
| ~ ( irel @ X66 @ X68 ) ) ) ) )
& ( ( ^ [X69: $i > $o,X70: $i] :
~ ( X69 @ X70 ) )
= mnot )
& ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
& ~ ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
& ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) ) ),
inference(rectify,[status(thm)],[f1]) ).
thf(f1,axiom,
( ( ( ^ [X8: $i > $o,X7: $i] : ( X8 @ X7 ) )
= iatom )
& ( iequiv
= ( ^ [X8: $i > $o,X9: $i > $o,X7: $i] :
( ! [X12: $i,X5: $i] :
( ~ ( irel @ X5 @ X12 )
| ( X8 @ X12 )
| ~ ! [X13: $i] :
( ( X9 @ X13 )
| ~ ( irel @ X5 @ X13 ) )
| ~ ( irel @ X7 @ X5 ) )
& ! [X5: $i,X10: $i] :
( ( X9 @ X10 )
| ~ ( irel @ X7 @ X5 )
| ~ ! [X11: $i] :
( ( X8 @ X11 )
| ~ ( irel @ X5 @ X11 ) )
| ~ ( irel @ X5 @ X10 ) ) ) ) )
& ( mbox_s4
= ( ^ [X8: $i > $o,X4: $i] :
! [X5: $i] :
( ( X8 @ X5 )
| ~ ( irel @ X4 @ X5 ) ) ) )
& ( ( ^ [X0: $i > $o,X6: $i > $o,X7: $i] :
( ~ ( X0 @ X7 )
| ( X6 @ X7 ) ) )
= mimplies )
& ( ( ^ [X8: $i > $o,X9: $i > $o,X7: $i] :
( ! [X5: $i] :
( ( X9 @ X5 )
| ~ ( irel @ X7 @ X5 ) )
| ! [X5: $i] :
( ( X8 @ X5 )
| ~ ( irel @ X7 @ X5 ) ) ) )
= ior )
& ( ( ^ [X18: $i > $o] :
~ ! [X19: $i] :
~ ( X18 @ X19 ) )
= isatisfiable )
& ! [X0: $i] :
? [X1: d_unsorted] :
( ( d2unsorted @ X1 )
= X0 )
& ! [X2: d_unsorted,X3: d_unsorted] :
( ( ( d2unsorted @ X2 )
= ( d2unsorted @ X3 ) )
=> ( X2 = X3 ) )
& ( icountersatisfiable
= ( ^ [X18: $i > $o] :
~ ! [X19: $i] : ( X18 @ X19 ) ) )
& ( ( ^ [X4: $i > $o,X5: $i > $o,X0: $i] :
( ( X4 @ X0 )
| ( X5 @ X0 ) ) )
= mor )
& ( ivalid
= ( ^ [X18: $i > $o] :
! [X19: $i] : ( X18 @ X19 ) ) )
& ( ( ^ [X8: $i > $o,X9: $i > $o,X7: $i] :
~ ! [X15: $i,X5: $i,X17: $i,X14: $i,X16: $i] :
( ~ ( irel @ X7 @ X5 )
| ( ( ~ ! [X13: $i] :
( ( X9 @ X13 )
| ~ ( irel @ X16 @ X13 ) )
| ( X8 @ X17 )
| ~ ( irel @ X16 @ X17 )
| ~ ( irel @ X5 @ X16 ) )
& ( ~ ( irel @ X14 @ X15 )
| ( X9 @ X15 )
| ~ ! [X11: $i] :
( ( X8 @ X11 )
| ~ ( irel @ X14 @ X11 ) )
| ~ ( irel @ X5 @ X14 ) ) ) ) )
= ixor )
& ( mand
= ( ^ [X4: $i > $o,X5: $i > $o,X0: $i] :
( ( X4 @ X0 )
& ( X5 @ X0 ) ) ) )
& ( ( ^ [X8: $i > $o,X7: $i] :
~ ! [X5: $i] :
( ~ ( irel @ X7 @ X5 )
| ( X8 @ X5 ) ) )
= inot )
& ! [X1: d_unsorted] : ( d_unsorted_0 = X1 )
& ( iimplied
= ( ^ [X8: $i > $o,X9: $i > $o,X7: $i] :
( ~ ! [X5: $i] :
( ( X9 @ X5 )
| ~ ( irel @ X7 @ X5 ) )
| ! [X5: $i] :
( ~ ( irel @ X7 @ X5 )
| ( X8 @ X5 ) ) ) ) )
& ( ( ^ [X18: $i > $o] :
! [X19: $i] :
~ ( X18 @ X19 ) )
= iinvalid )
& ( ( ^ [X8: $i > $o,X9: $i > $o,X7: $i] :
( ! [X5: $i] :
( ( X9 @ X5 )
| ~ ( irel @ X7 @ X5 ) )
| ~ ! [X5: $i] :
( ( X8 @ X5 )
| ~ ( irel @ X7 @ X5 ) ) ) )
= iimplies )
& ( iand
= ( ^ [X8: $i > $o,X9: $i > $o,X7: $i] :
( ! [X5: $i] :
( ~ ( irel @ X7 @ X5 )
| ( X9 @ X5 ) )
& ! [X5: $i] :
( ( X8 @ X5 )
| ~ ( irel @ X7 @ X5 ) ) ) ) )
& ( ( ^ [X4: $i > $o,X0: $i] :
~ ( X4 @ X0 ) )
= mnot )
& ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
& ~ ( ifalse @ ( d2unsorted @ d_unsorted_0 ) )
& ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.rHa6s2wqLE/DTF2THF_22212.p',lcl696_1) ).
thf(f24,plain,
! [X3: $i] :
( ( d2unsorted @ ( sK0 @ X3 ) )
= X3 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f296,plain,
( ( ( sK3 @ sK5 )
= $true )
| ~ spl1_2 ),
inference(trivial_inequality_removal,[status(thm)],[f294]) ).
thf(f294,plain,
( ( $true = $false )
| ( ( sK3 @ sK5 )
= $true )
| ~ spl1_2 ),
inference(superposition,[status(thm)],[f159,f67]) ).
thf(f67,plain,
! [X0: $i] :
( $true
= ( irel @ X0 @ X0 ) ),
inference(superposition,[status(thm)],[f22,f45]) ).
thf(f22,plain,
( ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f159,plain,
( ! [X1: $i] :
( ( $false
= ( irel @ sK5 @ X1 ) )
| ( ( sK3 @ X1 )
= $true ) )
| ~ spl1_2 ),
inference(avatar_component_clause,[status(thm)],[f158]) ).
thf(f158,definition,
( spl1_2
<=> ! [X1: $i] :
( ( ( sK3 @ X1 )
= $true )
| ( $false
= ( irel @ sK5 @ X1 ) ) ) ),
introduced(definition,[new_symbols(naming,[spl1_2])],[avatar_definition]) ).
thf(f178,plain,
( ( ( sK3 @ sK12 )
= $false )
| ~ spl1_6 ),
inference(avatar_component_clause,[status(thm)],[f176]) ).
thf(f176,definition,
( spl1_6
<=> ( ( sK3 @ sK12 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl1_6])],[avatar_definition]) ).
thf(f291,plain,
( ~ spl1_1
| ~ spl1_14 ),
inference(avatar_contradiction_clause,[status(thm)],[f290]) ).
thf(f290,plain,
( $false
| ~ spl1_1
| ~ spl1_14 ),
inference(trivial_inequality_removal,[status(thm)],[f287]) ).
thf(f287,plain,
( ( $true = $false )
| ~ spl1_1
| ~ spl1_14 ),
inference(superposition,[status(thm)],[f273,f216]) ).
thf(f216,plain,
( ( ( sK4 @ sK8 )
= $false )
| ~ spl1_14 ),
inference(avatar_component_clause,[status(thm)],[f214]) ).
thf(f214,definition,
( spl1_14
<=> ( ( sK4 @ sK8 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl1_14])],[avatar_definition]) ).
thf(f273,plain,
( ! [X0: $i] :
( ( sK4 @ X0 )
= $true )
| ~ spl1_1 ),
inference(superposition,[status(thm)],[f271,f49]) ).
thf(f271,plain,
( ( ( sK4 @ sK5 )
= $true )
| ~ spl1_1 ),
inference(trivial_inequality_removal,[status(thm)],[f269]) ).
thf(f269,plain,
( ( $true = $false )
| ( ( sK4 @ sK5 )
= $true )
| ~ spl1_1 ),
inference(superposition,[status(thm)],[f156,f67]) ).
thf(f156,plain,
( ! [X2: $i] :
( ( $false
= ( irel @ sK5 @ X2 ) )
| ( ( sK4 @ X2 )
= $true ) )
| ~ spl1_1 ),
inference(avatar_component_clause,[status(thm)],[f155]) ).
thf(f155,definition,
( spl1_1
<=> ! [X2: $i] :
( ( $false
= ( irel @ sK5 @ X2 ) )
| ( ( sK4 @ X2 )
= $true ) ) ),
introduced(definition,[new_symbols(naming,[spl1_1])],[avatar_definition]) ).
thf(f280,plain,
( ~ spl1_1
| ~ spl1_13 ),
inference(avatar_contradiction_clause,[status(thm)],[f279]) ).
thf(f279,plain,
( $false
| ~ spl1_1
| ~ spl1_13 ),
inference(trivial_inequality_removal,[status(thm)],[f276]) ).
thf(f276,plain,
( ( $true = $false )
| ~ spl1_1
| ~ spl1_13 ),
inference(superposition,[status(thm)],[f212,f273]) ).
thf(f212,plain,
( ( ( sK4 @ sK6 )
= $false )
| ~ spl1_13 ),
inference(avatar_component_clause,[status(thm)],[f210]) ).
thf(f210,definition,
( spl1_13
<=> ( ( sK4 @ sK6 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl1_13])],[avatar_definition]) ).
thf(f264,plain,
( ~ spl1_2
| ~ spl1_4 ),
inference(avatar_contradiction_clause,[status(thm)],[f263]) ).
thf(f263,plain,
( $false
| ~ spl1_2
| ~ spl1_4 ),
inference(trivial_inequality_removal,[status(thm)],[f259]) ).
thf(f259,plain,
( ( $true = $false )
| ~ spl1_2
| ~ spl1_4 ),
inference(superposition,[status(thm)],[f168,f247]) ).
thf(f247,plain,
( ! [X0: $i] :
( ( sK3 @ X0 )
= $true )
| ~ spl1_2 ),
inference(superposition,[status(thm)],[f245,f49]) ).
thf(f245,plain,
( ( ( sK3 @ sK5 )
= $true )
| ~ spl1_2 ),
inference(trivial_inequality_removal,[status(thm)],[f244]) ).
thf(f244,plain,
( ( ( sK3 @ sK5 )
= $true )
| ( $true = $false )
| ~ spl1_2 ),
inference(superposition,[status(thm)],[f67,f159]) ).
thf(f168,plain,
( ( ( sK3 @ sK9 )
= $false )
| ~ spl1_4 ),
inference(avatar_component_clause,[status(thm)],[f166]) ).
thf(f166,definition,
( spl1_4
<=> ( ( sK3 @ sK9 )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl1_4])],[avatar_definition]) ).
thf(f217,plain,
( spl1_13
| spl1_14 ),
inference(avatar_split_clause,[status(thm)],[f104,f214,f210]) ).
thf(f104,plain,
( ( ( sK4 @ sK6 )
= $false )
| ( ( sK4 @ sK8 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f97]) ).
thf(f97,plain,
( ( ( ~ ( irel @ sK5 @ sK8 )
| ( sK4 @ sK8 ) )
= $false )
| ( ( sK4 @ sK6 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f96]) ).
thf(f96,plain,
( ( ( ~ ( irel @ sK5 @ sK6 )
| ( sK4 @ sK6 ) )
= $false )
| ( ( ~ ( irel @ sK5 @ sK8 )
| ( sK4 @ sK8 ) )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f95]) ).
thf(f95,plain,
( ( ( ~ ( irel @ sK5 @ sK6 )
| ( sK4 @ sK6 ) )
= $false )
| ( $false
= ( ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) )
@ sK8 ) ) ),
inference(sigma_clausification,[status(thm)],[f82]) ).
thf(f82,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $false )
| ( ( ~ ( irel @ sK5 @ sK6 )
| ( sK4 @ sK6 ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f81]) ).
thf(f81,plain,
( ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false )
| ( ( ~ ( irel @ sK5 @ sK6 )
| ( sK4 @ sK6 ) )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f80]) ).
thf(f80,plain,
( ( ( ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) )
@ sK6 )
= $false )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false ) ),
inference(sigma_clausification,[status(thm)],[f79]) ).
thf(f79,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $false )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f77]) ).
thf(f77,plain,
( ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) ) )
= $false )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f75]) ).
thf(f75,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) ) )
!= ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f74]) ).
thf(f74,plain,
( ( ^ [Y0: $i] :
( ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK3 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK4 @ Y1 ) ) ) )
@ sK5 )
!= ( ^ [Y0: $i] :
( ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK4 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK3 @ Y1 ) ) ) )
@ sK5 ) ),
inference(negative_extensionality,[status(thm)],[f73]) ).
thf(f73,plain,
( ( ^ [Y0: $i] :
( ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK4 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK3 @ Y1 ) ) ) ) )
!= ( ^ [Y0: $i] :
( ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK3 @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ~ ( irel @ Y0 @ Y1 )
| ( sK4 @ Y1 ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f72]) ).
thf(f72,plain,
( ( ^ [Y0: $i > $o,Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( sK3 @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) )
@ sK4 )
!= ( ^ [Y0: $i > $o,Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( sK3 @ Y2 ) ) ) )
@ sK4 ) ),
inference(negative_extensionality,[status(thm)],[f71]) ).
thf(f71,plain,
( ( ^ [Y0: $i > $o,Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( sK3 @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) )
!= ( ^ [Y0: $i > $o,Y1: $i] :
( ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( sK3 @ Y2 ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f70]) ).
thf(f70,plain,
( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) ) )
@ sK3 )
!= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) )
@ sK3 ) ),
inference(negative_extensionality,[status(thm)],[f41]) ).
thf(f41,plain,
( ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) ) ) )
!= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f40]) ).
thf(f40,plain,
( ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y3 @ Y4 )
| ( Y2 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y3 @ Y4 )
| ( Y2 @ Y4 ) ) )
@ Y0 )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ~ ( irel @ Y3 @ Y4 )
| ( Y2 @ Y4 ) ) )
@ Y1 ) ) )
!= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) ),
inference(definition_unfolding,[status(thm)],[f16,f21,f19,f18,f18]) ).
thf(f18,plain,
( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ~ ( irel @ Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f19,plain,
( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f21,plain,
( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y0 @ Y3 ) ) )
| ( !! @ $i
@ ^ [Y3: $i] :
( ~ ( irel @ Y2 @ Y3 )
| ( Y1 @ Y3 ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f16,plain,
( ior
!= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mbox_s4 @ Y0 ) @ ( mbox_s4 @ Y1 ) ) ) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
thf(f11,plain,
( ior
!= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mbox_s4 @ Y0 ) @ ( mbox_s4 @ Y1 ) ) ) ),
inference(flattening,[status(thm)],[f8]) ).
thf(f8,plain,
( ior
!= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mbox_s4 @ Y0 ) @ ( mbox_s4 @ Y1 ) ) ) ),
inference(fool_elimination,[status(thm)],[f7]) ).
thf(f7,plain,
( ior
!= ( ^ [X0: $i > $o,X1: $i > $o] : ( mor @ ( mbox_s4 @ X0 ) @ ( mbox_s4 @ X1 ) ) ) ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,negated_conjecture,
( ior
!= ( ^ [X8: $i > $o,X9: $i > $o] : ( mor @ ( mbox_s4 @ X8 ) @ ( mbox_s4 @ X9 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
thf(f2,conjecture,
( ior
= ( ^ [X8: $i > $o,X9: $i > $o] : ( mor @ ( mbox_s4 @ X8 ) @ ( mbox_s4 @ X9 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.rHa6s2wqLE/DTF2THF_22212.p',ior) ).
thf(f179,plain,
( spl1_6
| spl1_4 ),
inference(avatar_split_clause,[status(thm)],[f131,f166,f176]) ).
thf(f131,plain,
( ( ( sK3 @ sK9 )
= $false )
| ( ( sK3 @ sK12 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f130]) ).
thf(f130,plain,
( ( ( ~ ( irel @ sK5 @ sK12 )
| ( sK3 @ sK12 ) )
= $false )
| ( ( sK3 @ sK9 )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f129]) ).
thf(f129,plain,
( ( ( sK3 @ sK9 )
= $false )
| ( ( ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) )
@ sK12 )
= $false ) ),
inference(sigma_clausification,[status(thm)],[f128]) ).
thf(f128,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $false )
| ( ( sK3 @ sK9 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f109]) ).
thf(f109,plain,
( ( ( sK3 @ sK9 )
= $false )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f108]) ).
thf(f108,plain,
( ( ( ~ ( irel @ sK5 @ sK9 )
| ( sK3 @ sK9 ) )
= $false )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f107]) ).
thf(f107,plain,
( ( ( ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) )
@ sK9 )
= $false )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false ) ),
inference(sigma_clausification,[status(thm)],[f78]) ).
thf(f78,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $false )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f77]) ).
thf(f160,plain,
( spl1_1
| spl1_2
| spl1_2 ),
inference(avatar_split_clause,[status(thm)],[f153,f158,f158,f155]) ).
thf(f153,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( irel @ sK5 @ X2 ) )
| ( ( sK3 @ X1 )
= $true )
| ( ( sK3 @ X3 )
= $true )
| ( ( irel @ sK5 @ X3 )
= $false )
| ( ( sK4 @ X2 )
= $true )
| ( $false
= ( irel @ sK5 @ X1 ) ) ),
inference(not_proxy_clausification,[status(thm)],[f152]) ).
thf(f152,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( sK3 @ X1 )
= $true )
| ( ( sK4 @ X2 )
= $true )
| ( $false
= ( irel @ sK5 @ X2 ) )
| ( ( sK3 @ X3 )
= $true )
| ( $true
= ( ~ ( irel @ sK5 @ X3 ) ) )
| ( $false
= ( irel @ sK5 @ X1 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f151]) ).
thf(f151,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( ( sK4 @ X2 )
= $true )
| ( ( sK3 @ X1 )
= $true )
| ( $false
= ( irel @ sK5 @ X2 ) )
| ( $true
= ( ~ ( irel @ sK5 @ X3 )
| ( sK3 @ X3 ) ) )
| ( $false
= ( irel @ sK5 @ X1 ) ) ),
inference(not_proxy_clausification,[status(thm)],[f150]) ).
thf(f150,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( irel @ sK5 @ X1 ) )
| ( ( sK4 @ X2 )
= $true )
| ( ( ~ ( irel @ sK5 @ X2 ) )
= $true )
| ( $true
= ( ~ ( irel @ sK5 @ X3 )
| ( sK3 @ X3 ) ) )
| ( ( sK3 @ X1 )
= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f149]) ).
thf(f149,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( irel @ sK5 @ X1 ) )
| ( ( sK4 @ X2 )
= $true )
| ( ( sK3 @ X1 )
= $true )
| ( ( ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) )
@ X3 )
= $true )
| ( ( ~ ( irel @ sK5 @ X2 ) )
= $true ) ),
inference(pi_clausification,[status(thm)],[f148]) ).
thf(f148,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( irel @ sK5 @ X1 ) )
| ( ( sK4 @ X2 )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $true )
| ( ( sK3 @ X1 )
= $true )
| ( ( ~ ( irel @ sK5 @ X2 ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f147]) ).
thf(f147,plain,
! [X2: $i,X1: $i] :
( ( ( ~ ( irel @ sK5 @ X2 )
| ( sK4 @ X2 ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $true )
| ( $false
= ( irel @ sK5 @ X1 ) )
| ( ( sK3 @ X1 )
= $true ) ),
inference(not_proxy_clausification,[status(thm)],[f146]) ).
thf(f146,plain,
! [X2: $i,X1: $i] :
( ( ( ~ ( irel @ sK5 @ X1 ) )
= $true )
| ( ( ~ ( irel @ sK5 @ X2 )
| ( sK4 @ X2 ) )
= $true )
| ( ( sK3 @ X1 )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f145]) ).
thf(f145,plain,
! [X2: $i,X1: $i] :
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $true )
| ( ( ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) )
@ X2 )
= $true )
| ( ( sK3 @ X1 )
= $true )
| ( ( ~ ( irel @ sK5 @ X1 ) )
= $true ) ),
inference(pi_clausification,[status(thm)],[f144]) ).
thf(f144,plain,
! [X1: $i] :
( ( ( sK3 @ X1 )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $true )
| ( ( ~ ( irel @ sK5 @ X1 ) )
= $true ) ),
inference(duplicate_literal_removal,[status(thm)],[f143]) ).
thf(f143,plain,
! [X1: $i] :
( ( ( ~ ( irel @ sK5 @ X1 ) )
= $true )
| ( ( sK3 @ X1 )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f142]) ).
thf(f142,plain,
! [X1: $i] :
( ( ( sK3 @ X1 )
= $true )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $true )
| ( ( ~ ( irel @ sK5 @ X1 ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f141]) ).
thf(f141,plain,
! [X1: $i] :
( ( ( ~ ( irel @ sK5 @ X1 )
| ( sK3 @ X1 ) )
= $true )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f140]) ).
thf(f140,plain,
! [X1: $i] :
( ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $true )
| ( ( ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) )
@ X1 )
= $true ) ),
inference(pi_clausification,[status(thm)],[f139]) ).
thf(f139,plain,
( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
= $true )
| ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
= $true )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f76]) ).
thf(f76,plain,
( ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) ) )
= $true )
| ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK3 @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ~ ( irel @ sK5 @ Y0 )
| ( sK4 @ Y0 ) ) ) )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f75]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.33 % Computer : n025.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 09:21:58 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.19/0.45 ---- Original DTF file ---
% 0.30/0.45 thf(spec,logic,$$dhol).
% 0.30/0.45 %------------------------------------------------------------------------------
% 0.30/0.45 % File : SWX153_1 : TPTP v9.3.0. Released v9.3.0.
% 0.30/0.45 % Domain : Software Verification
% 0.30/0.45 % Problem : Benchmark: LCL696^1, Active target: ior
% 0.30/0.45 % Version : Especial.
% 0.30/0.45 % English :
% 0.30/0.45
% 0.30/0.45 % Refs : [Kon26] Kondylidou (2026), Email to Geoff Sutcliffe
% 0.30/0.45 % Source : [Kon26]
% 0.30/0.45 % Names : ALG444^1__005__axclos.verify [Kon26]
% 0.30/0.45
% 0.30/0.45 % Status : Theorem
% 0.30/0.45 % Rating : ? v9.3.0
% 0.30/0.45 % Syntax : Number of formulae : 26 ( 1 unt; 24 typ; 0 def)
% 0.30/0.45 % Number of atoms : 69 ( 22 equ; 0 cnn)
% 0.30/0.45 % Maximal formula atoms : 24 ( 34 avg)
% 0.30/0.45 % Number of connectives : 188 ( 38 ~; 32 |; 26 &; 91 @)
% 0.30/0.45 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 0.30/0.45 % Maximal formula depth : 26 ( 14 avg)
% 0.30/0.45 % Number of types : 4 ( 2 usr)
% 0.30/0.45 % Number of type conns : 98 ( 98 >; 0 *; 0 +; 0 <<)
% 0.30/0.45 % Number of symbols : 23 ( 22 usr; 1 con; 0-3 aty)
% 0.30/0.45 % Number of variables : 73 ( 41 ^; 31 !; 1 ?; 73 :)
% 0.30/0.45 % SPC : TH0_THM_EQU_NAR
% 0.30/0.45
% 0.30/0.45 % Comments :
% 0.30/0.45 %------------------------------------------------------------------------------
% 0.30/0.45 thf(unsorted_type,type,
% 0.30/0.45 unsorted: $tType ).
% 0.30/0.45
% 0.30/0.45 thf(irel_decl,type,
% 0.30/0.45 irel: $i > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(mnot_decl,type,
% 0.30/0.45 mnot: ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(mor_decl,type,
% 0.30/0.45 mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(mand_decl,type,
% 0.30/0.45 mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(mimplies_decl,type,
% 0.30/0.45 mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(mbox_s4_decl,type,
% 0.30/0.45 mbox_s4: ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(iatom_decl,type,
% 0.30/0.45 iatom: ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(inot_decl,type,
% 0.30/0.45 inot: ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(itrue_decl,type,
% 0.30/0.45 itrue: $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(ifalse_decl,type,
% 0.30/0.45 ifalse: $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(iand_decl,type,
% 0.30/0.45 iand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(ior_decl,type,
% 0.30/0.45 ior: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(iimplies_decl,type,
% 0.30/0.45 iimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(iimplied_decl,type,
% 0.30/0.45 iimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(iequiv_decl,type,
% 0.30/0.45 iequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(ixor_decl,type,
% 0.30/0.45 ixor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 0.30/0.45
% 0.30/0.45 thf(ivalid_decl,type,
% 0.30/0.45 ivalid: ( $i > $o ) > $o ).
% 0.30/0.45
% 0.30/0.45 thf(isatisfiable_decl,type,
% 0.30/0.45 isatisfiable: ( $i > $o ) > $o ).
% 0.30/0.45
% 0.30/0.45 thf(icountersatisfiable_decl,type,
% 0.30/0.45 icountersatisfiable: ( $i > $o ) > $o ).
% 0.30/0.45
% 0.30/0.45 thf(iinvalid_decl,type,
% 0.30/0.45 iinvalid: ( $i > $o ) > $o ).
% 0.30/0.45
% 0.30/0.45 %----Types of the domains
% 0.30/0.45 thf(d_unsorted_type,type,
% 0.30/0.45 d_unsorted: $tType ).
% 0.30/0.45
% 0.30/0.45 %----Types of the promotion functions
% 0.30/0.45 thf(d2unsorted_decl,type,
% 0.30/0.45 d2unsorted: d_unsorted > $i ).
% 0.30/0.45
% 0.30/0.45 %----Types of the domain elements
% 0.30/0.45 thf(d_unsorted_0_decl,type,
% 0.30/0.45 d_unsorted_0: d_unsorted ).
% 0.30/0.45
% 0.30/0.45 thf(lcl696_1,axiom,
% 0.30/0.45 ( ! [U: $i] :
% 0.30/0.45 ? [DU: d_unsorted] :
% 0.30/0.45 ( U
% 0.30/0.45 = ( d2unsorted @ DU ) )
% 0.30/0.45 & ! [DU: d_unsorted] : ( DU = d_unsorted_0 )
% 0.30/0.45 & ! [DU1: d_unsorted,DU2: d_unsorted] :
% 0.30/0.45 ( ( ( d2unsorted @ DU1 )
% 0.30/0.45 = ( d2unsorted @ DU2 ) )
% 0.30/0.45 => ( DU1 = DU2 ) )
% 0.30/0.45 & ( mnot
% 0.30/0.45 = ( ^ [X: $i > $o,U: $i] :
% 0.30/0.45 ~ ( X @ U ) ) )
% 0.30/0.45 & ( mor
% 0.30/0.45 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 0.30/0.45 ( ( X @ U )
% 0.30/0.45 | ( Y @ U ) ) ) )
% 0.30/0.45 & ( mand
% 0.30/0.45 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 0.30/0.45 ( ( X @ U )
% 0.30/0.45 & ( Y @ U ) ) ) )
% 0.30/0.45 & ( mimplies
% 0.30/0.45 = ( ^ [U: $i > $o,V: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ( ~ ( U @ Flatten_var_0 )
% 0.30/0.45 | ( V @ Flatten_var_0 ) ) ) )
% 0.30/0.45 & ( mbox_s4
% 0.30/0.45 = ( ^ [P: $i > $o,X: $i] :
% 0.30/0.45 ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ X @ Y )
% 0.30/0.45 | ( P @ Y ) ) ) )
% 0.30/0.45 & ( iatom
% 0.30/0.45 = ( ^ [P: $i > $o,Flatten_var_0: $i] : ( P @ Flatten_var_0 ) ) )
% 0.30/0.45 & ( inot
% 0.30/0.45 = ( ^ [P: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ~ ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( P @ Y ) ) ) )
% 0.30/0.45 & ( iand
% 0.30/0.45 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ( ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( P @ Y ) )
% 0.30/0.45 & ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( Q @ Y ) ) ) ) )
% 0.30/0.45 & ( ior
% 0.30/0.45 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ( ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( P @ Y ) )
% 0.30/0.45 | ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( Q @ Y ) ) ) ) )
% 0.30/0.45 & ( iimplies
% 0.30/0.45 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ( ~ ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( P @ Y ) )
% 0.30/0.45 | ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( Q @ Y ) ) ) ) )
% 0.30/0.45 & ( iimplied
% 0.30/0.45 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ( ~ ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( Q @ Y ) )
% 0.30/0.45 | ! [Y: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( P @ Y ) ) ) ) )
% 0.30/0.45 & ( iequiv
% 0.30/0.45 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ( ! [Y: $i,Bound_variable_718: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ~ ! [Bound_variable_693: $i] :
% 0.30/0.45 ( ~ ( irel @ Y @ Bound_variable_693 )
% 0.30/0.45 | ( P @ Bound_variable_693 ) )
% 0.30/0.45 | ~ ( irel @ Y @ Bound_variable_718 )
% 0.30/0.45 | ( Q @ Bound_variable_718 ) )
% 0.30/0.45 & ! [Y: $i,Bound_variable_771: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ~ ! [Bound_variable_746: $i] :
% 0.30/0.45 ( ~ ( irel @ Y @ Bound_variable_746 )
% 0.30/0.45 | ( Q @ Bound_variable_746 ) )
% 0.30/0.45 | ~ ( irel @ Y @ Bound_variable_771 )
% 0.30/0.45 | ( P @ Bound_variable_771 ) ) ) ) )
% 0.30/0.45 & ( ixor
% 0.30/0.45 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 0.30/0.45 ~ ! [Y: $i,Bound_variable_849: $i,Bound_variable_851: $i,Bound_variable_864: $i,Bound_variable_866: $i] :
% 0.30/0.45 ( ~ ( irel @ Flatten_var_0 @ Y )
% 0.30/0.45 | ( ( ~ ( irel @ Y @ Bound_variable_849 )
% 0.30/0.45 | ~ ! [Bound_variable_693: $i] :
% 0.30/0.45 ( ~ ( irel @ Bound_variable_849 @ Bound_variable_693 )
% 0.30/0.45 | ( P @ Bound_variable_693 ) )
% 0.30/0.45 | ~ ( irel @ Bound_variable_849 @ Bound_variable_851 )
% 0.30/0.45 | ( Q @ Bound_variable_851 ) )
% 0.30/0.45 & ( ~ ( irel @ Y @ Bound_variable_864 )
% 0.30/0.45 | ~ ! [Bound_variable_746: $i] :
% 0.30/0.45 ( ~ ( irel @ Bound_variable_864 @ Bound_variable_746 )
% 0.30/0.45 | ( Q @ Bound_variable_746 ) )
% 0.30/0.45 | ~ ( irel @ Bound_variable_864 @ Bound_variable_866 )
% 0.30/0.45 | ( P @ Bound_variable_866 ) ) ) ) ) )
% 0.30/0.45 & ( ivalid
% 0.30/0.45 = ( ^ [Phi: $i > $o] :
% 0.30/0.45 ! [W: $i] : ( Phi @ W ) ) )
% 0.30/0.45 & ( isatisfiable
% 0.30/0.45 = ( ^ [Phi: $i > $o] :
% 0.30/0.45 ~ ! [W: $i] :
% 0.30/0.45 ~ ( Phi @ W ) ) )
% 0.30/0.45 & ( icountersatisfiable
% 0.30/0.45 = ( ^ [Phi: $i > $o] :
% 0.30/0.45 ~ ! [W: $i] : ( Phi @ W ) ) )
% 0.30/0.45 & ( iinvalid
% 0.30/0.45 = ( ^ [Phi: $i > $o] :
% 0.30/0.45 ! [W: $i] :
% 0.30/0.45 ~ ( Phi @ W ) ) )
% 0.30/0.45 & ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
% 0.30/0.45 & ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
% 0.30/0.45 & ~ ( ifalse @ ( d2unsorted @ d_unsorted_0 ) ) ) ).
% 0.30/0.45
% 0.30/0.45 thf(ior,conjecture,
% 0.30/0.45 ( ior
% 0.30/0.45 = ( ^ [P: $i > $o,Q: $i > $o] : ( mor @ ( mbox_s4 @ P ) @ ( mbox_s4 @ Q ) ) ) ) ).
% 0.30/0.45
% 0.30/0.45 %------------------------------------------------------------------------------
% 0.30/0.45 ------------------------
% 1.69/1.79 ---- Embedded in THF ---
% 1.69/1.79 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.69/1.79 %%% Generated on Tue May 05 09:21:59 EDT 2026
% 1.69/1.79 %%% using '$$dhol' embedding, version 1.3.0.
% 1.69/1.79 %%% Logic specification used:
% 1.69/1.79 %%% thf(spec, logic, $$dhol).
% 1.69/1.79
% 1.69/1.79 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.rHa6s2wqLE/DTF2DTF22212.p
% See solution above
% 1.69/1.79 ------------------------
% 1.91/1.80 ---- Cleaned THF ---
% 1.91/1.80 thf(unsorted_type,type,
% 1.91/1.80 unsorted: $tType ).
% 1.91/1.80
% 1.91/1.80 thf(irel_decl,type,
% 1.91/1.80 irel: $i > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(mnot_decl,type,
% 1.91/1.80 mnot: ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(mor_decl,type,
% 1.91/1.80 mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(mand_decl,type,
% 1.91/1.80 mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(mimplies_decl,type,
% 1.91/1.80 mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(mbox_s4_decl,type,
% 1.91/1.80 mbox_s4: ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(iatom_decl,type,
% 1.91/1.80 iatom: ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(inot_decl,type,
% 1.91/1.80 inot: ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(itrue_decl,type,
% 1.91/1.80 itrue: $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(ifalse_decl,type,
% 1.91/1.80 ifalse: $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(iand_decl,type,
% 1.91/1.80 iand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(ior_decl,type,
% 1.91/1.80 ior: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(iimplies_decl,type,
% 1.91/1.80 iimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(iimplied_decl,type,
% 1.91/1.80 iimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(iequiv_decl,type,
% 1.91/1.80 iequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(ixor_decl,type,
% 1.91/1.80 ixor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
% 1.91/1.80
% 1.91/1.80 thf(ivalid_decl,type,
% 1.91/1.80 ivalid: ( $i > $o ) > $o ).
% 1.91/1.80
% 1.91/1.80 thf(isatisfiable_decl,type,
% 1.91/1.80 isatisfiable: ( $i > $o ) > $o ).
% 1.91/1.80
% 1.91/1.80 thf(icountersatisfiable_decl,type,
% 1.91/1.80 icountersatisfiable: ( $i > $o ) > $o ).
% 1.91/1.80
% 1.91/1.80 thf(iinvalid_decl,type,
% 1.91/1.80 iinvalid: ( $i > $o ) > $o ).
% 1.91/1.80
% 1.91/1.80 thf(d_unsorted_type,type,
% 1.91/1.80 d_unsorted: $tType ).
% 1.91/1.80
% 1.91/1.80 thf(d2unsorted_decl,type,
% 1.91/1.80 d2unsorted: d_unsorted > $i ).
% 1.91/1.80
% 1.91/1.80 thf(d_unsorted_0_decl,type,
% 1.91/1.80 d_unsorted_0: d_unsorted ).
% 1.91/1.80
% 1.91/1.80 thf(lcl696_1,axiom,
% 1.91/1.80 ( ! [U: $i] :
% 1.91/1.80 ? [DU: d_unsorted] :
% 1.91/1.80 ( U
% 1.91/1.80 = ( d2unsorted @ DU ) )
% 1.91/1.80 & ! [DU: d_unsorted] : ( DU = d_unsorted_0 )
% 1.91/1.80 & ! [DU1: d_unsorted,DU2: d_unsorted] :
% 1.91/1.80 ( ( ( d2unsorted @ DU1 )
% 1.91/1.80 = ( d2unsorted @ DU2 ) )
% 1.91/1.80 => ( DU1 = DU2 ) )
% 1.91/1.80 & ( mnot
% 1.91/1.80 = ( ^ [X: $i > $o,U: $i] :
% 1.91/1.80 ~ ( X @ U ) ) )
% 1.91/1.80 & ( mor
% 1.91/1.80 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 1.91/1.80 ( ( X @ U )
% 1.91/1.80 | ( Y @ U ) ) ) )
% 1.91/1.80 & ( mand
% 1.91/1.80 = ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
% 1.91/1.80 ( ( X @ U )
% 1.91/1.80 & ( Y @ U ) ) ) )
% 1.91/1.80 & ( mimplies
% 1.91/1.80 = ( ^ [U: $i > $o,V: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ( ~ ( U @ Flatten_var_0 )
% 1.91/1.80 | ( V @ Flatten_var_0 ) ) ) )
% 1.91/1.80 & ( mbox_s4
% 1.91/1.80 = ( ^ [P: $i > $o,X: $i] :
% 1.91/1.80 ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ X @ Y )
% 1.91/1.80 | ( P @ Y ) ) ) )
% 1.91/1.80 & ( iatom
% 1.91/1.80 = ( ^ [P: $i > $o,Flatten_var_0: $i] : ( P @ Flatten_var_0 ) ) )
% 1.91/1.80 & ( inot
% 1.91/1.80 = ( ^ [P: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ~ ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( P @ Y ) ) ) )
% 1.91/1.80 & ( iand
% 1.91/1.80 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ( ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( P @ Y ) )
% 1.91/1.80 & ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( Q @ Y ) ) ) ) )
% 1.91/1.80 & ( ior
% 1.91/1.80 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ( ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( P @ Y ) )
% 1.91/1.80 | ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( Q @ Y ) ) ) ) )
% 1.91/1.80 & ( iimplies
% 1.91/1.80 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ( ~ ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( P @ Y ) )
% 1.91/1.80 | ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( Q @ Y ) ) ) ) )
% 1.91/1.80 & ( iimplied
% 1.91/1.80 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ( ~ ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( Q @ Y ) )
% 1.91/1.80 | ! [Y: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( P @ Y ) ) ) ) )
% 1.91/1.80 & ( iequiv
% 1.91/1.80 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ( ! [Y: $i,Bound_variable_718: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ~ ! [Bound_variable_693: $i] :
% 1.91/1.80 ( ~ ( irel @ Y @ Bound_variable_693 )
% 1.91/1.80 | ( P @ Bound_variable_693 ) )
% 1.91/1.80 | ~ ( irel @ Y @ Bound_variable_718 )
% 1.91/1.80 | ( Q @ Bound_variable_718 ) )
% 1.91/1.80 & ! [Y: $i,Bound_variable_771: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ~ ! [Bound_variable_746: $i] :
% 1.91/1.80 ( ~ ( irel @ Y @ Bound_variable_746 )
% 1.91/1.80 | ( Q @ Bound_variable_746 ) )
% 1.91/1.80 | ~ ( irel @ Y @ Bound_variable_771 )
% 1.91/1.80 | ( P @ Bound_variable_771 ) ) ) ) )
% 1.91/1.80 & ( ixor
% 1.91/1.80 = ( ^ [P: $i > $o,Q: $i > $o,Flatten_var_0: $i] :
% 1.91/1.80 ~ ! [Y: $i,Bound_variable_849: $i,Bound_variable_851: $i,Bound_variable_864: $i,Bound_variable_866: $i] :
% 1.91/1.80 ( ~ ( irel @ Flatten_var_0 @ Y )
% 1.91/1.80 | ( ( ~ ( irel @ Y @ Bound_variable_849 )
% 1.91/1.80 | ~ ! [Bound_variable_693: $i] :
% 1.91/1.80 ( ~ ( irel @ Bound_variable_849 @ Bound_variable_693 )
% 1.91/1.80 | ( P @ Bound_variable_693 ) )
% 1.91/1.80 | ~ ( irel @ Bound_variable_849 @ Bound_variable_851 )
% 1.91/1.80 | ( Q @ Bound_variable_851 ) )
% 1.91/1.80 & ( ~ ( irel @ Y @ Bound_variable_864 )
% 1.91/1.80 | ~ ! [Bound_variable_746: $i] :
% 1.91/1.80 ( ~ ( irel @ Bound_variable_864 @ Bound_variable_746 )
% 1.91/1.80 | ( Q @ Bound_variable_746 ) )
% 1.91/1.80 | ~ ( irel @ Bound_variable_864 @ Bound_variable_866 )
% 1.91/1.80 | ( P @ Bound_variable_866 ) ) ) ) ) )
% 1.91/1.80 & ( ivalid
% 1.91/1.80 = ( ^ [Phi: $i > $o] :
% 1.91/1.80 ! [W: $i] : ( Phi @ W ) ) )
% 1.91/1.80 & ( isatisfiable
% 1.91/1.80 = ( ^ [Phi: $i > $o] :
% 1.91/1.80 ~ ! [W: $i] :
% 1.91/1.80 ~ ( Phi @ W ) ) )
% 1.91/1.80 & ( icountersatisfiable
% 1.91/1.80 = ( ^ [Phi: $i > $o] :
% 1.91/1.80 ~ ! [W: $i] : ( Phi @ W ) ) )
% 1.91/1.80 & ( iinvalid
% 1.91/1.80 = ( ^ [Phi: $i > $o] :
% 1.91/1.80 ! [W: $i] :
% 1.91/1.80 ~ ( Phi @ W ) ) )
% 1.91/1.80 & ( irel @ ( d2unsorted @ d_unsorted_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
% 1.91/1.80 & ( itrue @ ( d2unsorted @ d_unsorted_0 ) )
% 1.91/1.80 & ~ ( ifalse @ ( d2unsorted @ d_unsorted_0 ) ) ) ).
% 1.91/1.80
% 1.91/1.80 thf(ior,conjecture,
% 1.91/1.80 ( ior
% 1.91/1.80 = ( ^ [P: $i > $o,Q: $i > $o] : ( mor @ ( mbox_s4 @ P ) @ ( mbox_s4 @ Q ) ) ) ) ).
% 1.91/1.80 ------------------------
% 1.91/1.82 % (22356)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_22212 for (2999ds/275Mi)
% 1.91/1.82 % (22352)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_22212 for (2999ds/4Mi)
% 1.91/1.82 % (22353)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_22212 for (2999ds/27Mi)
% 1.91/1.82 % (22354)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_22212 for (2999ds/2Mi)
% 1.91/1.82 % (22355)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_22212 for (2999ds/2Mi)
% 1.91/1.82 % (22357)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_22212 for (2999ds/18Mi)
% 1.91/1.82 % (22352)Instruction limit reached!
% 1.91/1.82 % (22352)------------------------------
% 1.91/1.82 % (22352)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.82 % (22351)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_22212 for (2999ds/183Mi)
% 1.91/1.82 % (22352)Termination reason: Unknown
% 1.91/1.82 % (22352)Termination phase: Property scanning
% 1.91/1.82
% 1.91/1.82 % (22352)Memory used [KB]: 1023
% 1.91/1.82 % (22352)Time elapsed: 0.004 s
% 1.91/1.82 % (22352)Instructions burned: 5 (million)
% 1.91/1.82 % (22352)------------------------------
% 1.91/1.82 % (22352)------------------------------
% 1.91/1.82 % (22354)Instruction limit reached!
% 1.91/1.82 % (22354)------------------------------
% 1.91/1.82 % (22354)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.82 % (22354)Termination reason: Unknown
% 1.91/1.82 % (22354)Termination phase: shuffling
% 1.91/1.82
% 1.91/1.82 % (22355)Instruction limit reached!
% 1.91/1.82 % (22355)------------------------------
% 1.91/1.82 % (22355)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.82 % (22355)Termination reason: Unknown
% 1.91/1.82 % (22355)Termination phase: shuffling
% 1.91/1.82
% 1.91/1.82 % (22355)Memory used [KB]: 1023
% 1.91/1.82 % (22355)Time elapsed: 0.003 s
% 1.91/1.82 % (22355)Instructions burned: 2 (million)
% 1.91/1.82 % (22355)------------------------------
% 1.91/1.82 % (22355)------------------------------
% 1.91/1.82 % (22354)Memory used [KB]: 1023
% 1.91/1.82 % (22354)Time elapsed: 0.003 s
% 1.91/1.82 % (22354)Instructions burned: 2 (million)
% 1.91/1.82 % (22354)------------------------------
% 1.91/1.82 % (22354)------------------------------
% 1.91/1.82 % (22356)Refutation not found, incomplete strategy
% 1.91/1.82 % (22356)------------------------------
% 1.91/1.82 % (22356)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.82 % (22356)Termination reason: Refutation not found, incomplete strategy
% 1.91/1.82
% 1.91/1.82
% 1.91/1.82 % (22356)Memory used [KB]: 5628
% 1.91/1.82 % (22356)Time elapsed: 0.005 s
% 1.91/1.82 % (22356)Instructions burned: 7 (million)
% 1.91/1.82 % (22356)------------------------------
% 1.91/1.82 % (22356)------------------------------
% 1.91/1.83 % (22357)Instruction limit reached!
% 1.91/1.83 % (22357)------------------------------
% 1.91/1.83 % (22357)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.83 % (22357)Termination reason: Unknown
% 1.91/1.83 % (22357)Termination phase: Saturation
% 1.91/1.83
% 1.91/1.83 % (22357)Memory used [KB]: 5628
% 1.91/1.83 % (22357)Time elapsed: 0.012 s
% 1.91/1.83 % (22357)Instructions burned: 18 (million)
% 1.91/1.83 % (22357)------------------------------
% 1.91/1.83 % (22357)------------------------------
% 1.91/1.84 % (22353)First to succeed.
% 1.91/1.84 % (22359)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_22212 for (2999ds/37Mi)
% 1.91/1.84 % (22358)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_22212 for (2999ds/3Mi)
% 1.91/1.84 % (22360)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_22212 for (2999ds/15Mi)
% 1.91/1.84 % (22361)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_22212 for (2999ds/3Mi)
% 1.91/1.84 % (22361)Instruction limit reached!
% 1.91/1.84 % (22361)------------------------------
% 1.91/1.84 % (22361)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.84 % (22361)Termination reason: Unknown
% 1.91/1.84 % (22361)Termination phase: Property scanning
% 1.91/1.84
% 1.91/1.84 % (22361)Memory used [KB]: 1023
% 1.91/1.84 % (22361)Time elapsed: 0.003 s
% 1.91/1.84 % (22361)Instructions burned: 4 (million)
% 1.91/1.84 % (22361)------------------------------
% 1.91/1.84 % (22361)------------------------------
% 1.91/1.84 % (22358)Instruction limit reached!
% 1.91/1.84 % (22358)------------------------------
% 1.91/1.84 % (22358)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.84 % (22358)Termination reason: Unknown
% 1.91/1.84 % (22358)Termination phase: Property scanning
% 1.91/1.84
% 1.91/1.84 % (22358)Memory used [KB]: 1023
% 1.91/1.84 % (22358)Time elapsed: 0.004 s
% 1.91/1.84 % (22358)Instructions burned: 4 (million)
% 1.91/1.84 % (22358)------------------------------
% 1.91/1.84 % (22358)------------------------------
% 1.91/1.84 % (22351)Also succeeded, but the first one will report.
% 1.91/1.84 % (22353)Refutation found. Thanks to Tanya!
% 1.91/1.84 % SZS status Theorem for DTF2THF_22212
% 1.91/1.84 % SZS output start Proof for DTF2THF_22212
% 1.91/1.84 thf(type_def_6, type, d_unsorted: $tType).
% 1.91/1.84 thf(func_def_0, type, unsorted: $tType).
% 1.91/1.84 thf(func_def_1, type, irel: $i > $i > $o).
% 1.91/1.84 thf(func_def_2, type, mnot: ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_3, type, mor: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_4, type, mand: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_5, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_6, type, mbox_s4: ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_7, type, iatom: ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_8, type, inot: ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_9, type, itrue: $i > $o).
% 1.91/1.84 thf(func_def_10, type, ifalse: $i > $o).
% 1.91/1.84 thf(func_def_11, type, iand: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_12, type, ior: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_13, type, iimplies: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_14, type, iimplied: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_15, type, iequiv: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_16, type, ixor: ($i > $o) > ($i > $o) > $i > $o).
% 1.91/1.84 thf(func_def_17, type, ivalid: ($i > $o) > $o).
% 1.91/1.84 thf(func_def_18, type, isatisfiable: ($i > $o) > $o).
% 1.91/1.84 thf(func_def_19, type, icountersatisfiable: ($i > $o) > $o).
% 1.91/1.84 thf(func_def_20, type, iinvalid: ($i > $o) > $o).
% 1.91/1.84 thf(func_def_21, type, d_unsorted: $tType).
% 1.91/1.84 thf(func_def_22, type, d2unsorted: d_unsorted > $i).
% 1.91/1.84 thf(func_def_23, type, d_unsorted_0: d_unsorted).
% 1.91/1.84 thf(func_def_25, type, vEPSILON: !>[X0: $tType]:((X0 > $o) > X0)).
% 1.91/1.84 thf(func_def_42, type, sK0: $i > d_unsorted).
% 1.91/1.84 thf(func_def_44, type, ph2: !>[X0: $tType]:(X0)).
% 1.91/1.84 thf(func_def_45, type, sK3: $i > $o).
% 1.91/1.84 thf(func_def_46, type, sK4: $i > $o).
% 1.91/1.84 thf(f321,plain,(
% 1.91/1.84 $false),
% 1.91/1.84 inference(avatar_sat_refutation,[status(thm)],[f160,f179,f217,f264,f280,f291,f320])).
% 1.91/1.84 thf(f320,plain,(
% 1.91/1.84 ~spl1_2 | ~spl1_6),
% 1.91/1.84 inference(avatar_contradiction_clause,[status(thm)],[f319])).
% 1.91/1.84 thf(f319,plain,(
% 1.91/1.84 $false | (~spl1_2 | ~spl1_6)),
% 1.91/1.84 inference(trivial_inequality_removal,[status(thm)],[f315])).
% 1.91/1.84 thf(f315,plain,(
% 1.91/1.84 ($true = $false) | (~spl1_2 | ~spl1_6)),
% 1.91/1.84 inference(superposition,[status(thm)],[f178,f298])).
% 1.91/1.84 thf(f298,plain,(
% 1.91/1.84 ( ! [X0 : $i] : (((sK3 @ X0) = $true)) ) | ~spl1_2),
% 1.91/1.84 inference(superposition,[status(thm)],[f296,f49])).
% 1.91/1.84 thf(f49,plain,(
% 1.91/1.84 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) )),
% 1.91/1.84 inference(superposition,[status(thm)],[f45,f45])).
% 1.91/1.84 thf(f45,plain,(
% 1.91/1.84 ( ! [X3 : $i] : (((d2unsorted @ d_unsorted_0) = X3)) )),
% 1.91/1.84 inference(forward_demodulation,[status(thm)],[f24,f27])).
% 1.91/1.84 thf(f27,plain,(
% 1.91/1.84 ( ! [X2 : d_unsorted] : ((d_unsorted_0 = X2)) )),
% 1.91/1.84 inference(cnf_transformation,[status(thm)],[f15])).
% 1.91/1.84 thf(f15,plain,(
% 1.91/1.84 (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (irel @ Y6 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y0 @ Y8)))))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y7))) & ((((~ (irel @ Y6 @ Y3)) | (~ (irel @ Y3 @ Y5))) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y3 @ Y8)) | (Y1 @ Y8))))))) | (~ (irel @ Y2 @ Y6)))))))))))))))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & ((ifalse @ (d2unsorted @ d_unsorted_0)) != $true) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ((itrue @ (d2unsorted @ d_unsorted_0)) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & ! [X0 : d_unsorted,X1 : d_unsorted] : ((X0 = X1) | ((d2unsorted @ X1) != (d2unsorted @ X0))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y1 @ Y5)))))) | (Y0 @ Y4)) | (~ (irel @ Y3 @ Y4)))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & ! [X2 : d_unsorted] : (d_unsorted_0 = X2) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X3 : $i] : ((d2unsorted @ (sK0 @ X3)) = X3) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) = $true) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 1.91/1.84 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0])],[f13,f14])).
% 1.91/1.84 thf(f14,plain,(
% 1.91/1.84 ! [X3 : $i] : (? [X4 : d_unsorted] : ((d2unsorted @ X4) = X3) => ((d2unsorted @ (sK0 @ X3)) = X3))),
% 1.91/1.84 introduced(definition,[],[choice_axiom])).
% 1.91/1.84 thf(f13,plain,(
% 1.91/1.84 (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (irel @ Y6 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y0 @ Y8)))))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y7))) & ((((~ (irel @ Y6 @ Y3)) | (~ (irel @ Y3 @ Y5))) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y3 @ Y8)) | (Y1 @ Y8))))))) | (~ (irel @ Y2 @ Y6)))))))))))))))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & ((ifalse @ (d2unsorted @ d_unsorted_0)) != $true) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ((itrue @ (d2unsorted @ d_unsorted_0)) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & ! [X0 : d_unsorted,X1 : d_unsorted] : ((X0 = X1) | ((d2unsorted @ X1) != (d2unsorted @ X0))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y1 @ Y5)))))) | (Y0 @ Y4)) | (~ (irel @ Y3 @ Y4)))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & ! [X2 : d_unsorted] : (d_unsorted_0 = X2) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X3 : $i] : ? [X4 : d_unsorted] : ((d2unsorted @ X4) = X3) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) = $true) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 1.91/1.84 inference(rectify,[status(thm)],[f12])).
% 1.91/1.84 thf(f12,plain,(
% 1.91/1.84 (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (irel @ Y6 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y0 @ Y8)))))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y7))) & ((((~ (irel @ Y6 @ Y3)) | (~ (irel @ Y3 @ Y5))) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y3 @ Y8)) | (Y1 @ Y8))))))) | (~ (irel @ Y2 @ Y6)))))))))))))))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & ((ifalse @ (d2unsorted @ d_unsorted_0)) != $true) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ((itrue @ (d2unsorted @ d_unsorted_0)) = $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & ! [X2 : d_unsorted,X3 : d_unsorted] : ((X2 = X3) | ((d2unsorted @ X2) != (d2unsorted @ X3))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y1 @ Y5)))))) | (Y0 @ Y4)) | (~ (irel @ Y3 @ Y4)))))))))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : ((d2unsorted @ X1) = X0) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & ((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) = $true) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 1.91/1.84 inference(ennf_transformation,[status(thm)],[f10])).
% 1.91/1.84 thf(f10,plain,(
% 1.91/1.84 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & ((ifalse @ (d2unsorted @ d_unsorted_0)) != $true) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y1 @ Y5)))))) | (Y0 @ Y4)) | (~ (irel @ Y3 @ Y4)))))))))))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : ((d2unsorted @ X1) = X0) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & ((itrue @ (d2unsorted @ d_unsorted_0)) = $true) & ((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) = $true) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (irel @ Y6 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y0 @ Y8)))))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y7))) & ((((~ (irel @ Y6 @ Y3)) | (~ (irel @ Y3 @ Y5))) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y3 @ Y8)) | (Y1 @ Y8))))))) | (~ (irel @ Y2 @ Y6)))))))))))))))))))) & ! [X2 : d_unsorted,X3 : d_unsorted] : (((d2unsorted @ X2) = (d2unsorted @ X3)) => (X2 = X3)) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 1.91/1.84 inference(flattening,[status(thm)],[f9])).
% 1.91/1.84 thf(f9,plain,(
% 1.91/1.84 (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y1 @ Y5)))))) | (Y0 @ Y4)) | (~ (irel @ Y3 @ Y4)))))))))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & ! [X0 : $i] : ? [X1 : d_unsorted] : ((d2unsorted @ X1) = X0) & ! [X2 : d_unsorted,X3 : d_unsorted] : (((d2unsorted @ X2) = (d2unsorted @ X3)) => (X2 = X3)) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (irel @ Y6 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y0 @ Y8)))))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y7))) & ((((~ (irel @ Y6 @ Y3)) | (~ (irel @ Y3 @ Y5))) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y3 @ Y8)) | (Y1 @ Y8))))))) | (~ (irel @ Y2 @ Y6)))))))))))))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & ! [X4 : d_unsorted] : (d_unsorted_0 = X4) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ((itrue @ (d2unsorted @ d_unsorted_0)) = $true) & ~((ifalse @ (d2unsorted @ d_unsorted_0)) = $true) & ((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) = $true)),
% 1.91/1.84 inference(rectify,[status(thm)],[f6])).
% 1.91/1.84 thf(f6,plain,(
% 1.91/1.84 (iatom = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (Y0 @ Y1))))) & (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y4 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y4 @ Y5)) | (Y0 @ Y5)))))) | (~ (irel @ Y2 @ Y4))) | (Y1 @ Y3)))))) & (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((((~ (irel @ Y2 @ Y3)) | (~ (!! @ $i @ (^[Y5 : $i]: ((~ (irel @ Y3 @ Y5)) | (Y1 @ Y5)))))) | (Y0 @ Y4)) | (~ (irel @ Y3 @ Y4)))))))))))))) & (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) & (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (~ (Y0 @ Y2))))))))) & (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (isatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1))))))) & ! [X24 : $i] : ? [X25 : d_unsorted] : ((d2unsorted @ X25) = X24) & ! [X26 : d_unsorted,X27 : d_unsorted] : (((d2unsorted @ X26) = (d2unsorted @ X27)) => (X26 = X27)) & (icountersatisfiable = (^[Y0 : $i > $o]: (~ (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))) & (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2)))))))) & (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) & (ixor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: (~ (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ $i @ (^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: (!! @ $i @ (^[Y7 : $i]: ((((((~ (irel @ Y6 @ Y4)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y4 @ Y8)) | (Y0 @ Y8)))))) | (Y1 @ Y7)) | (~ (irel @ Y4 @ Y7))) & ((((~ (irel @ Y6 @ Y3)) | (~ (irel @ Y3 @ Y5))) | (Y0 @ Y5)) | (~ (!! @ $i @ (^[Y8 : $i]: ((~ (irel @ Y3 @ Y8)) | (Y1 @ Y8))))))) | (~ (irel @ Y2 @ Y6)))))))))))))))))))) & (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) & (Y0 @ Y2)))))))) & (inot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) | (~ (irel @ Y1 @ Y2)))))))))) & ! [X51 : d_unsorted] : (d_unsorted_0 = X51) & (iimplied = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((Y0 @ Y3) | (~ (irel @ Y2 @ Y3))))) | (~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))) & (iinvalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (~ (Y0 @ Y1)))))) & (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((~ (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3))))))))))) & (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) | (~ (irel @ Y2 @ Y3)))))))))))) & (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1)))))) & ((itrue @ (d2unsorted @ d_unsorted_0)) = $true) & ~((ifalse @ (d2unsorted @ d_unsorted_0)) = $true) & ((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) = $true)),
% 1.91/1.84 inference(fool_elimination,[status(thm)],[f5])).
% 1.91/1.84 thf(f5,plain,(
% 1.91/1.84 ((^[X0 : $i > $o, X1 : $i] : (X0 @ X1)) = iatom) & (iequiv = (^[X2 : $i > $o, X3 : $i > $o, X4 : $i] : (! [X5 : $i,X6 : $i] : (~(irel @ X6 @ X5) | (X2 @ X5) | ~! [X7 : $i] : ((X3 @ X7) | ~(irel @ X6 @ X7)) | ~(irel @ X4 @ X6)) & ! [X8 : $i,X9 : $i] : ((X3 @ X9) | ~(irel @ X4 @ X8) | ~! [X10 : $i] : ((X2 @ X10) | ~(irel @ X8 @ X10)) | ~(irel @ X8 @ X9))))) & (mbox_s4 = (^[X11 : $i > $o, X12 : $i] : (! [X13 : $i] : ((X11 @ X13) | ~(irel @ X12 @ X13))))) & ((^[X14 : $i > $o, X15 : $i > $o, X16 : $i] : (~(X14 @ X16) | (X15 @ X16))) = mimplies) & ((^[X17 : $i > $o, X18 : $i > $o, X19 : $i] : (! [X20 : $i] : ((X18 @ X20) | ~(irel @ X19 @ X20)) | ! [X21 : $i] : ((X17 @ X21) | ~(irel @ X19 @ X21)))) = ior) & ((^[X22 : $i > $o] : (~! [X23 : $i] : ~(X22 @ X23))) = isatisfiable) & ! [X24 : $i] : ? [X25 : d_unsorted] : ((d2unsorted @ X25) = X24) & ! [X26 : d_unsorted,X27 : d_unsorted] : (((d2unsorted @ X26) = (d2unsorted @ X27)) => (X26 = X27)) & (icountersatisfiable = (^[X28 : $i > $o] : (~! [X29 : $i] : (X28 @ X29)))) & ((^[X30 : $i > $o, X31 : $i > $o, X32 : $i] : ((X30 @ X32) | (X31 @ X32))) = mor) & (ivalid = (^[X33 : $i > $o] : (! [X34 : $i] : (X33 @ X34)))) & ((^[X35 : $i > $o, X36 : $i > $o, X37 : $i] : (~! [X38 : $i,X39 : $i,X40 : $i,X41 : $i,X42 : $i] : (~(irel @ X37 @ X39) | ((~! [X43 : $i] : ((X36 @ X43) | ~(irel @ X42 @ X43)) | (X35 @ X40) | ~(irel @ X42 @ X40) | ~(irel @ X39 @ X42)) & (~(irel @ X41 @ X38) | (X36 @ X38) | ~! [X44 : $i] : ((X35 @ X44) | ~(irel @ X41 @ X44)) | ~(irel @ X39 @ X41)))))) = ixor) & (mand = (^[X45 : $i > $o, X46 : $i > $o, X47 : $i] : ((X45 @ X47) & (X46 @ X47)))) & ((^[X48 : $i > $o, X49 : $i] : (~! [X50 : $i] : (~(irel @ X49 @ X50) | (X48 @ X50)))) = inot) & ! [X51 : d_unsorted] : (d_unsorted_0 = X51) & (iimplied = (^[X52 : $i > $o, X53 : $i > $o, X54 : $i] : (~! [X55 : $i] : ((X53 @ X55) | ~(irel @ X54 @ X55)) | ! [X56 : $i] : (~(irel @ X54 @ X56) | (X52 @ X56))))) & ((^[X57 : $i > $o] : (! [X58 : $i] : ~(X57 @ X58))) = iinvalid) & ((^[X59 : $i > $o, X60 : $i > $o, X61 : $i] : (! [X62 : $i] : ((X60 @ X62) | ~(irel @ X61 @ X62)) | ~! [X63 : $i] : ((X59 @ X63) | ~(irel @ X61 @ X63)))) = iimplies) & (iand = (^[X64 : $i > $o, X65 : $i > $o, X66 : $i] : (! [X67 : $i] : (~(irel @ X66 @ X67) | (X65 @ X67)) & ! [X68 : $i] : ((X64 @ X68) | ~(irel @ X66 @ X68))))) & ((^[X69 : $i > $o, X70 : $i] : (~(X69 @ X70))) = mnot) & (itrue @ (d2unsorted @ d_unsorted_0)) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))),
% 1.91/1.84 inference(rectify,[status(thm)],[f1])).
% 1.91/1.84 thf(f1,axiom,(
% 1.91/1.84 ((^[X8 : $i > $o, X7 : $i] : (X8 @ X7)) = iatom) & (iequiv = (^[X8 : $i > $o, X9 : $i > $o, X7 : $i] : (! [X12 : $i,X5 : $i] : (~(irel @ X5 @ X12) | (X8 @ X12) | ~! [X13 : $i] : ((X9 @ X13) | ~(irel @ X5 @ X13)) | ~(irel @ X7 @ X5)) & ! [X5 : $i,X10 : $i] : ((X9 @ X10) | ~(irel @ X7 @ X5) | ~! [X11 : $i] : ((X8 @ X11) | ~(irel @ X5 @ X11)) | ~(irel @ X5 @ X10))))) & (mbox_s4 = (^[X8 : $i > $o, X4 : $i] : (! [X5 : $i] : ((X8 @ X5) | ~(irel @ X4 @ X5))))) & ((^[X0 : $i > $o, X6 : $i > $o, X7 : $i] : (~(X0 @ X7) | (X6 @ X7))) = mimplies) & ((^[X8 : $i > $o, X9 : $i > $o, X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)))) = ior) & ((^[X18 : $i > $o] : (~! [X19 : $i] : ~(X18 @ X19))) = isatisfiable) & ! [X0 : $i] : ? [X1 : d_unsorted] : ((d2unsorted @ X1) = X0) & ! [X2 : d_unsorted,X3 : d_unsorted] : (((d2unsorted @ X2) = (d2unsorted @ X3)) => (X2 = X3)) & (icountersatisfiable = (^[X18 : $i > $o] : (~! [X19 : $i] : (X18 @ X19)))) & ((^[X4 : $i > $o, X5 : $i > $o, X0 : $i] : ((X4 @ X0) | (X5 @ X0))) = mor) & (ivalid = (^[X18 : $i > $o] : (! [X19 : $i] : (X18 @ X19)))) & ((^[X8 : $i > $o, X9 : $i > $o, X7 : $i] : (~! [X15 : $i,X5 : $i,X17 : $i,X14 : $i,X16 : $i] : (~(irel @ X7 @ X5) | ((~! [X13 : $i] : ((X9 @ X13) | ~(irel @ X16 @ X13)) | (X8 @ X17) | ~(irel @ X16 @ X17) | ~(irel @ X5 @ X16)) & (~(irel @ X14 @ X15) | (X9 @ X15) | ~! [X11 : $i] : ((X8 @ X11) | ~(irel @ X14 @ X11)) | ~(irel @ X5 @ X14)))))) = ixor) & (mand = (^[X4 : $i > $o, X5 : $i > $o, X0 : $i] : ((X4 @ X0) & (X5 @ X0)))) & ((^[X8 : $i > $o, X7 : $i] : (~! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5)))) = inot) & ! [X1 : d_unsorted] : (d_unsorted_0 = X1) & (iimplied = (^[X8 : $i > $o, X9 : $i > $o, X7 : $i] : (~! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ! [X5 : $i] : (~(irel @ X7 @ X5) | (X8 @ X5))))) & ((^[X18 : $i > $o] : (! [X19 : $i] : ~(X18 @ X19))) = iinvalid) & ((^[X8 : $i > $o, X9 : $i > $o, X7 : $i] : (! [X5 : $i] : ((X9 @ X5) | ~(irel @ X7 @ X5)) | ~! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5)))) = iimplies) & (iand = (^[X8 : $i > $o, X9 : $i > $o, X7 : $i] : (! [X5 : $i] : (~(irel @ X7 @ X5) | (X9 @ X5)) & ! [X5 : $i] : ((X8 @ X5) | ~(irel @ X7 @ X5))))) & ((^[X4 : $i > $o, X0 : $i] : (~(X4 @ X0))) = mnot) & (itrue @ (d2unsorted @ d_unsorted_0)) & ~(ifalse @ (d2unsorted @ d_unsorted_0)) & (irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0))),
% 1.91/1.84 file('/export/starexec/sandbox2/tmp/tmp.rHa6s2wqLE/DTF2THF_22212.p',lcl696_1)).
% 1.91/1.84 thf(f24,plain,(
% 1.91/1.84 ( ! [X3 : $i] : (((d2unsorted @ (sK0 @ X3)) = X3)) )),
% 1.91/1.84 inference(cnf_transformation,[status(thm)],[f15])).
% 1.91/1.84 thf(f296,plain,(
% 1.91/1.84 ((sK3 @ sK5) = $true) | ~spl1_2),
% 1.91/1.84 inference(trivial_inequality_removal,[status(thm)],[f294])).
% 1.91/1.84 thf(f294,plain,(
% 1.91/1.84 ($true = $false) | ((sK3 @ sK5) = $true) | ~spl1_2),
% 1.91/1.84 inference(superposition,[status(thm)],[f159,f67])).
% 1.91/1.84 thf(f67,plain,(
% 1.91/1.84 ( ! [X0 : $i] : (($true = (irel @ X0 @ X0))) )),
% 1.91/1.84 inference(superposition,[status(thm)],[f22,f45])).
% 1.91/1.84 thf(f22,plain,(
% 1.91/1.84 ((irel @ (d2unsorted @ d_unsorted_0) @ (d2unsorted @ d_unsorted_0)) = $true)),
% 1.91/1.84 inference(cnf_transformation,[status(thm)],[f15])).
% 1.91/1.84 thf(f159,plain,(
% 1.91/1.84 ( ! [X1 : $i] : (($false = (irel @ sK5 @ X1)) | ((sK3 @ X1) = $true)) ) | ~spl1_2),
% 1.91/1.84 inference(avatar_component_clause,[status(thm)],[f158])).
% 1.91/1.84 thf(f158,definition,(
% 1.91/1.84 spl1_2 <=> ! [X1 : $i] : (((sK3 @ X1) = $true) | ($false = (irel @ sK5 @ X1)))),
% 1.91/1.84 introduced(definition,[new_symbols(naming,[spl1_2])],[avatar_definition])).
% 1.91/1.84 thf(f178,plain,(
% 1.91/1.84 ((sK3 @ sK12) = $false) | ~spl1_6),
% 1.91/1.84 inference(avatar_component_clause,[status(thm)],[f176])).
% 1.91/1.84 thf(f176,definition,(
% 1.91/1.84 spl1_6 <=> ((sK3 @ sK12) = $false)),
% 1.91/1.84 introduced(definition,[new_symbols(naming,[spl1_6])],[avatar_definition])).
% 1.91/1.84 thf(f291,plain,(
% 1.91/1.84 ~spl1_1 | ~spl1_14),
% 1.91/1.84 inference(avatar_contradiction_clause,[status(thm)],[f290])).
% 1.91/1.84 thf(f290,plain,(
% 1.91/1.84 $false | (~spl1_1 | ~spl1_14)),
% 1.91/1.84 inference(trivial_inequality_removal,[status(thm)],[f287])).
% 1.91/1.84 thf(f287,plain,(
% 1.91/1.84 ($true = $false) | (~spl1_1 | ~spl1_14)),
% 1.91/1.84 inference(superposition,[status(thm)],[f273,f216])).
% 1.91/1.84 thf(f216,plain,(
% 1.91/1.84 ((sK4 @ sK8) = $false) | ~spl1_14),
% 1.91/1.84 inference(avatar_component_clause,[status(thm)],[f214])).
% 1.91/1.84 thf(f214,definition,(
% 1.91/1.84 spl1_14 <=> ((sK4 @ sK8) = $false)),
% 1.91/1.84 introduced(definition,[new_symbols(naming,[spl1_14])],[avatar_definition])).
% 1.91/1.84 thf(f273,plain,(
% 1.91/1.84 ( ! [X0 : $i] : (((sK4 @ X0) = $true)) ) | ~spl1_1),
% 1.91/1.84 inference(superposition,[status(thm)],[f271,f49])).
% 1.91/1.84 thf(f271,plain,(
% 1.91/1.84 ((sK4 @ sK5) = $true) | ~spl1_1),
% 1.91/1.84 inference(trivial_inequality_removal,[status(thm)],[f269])).
% 1.91/1.84 thf(f269,plain,(
% 1.91/1.84 ($true = $false) | ((sK4 @ sK5) = $true) | ~spl1_1),
% 1.91/1.84 inference(superposition,[status(thm)],[f156,f67])).
% 1.91/1.84 thf(f156,plain,(
% 1.91/1.84 ( ! [X2 : $i] : (($false = (irel @ sK5 @ X2)) | ((sK4 @ X2) = $true)) ) | ~spl1_1),
% 1.91/1.84 inference(avatar_component_clause,[status(thm)],[f155])).
% 1.91/1.84 thf(f155,definition,(
% 1.91/1.84 spl1_1 <=> ! [X2 : $i] : (($false = (irel @ sK5 @ X2)) | ((sK4 @ X2) = $true))),
% 1.91/1.84 introduced(definition,[new_symbols(naming,[spl1_1])],[avatar_definition])).
% 1.91/1.84 thf(f280,plain,(
% 1.91/1.84 ~spl1_1 | ~spl1_13),
% 1.91/1.84 inference(avatar_contradiction_clause,[status(thm)],[f279])).
% 1.91/1.84 thf(f279,plain,(
% 1.91/1.84 $false | (~spl1_1 | ~spl1_13)),
% 1.91/1.84 inference(trivial_inequality_removal,[status(thm)],[f276])).
% 1.91/1.84 thf(f276,plain,(
% 1.91/1.84 ($true = $false) | (~spl1_1 | ~spl1_13)),
% 1.91/1.84 inference(superposition,[status(thm)],[f212,f273])).
% 1.91/1.84 thf(f212,plain,(
% 1.91/1.84 ((sK4 @ sK6) = $false) | ~spl1_13),
% 1.91/1.84 inference(avatar_component_clause,[status(thm)],[f210])).
% 1.91/1.84 thf(f210,definition,(
% 1.91/1.84 spl1_13 <=> ((sK4 @ sK6) = $false)),
% 1.91/1.84 introduced(definition,[new_symbols(naming,[spl1_13])],[avatar_definition])).
% 1.91/1.84 thf(f264,plain,(
% 1.91/1.84 ~spl1_2 | ~spl1_4),
% 1.91/1.84 inference(avatar_contradiction_clause,[status(thm)],[f263])).
% 1.91/1.84 thf(f263,plain,(
% 1.91/1.84 $false | (~spl1_2 | ~spl1_4)),
% 1.91/1.84 inference(trivial_inequality_removal,[status(thm)],[f259])).
% 1.91/1.84 thf(f259,plain,(
% 1.91/1.84 ($true = $false) | (~spl1_2 | ~spl1_4)),
% 1.91/1.84 inference(superposition,[status(thm)],[f168,f247])).
% 1.91/1.84 thf(f247,plain,(
% 1.91/1.84 ( ! [X0 : $i] : (((sK3 @ X0) = $true)) ) | ~spl1_2),
% 1.91/1.84 inference(superposition,[status(thm)],[f245,f49])).
% 1.91/1.84 thf(f245,plain,(
% 1.91/1.84 ((sK3 @ sK5) = $true) | ~spl1_2),
% 1.91/1.84 inference(trivial_inequality_removal,[status(thm)],[f244])).
% 1.91/1.84 thf(f244,plain,(
% 1.91/1.84 ((sK3 @ sK5) = $true) | ($true = $false) | ~spl1_2),
% 1.91/1.84 inference(superposition,[status(thm)],[f67,f159])).
% 1.91/1.84 thf(f168,plain,(
% 1.91/1.84 ((sK3 @ sK9) = $false) | ~spl1_4),
% 1.91/1.84 inference(avatar_component_clause,[status(thm)],[f166])).
% 1.91/1.84 thf(f166,definition,(
% 1.91/1.84 spl1_4 <=> ((sK3 @ sK9) = $false)),
% 1.91/1.84 introduced(definition,[new_symbols(naming,[spl1_4])],[avatar_definition])).
% 1.91/1.84 thf(f217,plain,(
% 1.91/1.84 spl1_13 | spl1_14),
% 1.91/1.84 inference(avatar_split_clause,[status(thm)],[f104,f214,f210])).
% 1.91/1.84 thf(f104,plain,(
% 1.91/1.84 ((sK4 @ sK6) = $false) | ((sK4 @ sK8) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f97])).
% 1.91/1.84 thf(f97,plain,(
% 1.91/1.84 (((~ (irel @ sK5 @ sK8)) | (sK4 @ sK8)) = $false) | ((sK4 @ sK6) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f96])).
% 1.91/1.84 thf(f96,plain,(
% 1.91/1.84 (((~ (irel @ sK5 @ sK6)) | (sK4 @ sK6)) = $false) | (((~ (irel @ sK5 @ sK8)) | (sK4 @ sK8)) = $false)),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f95])).
% 1.91/1.84 thf(f95,plain,(
% 1.91/1.84 (((~ (irel @ sK5 @ sK6)) | (sK4 @ sK6)) = $false) | ($false = ((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))) @ sK8))),
% 1.91/1.84 inference(sigma_clausification,[status(thm)],[f82])).
% 1.91/1.84 thf(f82,plain,(
% 1.91/1.84 ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $false) | (((~ (irel @ sK5 @ sK6)) | (sK4 @ sK6)) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f81])).
% 1.91/1.84 thf(f81,plain,(
% 1.91/1.84 (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false) | (((~ (irel @ sK5 @ sK6)) | (sK4 @ sK6)) = $false)),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f80])).
% 1.91/1.84 thf(f80,plain,(
% 1.91/1.84 (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))) @ sK6) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false)),
% 1.91/1.84 inference(sigma_clausification,[status(thm)],[f79])).
% 1.91/1.84 thf(f79,plain,(
% 1.91/1.84 ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f77])).
% 1.91/1.84 thf(f77,plain,(
% 1.91/1.84 (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0))))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f75])).
% 1.91/1.84 thf(f75,plain,(
% 1.91/1.84 (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0))))) != ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))))),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f74])).
% 1.91/1.84 thf(f74,plain,(
% 1.91/1.84 (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK4 @ Y1)))))) @ sK5) != ((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK4 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) @ sK5))),
% 1.91/1.84 inference(negative_extensionality,[status(thm)],[f73])).
% 1.91/1.84 thf(f73,plain,(
% 1.91/1.84 ((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK4 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))))) != (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK3 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((~ (irel @ Y0 @ Y1)) | (sK4 @ Y1)))))))),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f72])).
% 1.91/1.84 thf(f72,plain,(
% 1.91/1.84 (((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) @ sK4) != ((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))))) @ sK4))),
% 1.91/1.84 inference(negative_extensionality,[status(thm)],[f71])).
% 1.91/1.84 thf(f71,plain,(
% 1.91/1.84 ((^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (sK3 @ Y2)))))))))),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f70])).
% 1.91/1.84 thf(f70,plain,(
% 1.91/1.84 (((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))) @ sK3) != ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))) @ sK3))),
% 1.91/1.84 inference(negative_extensionality,[status(thm)],[f41])).
% 1.91/1.84 thf(f41,plain,(
% 1.91/1.84 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))))))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f40])).
% 1.91/1.84 thf(f40,plain,(
% 1.91/1.84 ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y3 @ Y4) | (Y2 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((~ (irel @ Y3 @ Y4)) | (Y2 @ Y4))))))) @ Y1))))) != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))),
% 1.91/1.84 inference(definition_unfolding,[status(thm)],[f16,f21,f19,f18,f18])).
% 1.91/1.84 thf(f18,plain,(
% 1.91/1.84 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((~ (irel @ Y1 @ Y2)) | (Y0 @ Y2))))))))),
% 1.91/1.84 inference(cnf_transformation,[status(thm)],[f15])).
% 1.91/1.84 thf(f19,plain,(
% 1.91/1.84 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y1 @ Y2) | (Y0 @ Y2))))))))),
% 1.91/1.84 inference(cnf_transformation,[status(thm)],[f15])).
% 1.91/1.84 thf(f21,plain,(
% 1.91/1.84 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y0 @ Y3)))) | (!! @ $i @ (^[Y3 : $i]: ((~ (irel @ Y2 @ Y3)) | (Y1 @ Y3)))))))))))),
% 1.91/1.84 inference(cnf_transformation,[status(thm)],[f15])).
% 1.91/1.84 thf(f16,plain,(
% 1.91/1.84 (ior != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 1.91/1.84 inference(cnf_transformation,[status(thm)],[f11])).
% 1.91/1.84 thf(f11,plain,(
% 1.91/1.84 (ior != (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 1.91/1.84 inference(flattening,[status(thm)],[f8])).
% 1.91/1.84 thf(f8,plain,(
% 1.91/1.84 ~(ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 1.91/1.84 inference(fool_elimination,[status(thm)],[f7])).
% 1.91/1.84 thf(f7,plain,(
% 1.91/1.84 ~(ior = (^[X0 : $i > $o, X1 : $i > $o] : (mor @ (mbox_s4 @ X0) @ (mbox_s4 @ X1))))),
% 1.91/1.84 inference(rectify,[status(thm)],[f3])).
% 1.91/1.84 thf(f3,negated_conjecture,(
% 1.91/1.84 ~(ior = (^[X8 : $i > $o, X9 : $i > $o] : (mor @ (mbox_s4 @ X8) @ (mbox_s4 @ X9))))),
% 1.91/1.84 inference(negated_conjecture,[status(cth)],[f2])).
% 1.91/1.84 thf(f2,conjecture,(
% 1.91/1.84 (ior = (^[X8 : $i > $o, X9 : $i > $o] : (mor @ (mbox_s4 @ X8) @ (mbox_s4 @ X9))))),
% 1.91/1.84 file('/export/starexec/sandbox2/tmp/tmp.rHa6s2wqLE/DTF2THF_22212.p',ior)).
% 1.91/1.84 thf(f179,plain,(
% 1.91/1.84 spl1_6 | spl1_4),
% 1.91/1.84 inference(avatar_split_clause,[status(thm)],[f131,f166,f176])).
% 1.91/1.84 thf(f131,plain,(
% 1.91/1.84 ((sK3 @ sK9) = $false) | ((sK3 @ sK12) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f130])).
% 1.91/1.84 thf(f130,plain,(
% 1.91/1.84 (((~ (irel @ sK5 @ sK12)) | (sK3 @ sK12)) = $false) | ((sK3 @ sK9) = $false)),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f129])).
% 1.91/1.84 thf(f129,plain,(
% 1.91/1.84 ((sK3 @ sK9) = $false) | (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0))) @ sK12) = $false)),
% 1.91/1.84 inference(sigma_clausification,[status(thm)],[f128])).
% 1.91/1.84 thf(f128,plain,(
% 1.91/1.84 ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $false) | ((sK3 @ sK9) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f109])).
% 1.91/1.84 thf(f109,plain,(
% 1.91/1.84 ((sK3 @ sK9) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f108])).
% 1.91/1.84 thf(f108,plain,(
% 1.91/1.84 (((~ (irel @ sK5 @ sK9)) | (sK3 @ sK9)) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false)),
% 1.91/1.84 inference(beta_eta_normalization,[status(thm)],[f107])).
% 1.91/1.84 thf(f107,plain,(
% 1.91/1.84 (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0))) @ sK9) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false)),
% 1.91/1.84 inference(sigma_clausification,[status(thm)],[f78])).
% 1.91/1.84 thf(f78,plain,(
% 1.91/1.84 ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $false) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $false)),
% 1.91/1.84 inference(binary_proxy_clausification,[status(thm)],[f77])).
% 1.91/1.84 thf(f160,plain,(
% 1.91/1.84 spl1_1 | spl1_2 | spl1_2),
% 1.91/1.84 inference(avatar_split_clause,[status(thm)],[f153,f158,f158,f155])).
% 1.91/1.84 thf(f153,plain,(
% 1.91/1.84 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = (irel @ sK5 @ X2)) | ((sK3 @ X1) = $true) | ((sK3 @ X3) = $true) | ((irel @ sK5 @ X3) = $false) | ((sK4 @ X2) = $true) | ($false = (irel @ sK5 @ X1))) )),
% 1.91/1.85 inference(not_proxy_clausification,[status(thm)],[f152])).
% 1.91/1.85 thf(f152,plain,(
% 1.91/1.85 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((sK3 @ X1) = $true) | ((sK4 @ X2) = $true) | ($false = (irel @ sK5 @ X2)) | ((sK3 @ X3) = $true) | ($true = (~ (irel @ sK5 @ X3))) | ($false = (irel @ sK5 @ X1))) )),
% 1.91/1.85 inference(binary_proxy_clausification,[status(thm)],[f151])).
% 1.91/1.85 thf(f151,plain,(
% 1.91/1.85 ( ! [X2 : $i,X3 : $i,X1 : $i] : (((sK4 @ X2) = $true) | ((sK3 @ X1) = $true) | ($false = (irel @ sK5 @ X2)) | ($true = ((~ (irel @ sK5 @ X3)) | (sK3 @ X3))) | ($false = (irel @ sK5 @ X1))) )),
% 1.91/1.85 inference(not_proxy_clausification,[status(thm)],[f150])).
% 1.91/1.85 thf(f150,plain,(
% 1.91/1.85 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = (irel @ sK5 @ X1)) | ((sK4 @ X2) = $true) | ((~ (irel @ sK5 @ X2)) = $true) | ($true = ((~ (irel @ sK5 @ X3)) | (sK3 @ X3))) | ((sK3 @ X1) = $true)) )),
% 1.91/1.85 inference(beta_eta_normalization,[status(thm)],[f149])).
% 1.91/1.85 thf(f149,plain,(
% 1.91/1.85 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = (irel @ sK5 @ X1)) | ((sK4 @ X2) = $true) | ((sK3 @ X1) = $true) | (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0))) @ X3) = $true) | ((~ (irel @ sK5 @ X2)) = $true)) )),
% 1.91/1.85 inference(pi_clausification,[status(thm)],[f148])).
% 1.91/1.85 thf(f148,plain,(
% 1.91/1.85 ( ! [X2 : $i,X1 : $i] : (($false = (irel @ sK5 @ X1)) | ((sK4 @ X2) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $true) | ((sK3 @ X1) = $true) | ((~ (irel @ sK5 @ X2)) = $true)) )),
% 1.91/1.85 inference(binary_proxy_clausification,[status(thm)],[f147])).
% 1.91/1.85 thf(f147,plain,(
% 1.91/1.85 ( ! [X2 : $i,X1 : $i] : ((((~ (irel @ sK5 @ X2)) | (sK4 @ X2)) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $true) | ($false = (irel @ sK5 @ X1)) | ((sK3 @ X1) = $true)) )),
% 1.91/1.85 inference(not_proxy_clausification,[status(thm)],[f146])).
% 1.91/1.85 thf(f146,plain,(
% 1.91/1.85 ( ! [X2 : $i,X1 : $i] : (((~ (irel @ sK5 @ X1)) = $true) | (((~ (irel @ sK5 @ X2)) | (sK4 @ X2)) = $true) | ((sK3 @ X1) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $true)) )),
% 1.91/1.85 inference(beta_eta_normalization,[status(thm)],[f145])).
% 1.91/1.85 thf(f145,plain,(
% 1.91/1.85 ( ! [X2 : $i,X1 : $i] : (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $true) | (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))) @ X2) = $true) | ((sK3 @ X1) = $true) | ((~ (irel @ sK5 @ X1)) = $true)) )),
% 1.91/1.85 inference(pi_clausification,[status(thm)],[f144])).
% 1.91/1.85 thf(f144,plain,(
% 1.91/1.85 ( ! [X1 : $i] : (((sK3 @ X1) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $true) | ((~ (irel @ sK5 @ X1)) = $true)) )),
% 1.91/1.85 inference(duplicate_literal_removal,[status(thm)],[f143])).
% 1.91/1.85 thf(f143,plain,(
% 1.91/1.85 ( ! [X1 : $i] : (((~ (irel @ sK5 @ X1)) = $true) | ((sK3 @ X1) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $true)) )),
% 1.91/1.85 inference(binary_proxy_clausification,[status(thm)],[f142])).
% 1.91/1.85 thf(f142,plain,(
% 1.91/1.85 ( ! [X1 : $i] : (((sK3 @ X1) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $true) | ((~ (irel @ sK5 @ X1)) = $true)) )),
% 1.91/1.85 inference(binary_proxy_clausification,[status(thm)],[f141])).
% 1.91/1.85 thf(f141,plain,(
% 1.91/1.85 ( ! [X1 : $i] : ((((~ (irel @ sK5 @ X1)) | (sK3 @ X1)) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $true)) )),
% 1.91/1.85 inference(beta_eta_normalization,[status(thm)],[f140])).
% 1.91/1.85 thf(f140,plain,(
% 1.91/1.85 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $true) | (((^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0))) @ X1) = $true)) )),
% 1.91/1.85 inference(pi_clausification,[status(thm)],[f139])).
% 1.91/1.85 thf(f139,plain,(
% 1.91/1.85 ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) = $true) | ((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $true)),
% 1.91/1.85 inference(binary_proxy_clausification,[status(thm)],[f76])).
% 1.91/1.85 thf(f76,plain,(
% 1.91/1.85 (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0))))) = $true) | (((!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK3 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((~ (irel @ sK5 @ Y0)) | (sK4 @ Y0))))) = $true)),
% 1.91/1.85 inference(binary_proxy_clausification,[status(thm)],[f75])).
% 1.91/1.85 % SZS output end Proof for DTF2THF_22212
% 1.91/1.85 % (22353)------------------------------
% 1.91/1.85 % (22353)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.91/1.85 % (22353)Termination reason: Refutation
% 1.91/1.85
% 1.91/1.85 % (22353)Memory used [KB]: 5884
% 1.91/1.85 % (22353)Time elapsed: 0.023 s
% 1.91/1.85 % (22353)Instructions burned: 26 (million)
% 1.91/1.85 % (22353)------------------------------
% 1.91/1.85 % (22353)------------------------------
% 1.91/1.85 % (22350)Success in time 0.038 s
%------------------------------------------------------------------------------