%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP004_7 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n009.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 : Sun Sep 27 07:35:25 AM UTC 2026
% Result : Theorem 159.67s 79.32s
% Output : Refutation 159.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 12
% Syntax : Number of formulae : 72 ( 40 unt; 0 typ; 1 def)
% Number of atoms : 125 ( 66 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 752 ( 54 ~; 30 |; 4 &; 654 @)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Number of types : 6 ( 5 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 125 ( 0 ^; 124 !; 0 ?; 125 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% Comments :
%------------------------------------------------------------------------------
thf(tyop_2Emin_2Ebool_type,type,
tyop_2Emin_2Ebool: $tType ).
thf(tyop_2Emin_2Eind_type,type,
tyop_2Emin_2Eind: $tType ).
thf(tyop_2Enum_2Enum_type,type,
tyop_2Enum_2Enum: $tType ).
thf(tyop_2Eone_2Eone_type,type,
tyop_2Eone_2Eone: $tType ).
thf(skt1_type,type,
skt1: $tType ).
thf(p_decl,type,
p: tyop_2Emin_2Ebool > $o ).
thf(c_2Ebool_2EIN_2E2_decl,type,
c_2Ebool_2EIN_2E2:
!>[TA: $tType] : ( TA > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > tyop_2Emin_2Ebool ) ).
thf(c_2Epred__set_2ECHOICE_2E1_decl,type,
c_2Epred__set_2ECHOICE_2E1:
!>[TA: $tType] : ( ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > TA ) ).
thf(c_2Epred__set_2EDELETE_2E2_decl,type,
c_2Epred__set_2EDELETE_2E2:
!>[TA: $tType] : ( ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > TA > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) ) ).
thf(c_2Epred__set_2EDISJOINT_2E2_decl,type,
c_2Epred__set_2EDISJOINT_2E2:
!>[TA: $tType] : ( ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > tyop_2Emin_2Ebool ) ).
thf(c_2Epred__set_2EEMPTY_2E0_decl,type,
c_2Epred__set_2EEMPTY_2E0:
!>[TA: $tType] : ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) ).
thf(c_2Epred__set_2EINSERT_2E2_decl,type,
c_2Epred__set_2EINSERT_2E2:
!>[TA: $tType] : ( TA > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) ) ).
thf(c_2Epred__set_2EINTER_2E2_decl,type,
c_2Epred__set_2EINTER_2E2:
!>[TA: $tType] : ( ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) ) ).
thf(c_2Epred__set_2EREST_2E1_decl,type,
c_2Epred__set_2EREST_2E1:
!>[TA: $tType] : ( ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) ) ).
thf(c_2Epred__set_2ESUBSET_2E2_decl,type,
c_2Epred__set_2ESUBSET_2E2:
!>[TA: $tType] : ( ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > ( tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ) ) > tyop_2Emin_2Ebool ) ).
thf(sk1_decl,type,
sk1: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun ) ).
thf(sk1_def,definition,
( sk1
= ( @+[A: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun )] :
~ ( A @ ( A @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ) ) ) ).
thf(42,axiom,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( TA @ c_2Epred__set_2EREST_2E1 ) )
= ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( A @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EREST__DEF) ).
thf(396,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( TA @ c_2Epred__set_2EREST_2E1 ) )
= ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( A @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(397,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( TA @ c_2Epred__set_2EREST_2E1 ) )
= ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( A @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) ) ),
inference(cnf,[status(esa)],[396]) ).
thf(398,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( TA @ c_2Epred__set_2EREST_2E1 ) )
= ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( A @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) ) ),
inference(lifteq,[status(thm)],[397]) ).
thf(1,conjecture,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( A @ ( TA @ c_2Epred__set_2EREST_2E1 ) @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EREST__SUBSET) ).
thf(2,negated_conjecture,
~ ! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( A @ ( TA @ c_2Epred__set_2EREST_2E1 ) @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(206,plain,
~ ! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( A @ ( TA @ c_2Epred__set_2EREST_2E1 ) @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(207,plain,
~ ( sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(cnf,[status(esa)],[206]) ).
thf(70890,plain,
! [A: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun )] :
( ( ( A @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) )
!= ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) ) )
| ~ ( sk1 @ ( A @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( A @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ) ),
inference(paramod_ordered,[status(thm)],[398,207]) ).
thf(70891,plain,
~ ( sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(pattern_uni,[status(thm)],[70890:[bind(A,$thf( sk1 ))]]) ).
thf(26,axiom,
! [TA: $tType,A: TA,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),C: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( C @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) @ ( B @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) )
= ( C @ ( A @ ( B @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2ESUBSET__INSERT__DELETE) ).
thf(305,plain,
! [TA: $tType,A: TA,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),C: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( C @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) @ ( B @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) )
= ( C @ ( A @ ( B @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(306,plain,
! [TA: $tType,C: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: TA] :
( ( C @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) @ ( B @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) )
= ( C @ ( A @ ( B @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) ) ),
inference(cnf,[status(esa)],[305]) ).
thf(307,plain,
! [TA: $tType,C: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: TA] :
( ( C @ ( A @ ( B @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) )
= ( C @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) @ ( B @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) ) ),
inference(lifteq,[status(thm)],[306]) ).
thf(85683,plain,
~ ( sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( skt1 @ c_2Epred__set_2EINSERT_2E2 ) ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(rewrite,[status(thm)],[70891,307]) ).
thf(53,axiom,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) )
=> ( A @ ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2ECHOICE__DEF) ).
thf(443,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) )
=> ( A @ ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(444,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p )
| ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(cnf,[status(esa)],[443]) ).
thf(445,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( A @ ( TA @ c_2Epred__set_2ECHOICE_2E1 ) @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p )
| ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(lifteq,[status(thm)],[444]) ).
thf(80,axiom,
! [TA: $tType,A: TA] :
( ( A @ ( TA @ c_2Epred__set_2EEMPTY_2E0 @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EEMPTY__DELETE) ).
thf(553,plain,
! [TA: $tType,A: TA] :
( ( A @ ( TA @ c_2Epred__set_2EEMPTY_2E0 @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(554,plain,
! [TA: $tType,A: TA] :
( ( A @ ( TA @ c_2Epred__set_2EEMPTY_2E0 @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ),
inference(cnf,[status(esa)],[553]) ).
thf(555,plain,
! [TA: $tType,A: TA] :
( ( A @ ( TA @ c_2Epred__set_2EEMPTY_2E0 @ ( TA @ c_2Epred__set_2EDELETE_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ),
inference(lifteq,[status(thm)],[554]) ).
thf(3,axiom,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EINTER__IDEMPOT) ).
thf(208,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(209,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= A ),
inference(cnf,[status(esa)],[208]) ).
thf(210,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= A ),
inference(lifteq,[status(thm)],[209]) ).
thf(27,axiom,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
<=> ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EDISJOINT__DEF) ).
thf(308,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) )
=> ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) )
& ( ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
=> ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(309,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) )
& ( ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) )
| ~ ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) ) ),
inference(cnf,[status(esa)],[308]) ).
thf(311,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(cnfConj,[status(thm)],[309]) ).
thf(313,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(lifteq,[status(thm)],[311]) ).
thf(19,axiom,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
<=> ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EDISJOINT__EMPTY__REFL__RWT) ).
thf(267,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) )
=> ( A @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) )
& ( ( A @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
=> ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(268,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( ( A @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
| ( A
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) )
& ( ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) )
| ~ ( A @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) ) ),
inference(cnf,[status(esa)],[267]) ).
thf(269,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) )
| ~ ( A @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) ),
inference(cnfConj,[status(thm)],[268]) ).
thf(271,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ~ ( A @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
| ( A
= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(lifteq,[status(thm)],[269]) ).
thf(9621,plain,
! [A: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun )] :
( ( A
!= ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) ) )
| ~ ( sk1 @ ( skt1 @ c_2Epred__set_2EEMPTY_2E0 @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p )
| ~ ( A @ ( A @ ( skt1 @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) ),
inference(paramod_ordered,[status(thm)],[271,207]) ).
thf(9622,plain,
( ~ ( sk1 @ ( skt1 @ c_2Epred__set_2EEMPTY_2E0 @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p )
| ~ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) ),
inference(pattern_uni,[status(thm)],[9621:[bind(A,$thf( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) ))]]) ).
thf(132,axiom,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( TA @ c_2Epred__set_2EEMPTY_2E0 @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EEMPTY__SUBSET) ).
thf(861,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( TA @ c_2Epred__set_2EEMPTY_2E0 @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(862,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( TA @ c_2Epred__set_2EEMPTY_2E0 @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(cnf,[status(esa)],[861]) ).
thf(18451,plain,
( ~ $true
| ~ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) ),
inference(rewrite,[status(thm)],[9622,862]) ).
thf(18452,plain,
~ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ),
inference(simp,[status(thm)],[18451]) ).
thf(28558,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
!= ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) )
| ~ $true
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(paramod_ordered,[status(thm)],[313,18452]) ).
thf(28559,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( ( B @ ( A @ ( TA @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p )
!= ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2EDISJOINT_2E2 ) ) @ p ) )
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINTER_2E2 ) ) )
!= ( TA @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(simp,[status(thm)],[28558]) ).
thf(28560,plain,
( ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2EINTER_2E2 ) ) )
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ),
inference(pattern_uni,[status(thm)],[28559:[bind(A,$thf( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) )),bind(B,$thf( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) )),bind_type(TA,$thf( skt1 ))]]) ).
thf(29323,plain,
! [A: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun )] :
( ( ( A @ ( A @ ( skt1 @ c_2Epred__set_2EINTER_2E2 ) ) )
!= ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) @ ( skt1 @ c_2Epred__set_2EINTER_2E2 ) ) ) )
| ( A
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(paramod_ordered,[status(thm)],[210,28560]) ).
thf(29324,plain,
( ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) )
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ),
inference(pattern_uni,[status(thm)],[29323:[bind(A,$thf( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) ))]]) ).
thf(70734,plain,
! [A: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun )] :
( ( ( A @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) )
!= ( sk1 @ ( skt1 @ c_2Epred__set_2EREST_2E1 ) ) )
| ( ( A @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( A @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) )
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(paramod_ordered,[status(thm)],[398,29324]) ).
thf(70735,plain,
( ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) )
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ),
inference(pattern_uni,[status(thm)],[70734:[bind(A,$thf( sk1 ))]]) ).
thf(70975,plain,
! [A: skt1] :
( ( ( A @ ( skt1 @ c_2Epred__set_2EEMPTY_2E0 @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) )
!= ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) ) )
| ( ( skt1 @ c_2Epred__set_2EEMPTY_2E0 )
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(paramod_ordered,[status(thm)],[555,70735]) ).
thf(70976,plain,
! [A: skt1] :
( ( A @ ( skt1 @ c_2Epred__set_2EEMPTY_2E0 @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) )
!= ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( sk1 @ ( skt1 @ c_2Epred__set_2EDELETE_2E2 ) ) ) ),
inference(simp,[status(thm)],[70975]) ).
thf(71105,plain,
! [A: skt1] :
( ( A
!= ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) ) )
| ( sk1
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ) ),
inference(simp,[status(thm)],[70976]) ).
thf(71131,plain,
( sk1
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) ),
inference(simp,[status(thm)],[71105]) ).
thf(88688,plain,
! [A: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun )] :
( ( A != sk1 )
| ( ( skt1 @ c_2Epred__set_2EEMPTY_2E0 )
!= ( skt1 @ c_2Epred__set_2EEMPTY_2E0 ) )
| ( A @ ( A @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( skt1 @ c_2Ebool_2EIN_2E2 ) ) @ p ) ),
inference(paramod_ordered,[status(thm)],[445,71131]) ).
thf(88689,plain,
! [A: tyop_2Emin_2Ebool @ ( skt1 @ tyop_2Emin_2Efun )] :
( ( A != sk1 )
| ( A @ ( A @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( skt1 @ c_2Ebool_2EIN_2E2 ) ) @ p ) ),
inference(simp,[status(thm)],[88688]) ).
thf(88690,plain,
sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( skt1 @ c_2Ebool_2EIN_2E2 ) ) @ p,
inference(pattern_uni,[status(thm)],[88689:[bind(A,$thf( sk1 ))]]) ).
thf(31,axiom,
! [TA: $tType,A: TA,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( B @ ( A @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p )
=> ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) )
= B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2EABSORPTION__RWT) ).
thf(342,plain,
! [TA: $tType,A: TA,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] :
( ( B @ ( A @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p )
=> ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(343,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: TA] :
( ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) )
= B )
| ~ ( B @ ( A @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p ) ),
inference(cnf,[status(esa)],[342]) ).
thf(344,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: TA] :
( ~ ( B @ ( A @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p )
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) )
= B ) ),
inference(lifteq,[status(thm)],[343]) ).
thf(90574,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: TA] :
( ( ( sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( skt1 @ c_2Ebool_2EIN_2E2 ) ) @ p )
!= ( B @ ( A @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p ) )
| ~ $true
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[88690,344]) ).
thf(90575,plain,
! [TA: $tType,B: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun ),A: TA] :
( ( ( sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( skt1 @ c_2Ebool_2EIN_2E2 ) ) @ p )
!= ( B @ ( A @ ( TA @ c_2Ebool_2EIN_2E2 ) ) @ p ) )
| ( ( B @ ( A @ ( TA @ c_2Epred__set_2EINSERT_2E2 ) ) )
= B ) ),
inference(simp,[status(thm)],[90574]) ).
thf(90576,plain,
( ( sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) @ ( skt1 @ c_2Epred__set_2EINSERT_2E2 ) ) )
= sk1 ),
inference(pattern_uni,[status(thm)],[90575:[bind(A,$thf( sk1 @ ( skt1 @ c_2Epred__set_2ECHOICE_2E1 ) )),bind(B,$thf( sk1 )),bind_type(TA,$thf( skt1 ))]]) ).
thf(90990,plain,
~ ( sk1 @ ( sk1 @ ( skt1 @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(rewrite,[status(thm)],[85683,90576]) ).
thf(107,axiom,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( A @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epred__set_2ESUBSET__REFL) ).
thf(716,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( A @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(717,plain,
! [TA: $tType,A: tyop_2Emin_2Ebool @ ( TA @ tyop_2Emin_2Efun )] : ( A @ ( A @ ( TA @ c_2Epred__set_2ESUBSET_2E2 ) ) @ p ),
inference(cnf,[status(esa)],[716]) ).
thf(91524,plain,
~ $true,
inference(rewrite,[status(thm)],[90990,717]) ).
thf(91525,plain,
$false,
inference(simp,[status(thm)],[91524]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP004_7 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.13/0.40 % Computer : n009.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Fri Sep 25 17:03:15 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.83/0.97 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 4.43/2.00 % [INFO] Parsing done (1023ms).
% 4.43/2.02 % [INFO] Running in sequential loop mode.
% 5.81/2.38 % [INFO] eprover registered as external prover.
% 5.81/2.39 % [INFO] Scanning for conjecture ...
% 7.45/2.88 % [INFO] Found a conjecture (or negated_conjecture) and 3173 axioms. Running axiom selection ...
% 8.43/3.08 % [INFO] Axiom selection finished. Selected 203 axioms (removed 2970 axioms).
% 9.20/3.27 % [INFO] Problem is typed first-order (TPTP TFF).
% 9.20/3.29 % [INFO] Type checking passed.
% 9.20/3.30 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 159.67/79.31 % [INFO] Killing All external provers ...
% 159.67/79.31 % Time passed: 78766ms (effective reasoning time: 77287ms)
% 159.67/79.31 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 159.67/79.32 % Axioms used in derivation (10): thm_2Epred__set_2EREST__DEF, thm_2Epred__set_2EABSORPTION__RWT, thm_2Epred__set_2ECHOICE__DEF, thm_2Epred__set_2EEMPTY__DELETE, thm_2Epred__set_2EINTER__IDEMPOT, thm_2Epred__set_2ESUBSET__INSERT__DELETE, thm_2Epred__set_2ESUBSET__REFL, thm_2Epred__set_2EDISJOINT__DEF, thm_2Epred__set_2EDISJOINT__EMPTY__REFL__RWT, thm_2Epred__set_2EEMPTY__SUBSET
% 159.67/79.32 % No. of inferences in proof: 71
% 159.67/79.32 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 78766 ms resp. 77287 ms w/o parsing
% 159.67/79.37 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 159.67/79.37 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------