%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWX180^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:40:27 AM UTC 2026
% Result : Theorem 0.39s 0.32s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 2
% Syntax : Number of formulae : 54 ( 29 unt; 0 typ; 0 def)
% Number of atoms : 388 ( 74 equ; 0 cnn)
% Maximal formula atoms : 109 ( 7 avg)
% Number of connectives : 1640 ( 255 ~; 234 |; 170 &; 946 @)
% ( 30 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 224 ( 11 avg)
% Number of types : 5 ( 3 usr)
% Number of type conns : 248 ( 248 >; 0 *; 0 +; 0 <<)
% Number of symbols : 80 ( 78 usr; 5 con; 0-4 aty)
% Number of variables : 397 ( 55 ^; 338 !; 4 ?; 397 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
mu: $tType ).
thf(decl_sort2,type,
d_unsorted: $tType ).
thf(decl_sort3,type,
d_mu: $tType ).
thf(decl_23,type,
meq_ind: mu > mu > $i > $o ).
thf(decl_24,type,
meq_prop: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_25,type,
mnot: ( $i > $o ) > $i > $o ).
thf(decl_26,type,
mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_27,type,
mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_28,type,
mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_29,type,
mimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_30,type,
mequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_31,type,
mxor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_32,type,
mforall_ind: ( mu > $i > $o ) > $i > $o ).
thf(decl_33,type,
mforall_prop: ( ( $i > $o ) > $i > $o ) > $i > $o ).
thf(decl_34,type,
mexists_ind: ( mu > $i > $o ) > $i > $o ).
thf(decl_35,type,
mexists_prop: ( ( $i > $o ) > $i > $o ) > $i > $o ).
thf(decl_36,type,
mtrue: $i > $o ).
thf(decl_37,type,
mfalse: $i > $o ).
thf(decl_38,type,
mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_39,type,
mdia: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(decl_40,type,
mreflexive: ( $i > $i > $o ) > $o ).
thf(decl_41,type,
msymmetric: ( $i > $i > $o ) > $o ).
thf(decl_42,type,
mserial: ( $i > $i > $o ) > $o ).
thf(decl_43,type,
mtransitive: ( $i > $i > $o ) > $o ).
thf(decl_44,type,
meuclidean: ( $i > $i > $o ) > $o ).
thf(decl_45,type,
mpartially_functional: ( $i > $i > $o ) > $o ).
thf(decl_46,type,
mfunctional: ( $i > $i > $o ) > $o ).
thf(decl_47,type,
mweakly_dense: ( $i > $i > $o ) > $o ).
thf(decl_48,type,
mweakly_connected: ( $i > $i > $o ) > $o ).
thf(decl_49,type,
mweakly_directed: ( $i > $i > $o ) > $o ).
thf(decl_50,type,
mvalid: ( $i > $o ) > $o ).
thf(decl_51,type,
minvalid: ( $i > $o ) > $o ).
thf(decl_52,type,
msatisfiable: ( $i > $o ) > $o ).
thf(decl_53,type,
mcountersatisfiable: ( $i > $o ) > $o ).
thf(decl_54,type,
d2unsorted: d_unsorted > $i ).
thf(decl_55,type,
d2mu: d_mu > mu ).
thf(decl_56,type,
d_unsorted_0: d_unsorted ).
thf(decl_57,type,
d_mu_0: d_mu ).
thf(decl_58,type,
esk1_1: $i > d_unsorted ).
thf(decl_59,type,
esk2_1: mu > d_mu ).
thf(decl_60,type,
esk3_2: ( mu > $i > $o ) > $i > mu ).
thf(decl_61,type,
epred1_2: ( ( $i > $o ) > $i > $o ) > $i > $i > $o ).
thf(decl_62,type,
esk4_2: ( mu > $i > $o ) > $i > mu ).
thf(decl_63,type,
epred2_2: ( ( $i > $o ) > $i > $o ) > $i > $i > $o ).
thf(decl_64,type,
esk5_3: ( $i > $i > $o ) > ( $i > $o ) > $i > $i ).
thf(decl_65,type,
esk6_3: ( $i > $i > $o ) > ( $i > $o ) > $i > $i ).
thf(decl_66,type,
esk7_1: ( $i > $i > $o ) > $i ).
thf(decl_67,type,
esk8_1: ( $i > $i > $o ) > $i ).
thf(decl_68,type,
esk9_1: ( $i > $i > $o ) > $i ).
thf(decl_69,type,
esk10_2: ( $i > $i > $o ) > $i > $i ).
thf(decl_70,type,
esk11_1: ( $i > $i > $o ) > $i ).
thf(decl_71,type,
esk12_1: ( $i > $i > $o ) > $i ).
thf(decl_72,type,
esk13_1: ( $i > $i > $o ) > $i ).
thf(decl_73,type,
esk14_1: ( $i > $i > $o ) > $i ).
thf(decl_74,type,
esk15_1: ( $i > $i > $o ) > $i ).
thf(decl_75,type,
esk16_1: ( $i > $i > $o ) > $i ).
thf(decl_76,type,
esk17_1: ( $i > $i > $o ) > $i ).
thf(decl_77,type,
esk18_1: ( $i > $i > $o ) > $i ).
thf(decl_78,type,
esk19_1: ( $i > $i > $o ) > $i ).
thf(decl_79,type,
esk20_1: ( $i > $i > $o ) > $i ).
thf(decl_80,type,
esk21_2: ( $i > $i > $o ) > $i > $i ).
thf(decl_81,type,
esk22_1: ( $i > $i > $o ) > $i ).
thf(decl_82,type,
esk23_2: ( $i > $i > $o ) > $i > $i ).
thf(decl_83,type,
esk24_3: ( $i > $i > $o ) > $i > $i > $i ).
thf(decl_84,type,
esk25_1: ( $i > $i > $o ) > $i ).
thf(decl_85,type,
esk26_1: ( $i > $i > $o ) > $i ).
thf(decl_86,type,
esk27_1: ( $i > $i > $o ) > $i ).
thf(decl_87,type,
esk28_1: ( $i > $i > $o ) > $i ).
thf(decl_88,type,
esk29_1: ( $i > $i > $o ) > $i ).
thf(decl_89,type,
esk30_4: ( $i > $i > $o ) > $i > $i > $i > $i ).
thf(decl_90,type,
esk31_1: ( $i > $i > $o ) > $i ).
thf(decl_91,type,
esk32_1: ( $i > $i > $o ) > $i ).
thf(decl_92,type,
esk33_1: ( $i > $i > $o ) > $i ).
thf(decl_93,type,
esk34_1: ( $i > $o ) > $i ).
thf(decl_94,type,
esk35_1: ( $i > $o ) > $i ).
thf(decl_95,type,
esk36_1: ( $i > $o ) > $i ).
thf(decl_96,type,
esk37_1: ( $i > $o ) > $i ).
thf(decl_97,type,
epred3_0: $i > $o ).
thf(decl_98,type,
epred4_0: $i > $o ).
thf(decl_99,type,
esk38_0: $i ).
thf(decl_101,type,
esk5_0: $i ).
thf(lcl698_1,axiom,
( ! [X1: $i] :
? [X2: d_unsorted] :
( X1
= ( d2unsorted @ X2 ) )
& ! [X2: d_unsorted] : ( X2 = d_unsorted_0 )
& ! [X3: d_unsorted,X4: d_unsorted] :
( ( ( d2unsorted @ X3 )
= ( d2unsorted @ X4 ) )
=> ( X3 = X4 ) )
& ! [X5: mu] :
? [X6: d_mu] :
( X5
= ( d2mu @ X6 ) )
& ! [X6: d_mu] : ( X6 = d_mu_0 )
& ! [X7: d_mu,X8: d_mu] :
( ( ( d2mu @ X7 )
= ( d2mu @ X8 ) )
=> ( X7 = X8 ) )
& ( meq_prop
= ( ^ [X9: $i > $o,X10: $i > $o,X11: $i] :
( ( X9 @ X11 )
<=> ( X10 @ X11 ) ) ) )
& ( mnot
= ( ^ [X12: $i > $o,X11: $i] :
~ ( X12 @ X11 ) ) )
& ( mor
= ( ^ [X12: $i > $o,X13: $i > $o,X11: $i] :
( ( X12 @ X11 )
| ( X13 @ X11 ) ) ) )
& ( mand
= ( ^ [X12: $i > $o,X13: $i > $o,X14: $i] :
~ ( ~ ( X12 @ X14 )
| ~ ( X13 @ X14 ) ) ) )
& ( mimplies
= ( ^ [X12: $i > $o,X13: $i > $o,X14: $i] :
( ~ ( X12 @ X14 )
| ( X13 @ X14 ) ) ) )
& ( mimplied
= ( ^ [X12: $i > $o,X13: $i > $o,X14: $i] :
( ~ ( X13 @ X14 )
| ( X12 @ X14 ) ) ) )
& ( mequiv
= ( ^ [X12: $i > $o,X13: $i > $o,X14: $i] :
~ ( ~ ( ~ ( X12 @ X14 )
| ( X13 @ X14 ) )
| ~ ( ~ ( X13 @ X14 )
| ( X12 @ X14 ) ) ) ) )
& ( mxor
= ( ^ [X12: $i > $o,X13: $i > $o,X14: $i] :
( ~ ( ~ ( X12 @ X14 )
| ( X13 @ X14 ) )
| ~ ( ~ ( X13 @ X14 )
| ( X12 @ X14 ) ) ) ) )
& ( mforall_ind
= ( ^ [X15: mu > $i > $o,X11: $i] :
! [X16: mu] : ( X15 @ X16 @ X11 ) ) )
& ( mforall_prop
= ( ^ [X17: ( $i > $o ) > $i > $o,X11: $i] :
! [X18: $i > $o] : ( X17 @ X18 @ X11 ) ) )
& ( mexists_ind
= ( ^ [X19: mu > $i > $o,X14: $i] :
~ ! [X20: mu] :
~ ( X19 @ X20 @ X14 ) ) )
& ( mexists_prop
= ( ^ [X21: ( $i > $o ) > $i > $o,X14: $i] :
~ ! [X18: $i > $o] :
~ ( X21 @ X18 @ X14 ) ) )
& ( mbox
= ( ^ [X22: $i > $i > $o,X12: $i > $o,X11: $i] :
! [X23: $i] :
( ~ ( X22 @ X11 @ X23 )
| ( X12 @ X23 ) ) ) )
& ( mdia
= ( ^ [X22: $i > $i > $o,X12: $i > $o,X14: $i] :
~ ! [X23: $i] :
( ~ ( X22 @ X14 @ X23 )
| ~ ( X12 @ X23 ) ) ) )
& ( mreflexive
= ( ^ [X22: $i > $i > $o] :
! [X24: $i] : ( X22 @ X24 @ X24 ) ) )
& ( msymmetric
= ( ^ [X22: $i > $i > $o] :
! [X24: $i,X25: $i] :
( ~ ( X22 @ X24 @ X25 )
| ( X22 @ X25 @ X24 ) ) ) )
& ( mserial
= ( ^ [X22: $i > $i > $o] :
! [X24: $i] :
~ ! [X25: $i] :
~ ( X22 @ X24 @ X25 ) ) )
& ( mtransitive
= ( ^ [X22: $i > $i > $o] :
! [X24: $i,X25: $i,X1: $i] :
( ~ ( X22 @ X24 @ X25 )
| ~ ( X22 @ X25 @ X1 )
| ( X22 @ X24 @ X1 ) ) ) )
& ( meuclidean
= ( ^ [X22: $i > $i > $o] :
! [X24: $i,X25: $i,X1: $i] :
( ~ ( X22 @ X24 @ X25 )
| ~ ( X22 @ X24 @ X1 )
| ( X22 @ X25 @ X1 ) ) ) )
& ( mpartially_functional
= ( ^ [X22: $i > $i > $o] :
! [X24: $i,X25: $i,X1: $i] :
( ~ ( X22 @ X24 @ X25 )
| ~ ( X22 @ X24 @ X1 )
| ( X25 = X1 ) ) ) )
& ( mfunctional
= ( ^ [X22: $i > $i > $o] :
! [X24: $i] :
~ ! [X25: $i] :
( ~ ( X22 @ X24 @ X25 )
| ~ ! [X1: $i] :
( ~ ( X22 @ X24 @ X1 )
| ( X25 = X1 ) ) ) ) )
& ( mweakly_dense
= ( ^ [X22: $i > $i > $o] :
! [X24: $i,X25: $i] :
( ~ ( X22 @ X24 @ X25 )
| ~ ! [X26: $i] :
( ~ ( X22 @ X24 @ X26 )
| ~ ( X22 @ X26 @ X25 ) ) ) ) )
& ( mweakly_connected
= ( ^ [X22: $i > $i > $o] :
! [X24: $i,X25: $i,X1: $i] :
( ~ ( X22 @ X24 @ X25 )
| ~ ( X22 @ X24 @ X1 )
| ( X22 @ X25 @ X1 )
| ( X25 = X1 )
| ( X22 @ X1 @ X25 ) ) ) )
& ( mweakly_directed
= ( ^ [X22: $i > $i > $o] :
! [X24: $i,X25: $i,X1: $i] :
( ~ ( X22 @ X24 @ X25 )
| ~ ( X22 @ X24 @ X1 )
| ~ ! [X23: $i] :
( ~ ( X22 @ X25 @ X23 )
| ~ ( X22 @ X1 @ X23 ) ) ) ) )
& ( mvalid
= ( ^ [X12: $i > $o] :
! [X11: $i] : ( X12 @ X11 ) ) )
& ( minvalid
= ( ^ [X12: $i > $o] :
! [X11: $i] :
~ ( X12 @ X11 ) ) )
& ( msatisfiable
= ( ^ [X12: $i > $o] :
~ ! [X11: $i] :
~ ( X12 @ X11 ) ) )
& ( mcountersatisfiable
= ( ^ [X12: $i > $o] :
~ ! [X11: $i] : ( X12 @ X11 ) ) )
& ( meq_ind @ ( d2mu @ d_mu_0 ) @ ( d2mu @ d_mu_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
& ( mtrue @ ( d2unsorted @ d_unsorted_0 ) )
& ~ ( mfalse @ ( d2unsorted @ d_unsorted_0 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.bxCrPn2Vv3/E---3.1_796576.p',lcl698_1) ).
thf(mequiv,conjecture,
( mequiv
= ( ^ [X12: $i > $o,X13: $i > $o] : ( mand @ ( mimplies @ X12 @ X13 ) @ ( mimplies @ X13 @ X12 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.bxCrPn2Vv3/E---3.1_796576.p',mequiv) ).
thf(c_0_2,plain,
( ! [X1: $i] :
? [X2: d_unsorted] :
( X1
= ( d2unsorted @ X2 ) )
& ! [X2: d_unsorted] : ( X2 = d_unsorted_0 )
& ! [X3: d_unsorted,X4: d_unsorted] :
( ( ( d2unsorted @ X3 )
= ( d2unsorted @ X4 ) )
=> ( X3 = X4 ) )
& ! [X5: mu] :
? [X6: d_mu] :
( X5
= ( d2mu @ X6 ) )
& ! [X6: d_mu] : ( X6 = d_mu_0 )
& ! [X7: d_mu,X8: d_mu] :
( ( ( d2mu @ X7 )
= ( d2mu @ X8 ) )
=> ( X7 = X8 ) )
& ! [X37: $i > $o,X38: $i > $o,X39: $i] :
( ( meq_prop @ X37 @ X38 @ X39 )
<=> ( ( X37 @ X39 )
<=> ( X38 @ X39 ) ) )
& ! [X40: $i > $o,X41: $i] :
( ( mnot @ X40 @ X41 )
<=> ~ ( X40 @ X41 ) )
& ! [X42: $i > $o,X43: $i > $o,X44: $i] :
( ( mor @ X42 @ X43 @ X44 )
<=> ( ( X42 @ X44 )
| ( X43 @ X44 ) ) )
& ! [X45: $i > $o,X46: $i > $o,X47: $i] :
( ( mand @ X45 @ X46 @ X47 )
<=> ~ ( ~ ( X45 @ X47 )
| ~ ( X46 @ X47 ) ) )
& ! [X48: $i > $o,X49: $i > $o,X50: $i] :
( ( mimplies @ X48 @ X49 @ X50 )
<=> ( ~ ( X48 @ X50 )
| ( X49 @ X50 ) ) )
& ! [X51: $i > $o,X52: $i > $o,X53: $i] :
( ( mimplied @ X51 @ X52 @ X53 )
<=> ( ~ ( X52 @ X53 )
| ( X51 @ X53 ) ) )
& ! [X54: $i > $o,X55: $i > $o,X56: $i] :
( ( mequiv @ X54 @ X55 @ X56 )
<=> ~ ( ~ ( ~ ( X54 @ X56 )
| ( X55 @ X56 ) )
| ~ ( ~ ( X55 @ X56 )
| ( X54 @ X56 ) ) ) )
& ! [X57: $i > $o,X58: $i > $o,X59: $i] :
( ( mxor @ X57 @ X58 @ X59 )
<=> ( ~ ( ~ ( X57 @ X59 )
| ( X58 @ X59 ) )
| ~ ( ~ ( X58 @ X59 )
| ( X57 @ X59 ) ) ) )
& ! [X60: mu > $i > $o,X61: $i] :
( ( mforall_ind @ X60 @ X61 )
<=> ! [X16: mu] : ( X60 @ X16 @ X61 ) )
& ! [X62: ( $i > $o ) > $i > $o,X63: $i] :
( ( mforall_prop @ X62 @ X63 )
<=> ! [X18: $i > $o] : ( X62 @ X18 @ X63 ) )
& ! [X64: mu > $i > $o,X65: $i] :
( ( mexists_ind @ X64 @ X65 )
<=> ~ ! [X20: mu] :
~ ( X64 @ X20 @ X65 ) )
& ! [X66: ( $i > $o ) > $i > $o,X67: $i] :
( ( mexists_prop @ X66 @ X67 )
<=> ~ ! [X18: $i > $o] :
~ ( X66 @ X18 @ X67 ) )
& ! [X68: $i > $i > $o,X69: $i > $o,X70: $i] :
( ( mbox @ X68 @ X69 @ X70 )
<=> ! [X23: $i] :
( ~ ( X68 @ X70 @ X23 )
| ( X69 @ X23 ) ) )
& ! [X71: $i > $i > $o,X72: $i > $o,X73: $i] :
( ( mdia @ X71 @ X72 @ X73 )
<=> ~ ! [X23: $i] :
( ~ ( X71 @ X73 @ X23 )
| ~ ( X72 @ X23 ) ) )
& ! [X74: $i > $i > $o] :
( ( mreflexive @ X74 )
<=> ! [X24: $i] : ( X74 @ X24 @ X24 ) )
& ! [X75: $i > $i > $o] :
( ( msymmetric @ X75 )
<=> ! [X24: $i,X25: $i] :
( ~ ( X75 @ X24 @ X25 )
| ( X75 @ X25 @ X24 ) ) )
& ! [X76: $i > $i > $o] :
( ( mserial @ X76 )
<=> ! [X24: $i] :
~ ! [X25: $i] :
~ ( X76 @ X24 @ X25 ) )
& ! [X77: $i > $i > $o] :
( ( mtransitive @ X77 )
<=> ! [X24: $i,X25: $i,X1: $i] :
( ~ ( X77 @ X24 @ X25 )
| ~ ( X77 @ X25 @ X1 )
| ( X77 @ X24 @ X1 ) ) )
& ! [X78: $i > $i > $o] :
( ( meuclidean @ X78 )
<=> ! [X24: $i,X25: $i,X1: $i] :
( ~ ( X78 @ X24 @ X25 )
| ~ ( X78 @ X24 @ X1 )
| ( X78 @ X25 @ X1 ) ) )
& ! [X79: $i > $i > $o] :
( ( mpartially_functional @ X79 )
<=> ! [X24: $i,X25: $i,X1: $i] :
( ~ ( X79 @ X24 @ X25 )
| ~ ( X79 @ X24 @ X1 )
| ( X25 = X1 ) ) )
& ! [X80: $i > $i > $o] :
( ( mfunctional @ X80 )
<=> ! [X24: $i] :
~ ! [X25: $i] :
( ~ ( X80 @ X24 @ X25 )
| ~ ! [X1: $i] :
( ~ ( X80 @ X24 @ X1 )
| ( X25 = X1 ) ) ) )
& ! [X81: $i > $i > $o] :
( ( mweakly_dense @ X81 )
<=> ! [X24: $i,X25: $i] :
( ~ ( X81 @ X24 @ X25 )
| ~ ! [X26: $i] :
( ~ ( X81 @ X24 @ X26 )
| ~ ( X81 @ X26 @ X25 ) ) ) )
& ! [X82: $i > $i > $o] :
( ( mweakly_connected @ X82 )
<=> ! [X24: $i,X25: $i,X1: $i] :
( ~ ( X82 @ X24 @ X25 )
| ~ ( X82 @ X24 @ X1 )
| ( X82 @ X25 @ X1 )
| ( X25 = X1 )
| ( X82 @ X1 @ X25 ) ) )
& ! [X83: $i > $i > $o] :
( ( mweakly_directed @ X83 )
<=> ! [X24: $i,X25: $i,X1: $i] :
( ~ ( X83 @ X24 @ X25 )
| ~ ( X83 @ X24 @ X1 )
| ~ ! [X23: $i] :
( ~ ( X83 @ X25 @ X23 )
| ~ ( X83 @ X1 @ X23 ) ) ) )
& ! [X84: $i > $o] :
( ( mvalid @ X84 )
<=> ! [X11: $i] : ( X84 @ X11 ) )
& ! [X85: $i > $o] :
( ( minvalid @ X85 )
<=> ! [X11: $i] :
~ ( X85 @ X11 ) )
& ! [X86: $i > $o] :
( ( msatisfiable @ X86 )
<=> ~ ! [X11: $i] :
~ ( X86 @ X11 ) )
& ! [X87: $i > $o] :
( ( mcountersatisfiable @ X87 )
<=> ~ ! [X11: $i] : ( X87 @ X11 ) )
& ( meq_ind @ ( d2mu @ d_mu_0 ) @ ( d2mu @ d_mu_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
& ( mtrue @ ( d2unsorted @ d_unsorted_0 ) )
& ~ ( mfalse @ ( d2unsorted @ d_unsorted_0 ) ) ),
inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[lcl698_1])])]) ).
thf(c_0_3,negated_conjecture,
( mequiv
!= ( ^ [X12: $i > $o,X13: $i > $o] : ( mand @ ( mimplies @ X12 @ X13 ) @ ( mimplies @ X13 @ X12 ) ) ) ),
inference(assume_negation,[status(cth)],[mequiv]) ).
thf(c_0_4,plain,
! [X90: $i,X92: d_unsorted,X93: d_unsorted,X94: d_unsorted,X95: mu,X97: d_mu,X98: d_mu,X99: d_mu,X100: $i > $o,X101: $i > $o,X102: $i,X103: $i > $o,X104: $i,X105: $i > $o,X106: $i > $o,X107: $i,X108: $i > $o,X109: $i > $o,X110: $i,X111: $i > $o,X112: $i > $o,X113: $i,X114: $i > $o,X115: $i > $o,X116: $i,X117: $i > $o,X118: $i > $o,X119: $i,X120: $i > $o,X121: $i > $o,X122: $i,X123: mu > $i > $o,X124: $i,X125: mu,X126: mu > $i > $o,X127: $i,X129: ( $i > $o ) > $i > $o,X130: $i,X131: $i > $o,X132: ( $i > $o ) > $i > $o,X133: $i,X135: mu > $i > $o,X136: $i,X138: mu > $i > $o,X139: $i,X140: mu,X141: ( $i > $o ) > $i > $o,X142: $i,X144: ( $i > $o ) > $i > $o,X145: $i,X146: $i > $o,X147: $i > $i > $o,X148: $i > $o,X149: $i,X150: $i,X151: $i > $i > $o,X152: $i > $o,X153: $i,X155: $i > $i > $o,X156: $i > $o,X157: $i,X159: $i > $i > $o,X160: $i > $o,X161: $i,X162: $i,X163: $i > $i > $o,X164: $i,X165: $i > $i > $o,X167: $i > $i > $o,X168: $i,X169: $i,X170: $i > $i > $o,X173: $i > $i > $o,X174: $i,X176: $i > $i > $o,X178: $i,X179: $i > $i > $o,X180: $i,X181: $i,X182: $i,X183: $i > $i > $o,X187: $i > $i > $o,X188: $i,X189: $i,X190: $i,X191: $i > $i > $o,X195: $i > $i > $o,X196: $i,X197: $i,X198: $i,X199: $i > $i > $o,X203: $i > $i > $o,X204: $i,X206: $i,X207: $i > $i > $o,X209: $i,X211: $i > $i > $o,X212: $i,X213: $i,X215: $i > $i > $o,X218: $i,X219: $i > $i > $o,X220: $i,X221: $i,X222: $i,X223: $i > $i > $o,X227: $i > $i > $o,X228: $i,X229: $i,X230: $i,X232: $i > $i > $o,X236: $i,X237: $i > $o,X238: $i,X239: $i > $o,X241: $i > $o,X242: $i,X243: $i > $o,X245: $i > $o,X247: $i > $o,X248: $i,X249: $i > $o,X251: $i > $o,X252: $i] :
( ( X90
= ( d2unsorted @ ( esk1_1 @ X90 ) ) )
& ( X92 = d_unsorted_0 )
& ( ( ( d2unsorted @ X93 )
!= ( d2unsorted @ X94 ) )
| ( X93 = X94 ) )
& ( X95
= ( d2mu @ ( esk2_1 @ X95 ) ) )
& ( X97 = d_mu_0 )
& ( ( ( d2mu @ X98 )
!= ( d2mu @ X99 ) )
| ( X98 = X99 ) )
& ( ~ ( X100 @ X102 )
| ( X101 @ X102 )
| ~ ( meq_prop @ X100 @ X101 @ X102 ) )
& ( ~ ( X101 @ X102 )
| ( X100 @ X102 )
| ~ ( meq_prop @ X100 @ X101 @ X102 ) )
& ( ~ ( X100 @ X102 )
| ~ ( X101 @ X102 )
| ( meq_prop @ X100 @ X101 @ X102 ) )
& ( ( X100 @ X102 )
| ( X101 @ X102 )
| ( meq_prop @ X100 @ X101 @ X102 ) )
& ( ~ ( mnot @ X103 @ X104 )
| ~ ( X103 @ X104 ) )
& ( ( X103 @ X104 )
| ( mnot @ X103 @ X104 ) )
& ( ~ ( mor @ X105 @ X106 @ X107 )
| ( X105 @ X107 )
| ( X106 @ X107 ) )
& ( ~ ( X105 @ X107 )
| ( mor @ X105 @ X106 @ X107 ) )
& ( ~ ( X106 @ X107 )
| ( mor @ X105 @ X106 @ X107 ) )
& ( ( X108 @ X110 )
| ~ ( mand @ X108 @ X109 @ X110 ) )
& ( ( X109 @ X110 )
| ~ ( mand @ X108 @ X109 @ X110 ) )
& ( ~ ( X108 @ X110 )
| ~ ( X109 @ X110 )
| ( mand @ X108 @ X109 @ X110 ) )
& ( ~ ( mimplies @ X111 @ X112 @ X113 )
| ~ ( X111 @ X113 )
| ( X112 @ X113 ) )
& ( ( X111 @ X113 )
| ( mimplies @ X111 @ X112 @ X113 ) )
& ( ~ ( X112 @ X113 )
| ( mimplies @ X111 @ X112 @ X113 ) )
& ( ~ ( mimplied @ X114 @ X115 @ X116 )
| ~ ( X115 @ X116 )
| ( X114 @ X116 ) )
& ( ( X115 @ X116 )
| ( mimplied @ X114 @ X115 @ X116 ) )
& ( ~ ( X114 @ X116 )
| ( mimplied @ X114 @ X115 @ X116 ) )
& ( ~ ( X117 @ X119 )
| ( X118 @ X119 )
| ~ ( mequiv @ X117 @ X118 @ X119 ) )
& ( ~ ( X118 @ X119 )
| ( X117 @ X119 )
| ~ ( mequiv @ X117 @ X118 @ X119 ) )
& ( ( X118 @ X119 )
| ( X117 @ X119 )
| ( mequiv @ X117 @ X118 @ X119 ) )
& ( ~ ( X117 @ X119 )
| ( X117 @ X119 )
| ( mequiv @ X117 @ X118 @ X119 ) )
& ( ( X118 @ X119 )
| ~ ( X118 @ X119 )
| ( mequiv @ X117 @ X118 @ X119 ) )
& ( ~ ( X117 @ X119 )
| ~ ( X118 @ X119 )
| ( mequiv @ X117 @ X118 @ X119 ) )
& ( ( X121 @ X122 )
| ( X120 @ X122 )
| ~ ( mxor @ X120 @ X121 @ X122 ) )
& ( ~ ( X120 @ X122 )
| ( X120 @ X122 )
| ~ ( mxor @ X120 @ X121 @ X122 ) )
& ( ( X121 @ X122 )
| ~ ( X121 @ X122 )
| ~ ( mxor @ X120 @ X121 @ X122 ) )
& ( ~ ( X120 @ X122 )
| ~ ( X121 @ X122 )
| ~ ( mxor @ X120 @ X121 @ X122 ) )
& ( ~ ( X120 @ X122 )
| ( X121 @ X122 )
| ( mxor @ X120 @ X121 @ X122 ) )
& ( ~ ( X121 @ X122 )
| ( X120 @ X122 )
| ( mxor @ X120 @ X121 @ X122 ) )
& ( ~ ( mforall_ind @ X123 @ X124 )
| ( X123 @ X125 @ X124 ) )
& ( ~ ( X126 @ ( esk3_2 @ X126 @ X127 ) @ X127 )
| ( mforall_ind @ X126 @ X127 ) )
& ( ~ ( mforall_prop @ X129 @ X130 )
| ( X129 @ X131 @ X130 ) )
& ( ~ ( X132 @ ( epred1_2 @ X132 @ X133 ) @ X133 )
| ( mforall_prop @ X132 @ X133 ) )
& ( ~ ( mexists_ind @ X135 @ X136 )
| ( X135 @ ( esk4_2 @ X135 @ X136 ) @ X136 ) )
& ( ~ ( X138 @ X140 @ X139 )
| ( mexists_ind @ X138 @ X139 ) )
& ( ~ ( mexists_prop @ X141 @ X142 )
| ( X141 @ ( epred2_2 @ X141 @ X142 ) @ X142 ) )
& ( ~ ( X144 @ X146 @ X145 )
| ( mexists_prop @ X144 @ X145 ) )
& ( ~ ( mbox @ X147 @ X148 @ X149 )
| ~ ( X147 @ X149 @ X150 )
| ( X148 @ X150 ) )
& ( ( X151 @ X153 @ ( esk5_3 @ X151 @ X152 @ X153 ) )
| ( mbox @ X151 @ X152 @ X153 ) )
& ( ~ ( X152 @ ( esk5_3 @ X151 @ X152 @ X153 ) )
| ( mbox @ X151 @ X152 @ X153 ) )
& ( ( X155 @ X157 @ ( esk6_3 @ X155 @ X156 @ X157 ) )
| ~ ( mdia @ X155 @ X156 @ X157 ) )
& ( ( X156 @ ( esk6_3 @ X155 @ X156 @ X157 ) )
| ~ ( mdia @ X155 @ X156 @ X157 ) )
& ( ~ ( X159 @ X161 @ X162 )
| ~ ( X160 @ X162 )
| ( mdia @ X159 @ X160 @ X161 ) )
& ( ~ ( mreflexive @ X163 )
| ( X163 @ X164 @ X164 ) )
& ( ~ ( X165 @ ( esk7_1 @ X165 ) @ ( esk7_1 @ X165 ) )
| ( mreflexive @ X165 ) )
& ( ~ ( msymmetric @ X167 )
| ~ ( X167 @ X168 @ X169 )
| ( X167 @ X169 @ X168 ) )
& ( ( X170 @ ( esk8_1 @ X170 ) @ ( esk9_1 @ X170 ) )
| ( msymmetric @ X170 ) )
& ( ~ ( X170 @ ( esk9_1 @ X170 ) @ ( esk8_1 @ X170 ) )
| ( msymmetric @ X170 ) )
& ( ~ ( mserial @ X173 )
| ( X173 @ X174 @ ( esk10_2 @ X173 @ X174 ) ) )
& ( ~ ( X176 @ ( esk11_1 @ X176 ) @ X178 )
| ( mserial @ X176 ) )
& ( ~ ( mtransitive @ X179 )
| ~ ( X179 @ X180 @ X181 )
| ~ ( X179 @ X181 @ X182 )
| ( X179 @ X180 @ X182 ) )
& ( ( X183 @ ( esk12_1 @ X183 ) @ ( esk13_1 @ X183 ) )
| ( mtransitive @ X183 ) )
& ( ( X183 @ ( esk13_1 @ X183 ) @ ( esk14_1 @ X183 ) )
| ( mtransitive @ X183 ) )
& ( ~ ( X183 @ ( esk12_1 @ X183 ) @ ( esk14_1 @ X183 ) )
| ( mtransitive @ X183 ) )
& ( ~ ( meuclidean @ X187 )
| ~ ( X187 @ X188 @ X189 )
| ~ ( X187 @ X188 @ X190 )
| ( X187 @ X189 @ X190 ) )
& ( ( X191 @ ( esk15_1 @ X191 ) @ ( esk16_1 @ X191 ) )
| ( meuclidean @ X191 ) )
& ( ( X191 @ ( esk15_1 @ X191 ) @ ( esk17_1 @ X191 ) )
| ( meuclidean @ X191 ) )
& ( ~ ( X191 @ ( esk16_1 @ X191 ) @ ( esk17_1 @ X191 ) )
| ( meuclidean @ X191 ) )
& ( ~ ( mpartially_functional @ X195 )
| ~ ( X195 @ X196 @ X197 )
| ~ ( X195 @ X196 @ X198 )
| ( X197 = X198 ) )
& ( ( X199 @ ( esk18_1 @ X199 ) @ ( esk19_1 @ X199 ) )
| ( mpartially_functional @ X199 ) )
& ( ( X199 @ ( esk18_1 @ X199 ) @ ( esk20_1 @ X199 ) )
| ( mpartially_functional @ X199 ) )
& ( ( ( esk19_1 @ X199 )
!= ( esk20_1 @ X199 ) )
| ( mpartially_functional @ X199 ) )
& ( ( X203 @ X204 @ ( esk21_2 @ X203 @ X204 ) )
| ~ ( mfunctional @ X203 ) )
& ( ~ ( X203 @ X204 @ X206 )
| ( ( esk21_2 @ X203 @ X204 )
= X206 )
| ~ ( mfunctional @ X203 ) )
& ( ( X207 @ ( esk22_1 @ X207 ) @ ( esk23_2 @ X207 @ X209 ) )
| ~ ( X207 @ ( esk22_1 @ X207 ) @ X209 )
| ( mfunctional @ X207 ) )
& ( ( X209
!= ( esk23_2 @ X207 @ X209 ) )
| ~ ( X207 @ ( esk22_1 @ X207 ) @ X209 )
| ( mfunctional @ X207 ) )
& ( ( X211 @ X212 @ ( esk24_3 @ X211 @ X212 @ X213 ) )
| ~ ( X211 @ X212 @ X213 )
| ~ ( mweakly_dense @ X211 ) )
& ( ( X211 @ ( esk24_3 @ X211 @ X212 @ X213 ) @ X213 )
| ~ ( X211 @ X212 @ X213 )
| ~ ( mweakly_dense @ X211 ) )
& ( ( X215 @ ( esk25_1 @ X215 ) @ ( esk26_1 @ X215 ) )
| ( mweakly_dense @ X215 ) )
& ( ~ ( X215 @ ( esk25_1 @ X215 ) @ X218 )
| ~ ( X215 @ X218 @ ( esk26_1 @ X215 ) )
| ( mweakly_dense @ X215 ) )
& ( ~ ( mweakly_connected @ X219 )
| ~ ( X219 @ X220 @ X221 )
| ~ ( X219 @ X220 @ X222 )
| ( X219 @ X221 @ X222 )
| ( X221 = X222 )
| ( X219 @ X222 @ X221 ) )
& ( ( X223 @ ( esk27_1 @ X223 ) @ ( esk28_1 @ X223 ) )
| ( mweakly_connected @ X223 ) )
& ( ( X223 @ ( esk27_1 @ X223 ) @ ( esk29_1 @ X223 ) )
| ( mweakly_connected @ X223 ) )
& ( ~ ( X223 @ ( esk28_1 @ X223 ) @ ( esk29_1 @ X223 ) )
| ( mweakly_connected @ X223 ) )
& ( ( ( esk28_1 @ X223 )
!= ( esk29_1 @ X223 ) )
| ( mweakly_connected @ X223 ) )
& ( ~ ( X223 @ ( esk29_1 @ X223 ) @ ( esk28_1 @ X223 ) )
| ( mweakly_connected @ X223 ) )
& ( ( X227 @ X229 @ ( esk30_4 @ X227 @ X228 @ X229 @ X230 ) )
| ~ ( X227 @ X228 @ X229 )
| ~ ( X227 @ X228 @ X230 )
| ~ ( mweakly_directed @ X227 ) )
& ( ( X227 @ X230 @ ( esk30_4 @ X227 @ X228 @ X229 @ X230 ) )
| ~ ( X227 @ X228 @ X229 )
| ~ ( X227 @ X228 @ X230 )
| ~ ( mweakly_directed @ X227 ) )
& ( ( X232 @ ( esk31_1 @ X232 ) @ ( esk32_1 @ X232 ) )
| ( mweakly_directed @ X232 ) )
& ( ( X232 @ ( esk31_1 @ X232 ) @ ( esk33_1 @ X232 ) )
| ( mweakly_directed @ X232 ) )
& ( ~ ( X232 @ ( esk32_1 @ X232 ) @ X236 )
| ~ ( X232 @ ( esk33_1 @ X232 ) @ X236 )
| ( mweakly_directed @ X232 ) )
& ( ~ ( mvalid @ X237 )
| ( X237 @ X238 ) )
& ( ~ ( X239 @ ( esk34_1 @ X239 ) )
| ( mvalid @ X239 ) )
& ( ~ ( minvalid @ X241 )
| ~ ( X241 @ X242 ) )
& ( ( X243 @ ( esk35_1 @ X243 ) )
| ( minvalid @ X243 ) )
& ( ~ ( msatisfiable @ X245 )
| ( X245 @ ( esk36_1 @ X245 ) ) )
& ( ~ ( X247 @ X248 )
| ( msatisfiable @ X247 ) )
& ( ~ ( mcountersatisfiable @ X249 )
| ~ ( X249 @ ( esk37_1 @ X249 ) ) )
& ( ( X251 @ X252 )
| ( mcountersatisfiable @ X251 ) )
& ( meq_ind @ ( d2mu @ d_mu_0 ) @ ( d2mu @ d_mu_0 ) @ ( d2unsorted @ d_unsorted_0 ) )
& ( mtrue @ ( d2unsorted @ d_unsorted_0 ) )
& ~ ( mfalse @ ( d2unsorted @ d_unsorted_0 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])])])])]) ).
thf(c_0_5,negated_conjecture,
~ ! [X88: $i > $o,X89: $i > $o] :
( ( mequiv @ X88 @ X89 )
= ( mand @ ( mimplies @ X88 @ X89 ) @ ( mimplies @ X89 @ X88 ) ) ),
inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_3])]) ).
thf(c_0_6,plain,
! [X1: $i] :
( X1
= ( d2unsorted @ ( esk1_1 @ X1 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_7,plain,
! [X2: d_unsorted] : ( X2 = d_unsorted_0 ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_8,negated_conjecture,
( ( mequiv @ epred3_0 @ epred4_0 )
!= ( mand @ ( mimplies @ epred3_0 @ epred4_0 ) @ ( mimplies @ epred4_0 @ epred3_0 ) ) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])]) ).
thf(c_0_9,plain,
! [X9: $i > $o] :
( ~ ( mcountersatisfiable @ X9 )
| ~ ( X9 @ ( esk37_1 @ X9 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_10,plain,
! [X1: $i] :
( ( d2unsorted @ d_unsorted_0 )
= X1 ),
inference(rw,[status(thm)],[c_0_6,c_0_7]) ).
thf(c_0_11,negated_conjecture,
( ( mequiv @ epred3_0 @ epred4_0 )
!= ( mand @ ( mimplies @ epred3_0 @ epred4_0 ) @ ( mimplies @ epred4_0 @ epred3_0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
thf(c_0_12,plain,
! [X9: $i > $o] :
( ~ ( mcountersatisfiable @ X9 )
| ~ ( X9 @ esk38_0 ) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_9,c_0_10]),c_0_10]) ).
thf(c_0_13,plain,
! [X1: $i,X9: $i > $o] :
( ( X9 @ X1 )
| ( mcountersatisfiable @ X9 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_14,plain,
! [X1: $i] : ( esk38_0 = X1 ),
inference(rw,[status(thm)],[c_0_10,c_0_10]) ).
thf(c_0_15,negated_conjecture,
( ( mand @ ( mimplies @ epred3_0 @ epred4_0 ) @ ( mimplies @ epred4_0 @ epred3_0 ) @ esk5_0 )
<~> ( mequiv @ epred3_0 @ epred4_0 @ esk5_0 ) ),
inference(neg_ext,[status(thm)],[c_0_11]) ).
thf(c_0_16,plain,
! [X1: $i,X9: $i > $o] :
( ( X9 @ X1 )
| ~ ( X9 @ esk38_0 ) ),
inference(spm,[status(thm)],[c_0_12,c_0_13]) ).
thf(c_0_17,plain,
! [X1: $i,X11: $i] : ( X1 = X11 ),
inference(spm,[status(thm)],[c_0_14,c_0_14]) ).
thf(c_0_18,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( X9 @ X1 )
| ~ ( mand @ X9 @ X10 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_19,negated_conjecture,
( ( mand @ ( mimplies @ epred3_0 @ epred4_0 ) @ ( mimplies @ epred4_0 @ epred3_0 ) @ esk5_0 )
| ( mequiv @ epred3_0 @ epred4_0 @ esk5_0 ) ),
inference(dynamic_cnf,[status(thm)],[c_0_15]) ).
thf(c_0_20,plain,
! [X1: $i,X9: $i > $o,X11: $i] :
( ( X9 @ X1 )
| ~ ( X9 @ X11 ) ),
inference(spm,[status(thm)],[c_0_16,c_0_17]) ).
thf(c_0_21,negated_conjecture,
( ( mequiv @ epred3_0 @ epred4_0 @ esk5_0 )
| ( mimplies @ epred3_0 @ epred4_0 @ esk5_0 ) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
thf(c_0_22,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( X9 @ X1 )
| ( mimplies @ X9 @ X10 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_23,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( mimplies @ X10 @ X9 @ X1 )
| ~ ( X9 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_24,negated_conjecture,
( ~ ( mand @ ( mimplies @ epred3_0 @ epred4_0 ) @ ( mimplies @ epred4_0 @ epred3_0 ) @ esk5_0 )
| ~ ( mequiv @ epred3_0 @ epred4_0 @ esk5_0 ) ),
inference(dynamic_cnf,[status(thm)],[c_0_15]) ).
thf(c_0_25,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( X10 @ X1 )
| ~ ( X9 @ X1 )
| ~ ( mequiv @ X9 @ X10 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_26,negated_conjecture,
! [X1: $i] :
( ( mimplies @ epred3_0 @ epred4_0 @ esk5_0 )
| ( mequiv @ epred3_0 @ epred4_0 @ X1 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
thf(c_0_27,plain,
! [X1: $i,X9: $i > $o,X10: $i > $o,X11: $i] :
( ( mimplies @ X9 @ X10 @ X1 )
| ( X9 @ X11 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_22]) ).
thf(c_0_28,plain,
! [X1: $i,X9: $i > $o,X10: $i > $o,X11: $i] :
( ( mimplies @ X9 @ X10 @ X1 )
| ~ ( X10 @ X11 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_23]) ).
thf(c_0_29,negated_conjecture,
! [X1: $i] :
( ~ ( mand @ ( mimplies @ epred3_0 @ epred4_0 ) @ ( mimplies @ epred4_0 @ epred3_0 ) @ X1 )
| ~ ( mequiv @ epred3_0 @ epred4_0 @ X1 ) ),
inference(spm,[status(thm)],[c_0_24,c_0_17]) ).
thf(c_0_30,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( mand @ X9 @ X10 @ X1 )
| ~ ( X9 @ X1 )
| ~ ( X10 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_31,negated_conjecture,
mimplies @ epred3_0 @ epred4_0 @ esk5_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_27]),c_0_28]) ).
thf(c_0_32,negated_conjecture,
! [X1: $i] :
( ~ ( mequiv @ epred3_0 @ epred4_0 @ X1 )
| ~ ( mimplies @ epred4_0 @ epred3_0 @ X1 )
| ~ ( mimplies @ epred3_0 @ epred4_0 @ X1 ) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
thf(c_0_33,negated_conjecture,
! [X1: $i] : ( mimplies @ epred3_0 @ epred4_0 @ X1 ),
inference(spm,[status(thm)],[c_0_20,c_0_31]) ).
thf(c_0_34,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( X10 @ X1 )
| ~ ( mimplies @ X9 @ X10 @ X1 )
| ~ ( X9 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_35,negated_conjecture,
! [X1: $i] :
( ~ ( mequiv @ epred3_0 @ epred4_0 @ X1 )
| ~ ( mimplies @ epred4_0 @ epred3_0 @ X1 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32,c_0_33])]) ).
thf(c_0_36,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( mequiv @ X9 @ X10 @ X1 )
| ~ ( X9 @ X1 )
| ~ ( X10 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_37,negated_conjecture,
! [X1: $i] :
( ( epred4_0 @ X1 )
| ~ ( epred3_0 @ X1 ) ),
inference(spm,[status(thm)],[c_0_34,c_0_33]) ).
thf(c_0_38,negated_conjecture,
! [X1: $i] :
( ~ ( mimplies @ epred4_0 @ epred3_0 @ X1 )
| ~ ( epred4_0 @ X1 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_34]) ).
thf(c_0_39,plain,
! [X1: $i,X9: $i > $o,X10: $i > $o] :
( ( mimplies @ X9 @ X10 @ X1 )
| ( mcountersatisfiable @ X10 ) ),
inference(spm,[status(thm)],[c_0_28,c_0_13]) ).
thf(c_0_40,negated_conjecture,
! [X1: $i,X11: $i] :
( ( epred4_0 @ X1 )
| ~ ( epred3_0 @ X11 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_37]) ).
thf(c_0_41,negated_conjecture,
! [X1: $i] :
( ( mcountersatisfiable @ epred3_0 )
| ~ ( epred4_0 @ X1 ) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
thf(c_0_42,negated_conjecture,
mcountersatisfiable @ epred3_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_13]),c_0_41]) ).
thf(c_0_43,negated_conjecture,
~ ( epred3_0 @ esk38_0 ),
inference(spm,[status(thm)],[c_0_12,c_0_42]) ).
thf(c_0_44,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( X9 @ X1 )
| ~ ( mand @ X10 @ X9 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_45,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( X9 @ X1 )
| ( X10 @ X1 )
| ( mequiv @ X10 @ X9 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_46,negated_conjecture,
! [X1: $i] :
~ ( epred3_0 @ X1 ),
inference(spm,[status(thm)],[c_0_43,c_0_17]) ).
thf(c_0_47,negated_conjecture,
( ( mequiv @ epred3_0 @ epred4_0 @ esk5_0 )
| ( mimplies @ epred4_0 @ epred3_0 @ esk5_0 ) ),
inference(spm,[status(thm)],[c_0_44,c_0_19]) ).
thf(c_0_48,negated_conjecture,
! [X1: $i] : ( epred4_0 @ X1 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_45]),c_0_46]),c_0_27]) ).
thf(c_0_49,negated_conjecture,
! [X1: $i] :
( ( mimplies @ epred4_0 @ epred3_0 @ esk5_0 )
| ( mequiv @ epred3_0 @ epred4_0 @ X1 ) ),
inference(spm,[status(thm)],[c_0_20,c_0_47]) ).
thf(c_0_50,negated_conjecture,
! [X1: $i] :
~ ( mimplies @ epred4_0 @ epred3_0 @ X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38,c_0_48])]) ).
thf(c_0_51,plain,
! [X10: $i > $o,X9: $i > $o,X1: $i] :
( ( X10 @ X1 )
| ~ ( X9 @ X1 )
| ~ ( mequiv @ X10 @ X9 @ X1 ) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
thf(c_0_52,negated_conjecture,
! [X1: $i] : ( mequiv @ epred3_0 @ epred4_0 @ X1 ),
inference(sr,[status(thm)],[c_0_49,c_0_50]) ).
thf(c_0_53,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_52]),c_0_48])]),c_0_46]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX180^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.16 % Computer : n026.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Tue Sep 29 16:12:42 UTC 2026
% 0.08/0.16 % CPUTime :
% 0.08/0.16 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running higher-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.bxCrPn2Vv3/E---3.1_796576.p
% 0.39/0.32 % Version: 3.5.1-ho
% 0.39/0.32 % Preprocessing class: HSMSSMSSSSSNHHN.
% 0.39/0.32 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.39/0.32 % Starting new_ho_12 with 1200s (4) cores
% 0.39/0.32 % Starting sh3l with 600s (2) cores
% 0.39/0.32 % Starting ehoh_best5_lambda with 300s (1) cores
% 0.39/0.32 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.39/0.32 % sh3l with pid 796590 completed with status 9
% 0.39/0.32 % new_ho_12 with pid 796589 completed with status 0
% 0.39/0.32 % Result found by new_ho_12
% 0.39/0.32 % Preprocessing class: HSMSSMSSSSSNHHN.
% 0.39/0.32 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.39/0.32 % Starting new_ho_12 with 1200s (4) cores
% 0.39/0.32 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.39/0.32 % No SInE strategy applied
% 0.39/0.32 % Search class: HGHSM-FFMF31-SHHFFMBN
% 0.39/0.32 % partial match(2): HGHSS-FFMF11-SHHFFMBN
% 0.39/0.32 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.39/0.32 % Starting SubtermCWHack with 109s (1) cores
% 0.39/0.32 % Starting new_ho_12 with 121s (1) cores
% 0.39/0.32 % Starting ho_unfolding_1 with 109s (1) cores
% 0.39/0.32 % Starting ho_unfolding_4 with 109s (1) cores
% 0.39/0.32 % new_ho_12 with pid 796598 completed with status 0
% 0.39/0.32 % Result found by new_ho_12
% 0.39/0.32 % Preprocessing class: HSMSSMSSSSSNHHN.
% 0.39/0.32 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.39/0.32 % Starting new_ho_12 with 1200s (4) cores
% 0.39/0.32 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.39/0.32 % No SInE strategy applied
% 0.39/0.32 % Search class: HGHSM-FFMF31-SHHFFMBN
% 0.39/0.32 % partial match(2): HGHSS-FFMF11-SHHFFMBN
% 0.39/0.32 % Scheduled 7 strats onto 4 cores with 1200 seconds (1200 total)
% 0.39/0.32 % Starting SubtermCWHack with 109s (1) cores
% 0.39/0.32 % Starting new_ho_12 with 121s (1) cores
% 0.39/0.32 % Preprocessing time : 0.003 s
% 0.39/0.32 % Presaturation interreduction done
% 0.39/0.32
% 0.39/0.32 % Proof found!
% 0.39/0.32 % SZS status Theorem
% 0.39/0.32 % SZS output start CNFRefutation
% See solution above
% 0.39/0.32 % Parsed axioms : 41
% 0.39/0.32 % Removed by relevancy pruning/SinE : 0
% 0.39/0.32 % Initial clauses : 139
% 0.39/0.32 % Removed in clause preprocessing : 43
% 0.39/0.32 % Initial clauses in saturation : 96
% 0.39/0.32 % Processed clauses : 549
% 0.39/0.32 % ...of these trivial : 24
% 0.39/0.32 % ...subsumed : 74
% 0.39/0.32 % ...remaining for further processing : 451
% 0.39/0.32 % Other redundant clauses eliminated : 1
% 0.39/0.32 % Clauses deleted for lack of memory : 0
% 0.39/0.32 % Backward-subsumed : 82
% 0.39/0.32 % Backward-rewritten : 40
% 0.39/0.32 % Generated clauses : 3397
% 0.39/0.32 % ...of the previous two non-redundant : 3059
% 0.39/0.32 % ...aggressively subsumed : 0
% 0.39/0.32 % Contextual simplify-reflections : 14
% 0.39/0.32 % Paramodulations : 3391
% 0.39/0.32 % Factorizations : 0
% 0.39/0.32 % NegExts : 1
% 0.39/0.32 % Equation resolutions : 1
% 0.39/0.32 % Disequality decompositions : 0
% 0.39/0.32 % Total rewrite steps : 555
% 0.39/0.32 % ...of those cached : 359
% 0.39/0.32 % Propositional unsat checks : 0
% 0.39/0.32 % Propositional check models : 0
% 0.39/0.32 % Propositional check unsatisfiable : 0
% 0.39/0.32 % Propositional clauses : 0
% 0.39/0.32 % Propositional clauses after purity: 0
% 0.39/0.32 % Propositional unsat core size : 0
% 0.39/0.32 % Propositional preprocessing time : 0.000
% 0.39/0.32 % Propositional encoding time : 0.000
% 0.39/0.32 % Propositional solver time : 0.000
% 0.39/0.32 % Success case prop preproc time : 0.000
% 0.39/0.32 % Success case prop encoding time : 0.000
% 0.39/0.32 % Success case prop solver time : 0.000
% 0.39/0.32 % Current number of processed clauses : 244
% 0.39/0.32 % Positive orientable unit clauses : 100
% 0.39/0.32 % Positive unorientable unit clauses: 4
% 0.39/0.32 % Negative unit clauses : 27
% 0.39/0.32 % Non-unit-clauses : 113
% 0.39/0.32 % Current number of unprocessed clauses: 2463
% 0.39/0.32 % ...number of literals in the above : 4905
% 0.39/0.32 % Current number of archived formulas : 0
% 0.39/0.32 % Current number of archived clauses : 206
% 0.39/0.32 % Clause-clause subsumption calls (NU) : 14228
% 0.39/0.32 % Rec. Clause-clause subsumption calls : 12071
% 0.39/0.32 % Non-unit clause-clause subsumptions : 98
% 0.39/0.32 % Unit Clause-clause subsumption calls : 5404
% 0.39/0.32 % Rewrite failures with RHS unbound : 0
% 0.39/0.32 % BW rewrite match attempts : 390
% 0.39/0.32 % BW rewrite match successes : 45
% 0.39/0.32 % Condensation attempts : 0
% 0.39/0.32 % Condensation successes : 0
% 0.39/0.32 % Termbank termtop insertions : 43529
% 0.39/0.32 % Search garbage collected termcells : 2941
% 0.39/0.32
% 0.39/0.32 % -------------------------------------------------
% 0.39/0.32 % User time : 0.085 s
% 0.39/0.32 % System time : 0.007 s
% 0.39/0.32 % Total time : 0.091 s
% 0.39/0.32 % Maximum resident set size: 4220 pages
% 0.39/0.32
% 0.39/0.32 % -------------------------------------------------
% 0.39/0.32 % User time : 0.351 s
% 0.39/0.32 % System time : 0.042 s
% 0.39/0.32 % Total time : 0.393 s
% 0.39/0.32 % Maximum resident set size: 4864 pages
% 0.39/0.32 % E exiting
%------------------------------------------------------------------------------