%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV453^1 : TPTP v9.3.1. Released v7.0.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 : n004.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:37:19 AM UTC 2026
% Result : Theorem 93.00s 41.09s
% Output : Refutation 93.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 5
% Syntax : Number of formulae : 70 ( 34 unt; 0 typ; 1 def)
% Number of atoms : 334 ( 65 equ; 0 cnn)
% Maximal formula atoms : 7 ( 4 avg)
% Number of connectives : 779 ( 62 ~; 52 |; 18 &; 647 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 118 ( 118 >; 0 *; 0 +; 0 <<)
% Number of symbols : 9 ( 5 usr; 4 con; 0-4 aty)
% Number of variables : 277 ( 66 ^; 210 !; 0 ?; 277 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% Comments :
%------------------------------------------------------------------------------
thf(skt1_type,type,
skt1: $tType ).
thf('const/sets/UNIV_decl',type,
'const/sets/UNIV':
!>[TA: $tType] : ( TA > $o ) ).
thf('const/sets/INTER_decl',type,
'const/sets/INTER':
!>[TA: $tType] : ( ( TA > $o ) > ( TA > $o ) > TA > $o ) ).
thf('const/sets/IN_decl',type,
'const/sets/IN':
!>[TA: $tType] : ( TA > ( TA > $o ) > $o ) ).
thf(sk1_decl,type,
sk1: skt1 > $o ).
thf(sk3_decl,type,
sk3: skt1 ).
thf(sk1_def,definition,
( sk1
= ( @+[A: skt1 > $o] :
( ( 'const/sets/INTER' @ skt1 @ A @ ( 'const/sets/UNIV' @ skt1 ) )
!= A ) ) ) ).
thf(3,axiom,
! [TA: $tType,A: TA > $o,B: TA] :
( ( 'const/sets/IN' @ TA @ B @ A )
= ( A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/IN_') ).
thf(10,plain,
! [TA: $tType,A: TA > $o,B: TA] :
( ( 'const/sets/IN' @ TA @ B @ A )
= ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(11,plain,
! [TA: $tType,B: TA,A: TA > $o] :
( ( 'const/sets/IN' @ TA @ B @ A )
= ( A @ B ) ),
inference(cnf,[status(esa)],[10]) ).
thf(12,plain,
! [TA: $tType,B: TA,A: TA > $o] :
( ( 'const/sets/IN' @ TA @ B @ A )
= ( A @ B ) ),
inference(lifteq,[status(thm)],[11]) ).
thf(25,plain,
! [TA: $tType,B: TA,A: TA > $o] :
( ( 'const/sets/IN' @ TA @ B @ A )
| ~ ( A @ B ) ),
inference(bool_ext,[status(thm)],[12]) ).
thf(4,axiom,
! [TA: $tType,A: TA] : ( 'const/sets/IN' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/IN_UNIV_') ).
thf(13,plain,
! [TA: $tType,A: TA] : ( 'const/sets/IN' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(14,plain,
! [TA: $tType,A: TA] : ( 'const/sets/IN' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) ),
inference(cnf,[status(esa)],[13]) ).
thf(5,axiom,
! [TA: $tType,A: TA > $o,B: TA > $o,C: TA] :
( ( 'const/sets/IN' @ TA @ C @ ( 'const/sets/INTER' @ TA @ A @ B ) )
= ( ( 'const/sets/IN' @ TA @ C @ A )
& ( 'const/sets/IN' @ TA @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/IN_INTER_') ).
thf(15,plain,
! [TA: $tType,A: TA > $o,B: TA > $o,C: TA] :
( ( 'const/sets/IN' @ TA @ C @ ( 'const/sets/INTER' @ TA @ A @ B ) )
= ( ( 'const/sets/IN' @ TA @ C @ A )
& ( 'const/sets/IN' @ TA @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(16,plain,
! [TA: $tType,C: TA,B: TA > $o,A: TA > $o] :
( ( 'const/sets/IN' @ TA @ C @ ( 'const/sets/INTER' @ TA @ A @ B ) )
= ( ( 'const/sets/IN' @ TA @ C @ A )
& ( 'const/sets/IN' @ TA @ C @ B ) ) ),
inference(cnf,[status(esa)],[15]) ).
thf(17,plain,
! [TA: $tType,C: TA,B: TA > $o,A: TA > $o] :
( ( 'const/sets/IN' @ TA @ C @ ( 'const/sets/INTER' @ TA @ A @ B ) )
= ( ( 'const/sets/IN' @ TA @ C @ A )
& ( 'const/sets/IN' @ TA @ C @ B ) ) ),
inference(lifteq,[status(thm)],[16]) ).
thf(124,plain,
! [TA: $tType,TB: $tType,D: TB,C: TB > $o,B: TB > $o,A: TA] :
( ( ( ( 'const/sets/IN' @ TB @ D @ B )
& $true )
= ( 'const/sets/IN' @ TB @ D @ ( 'const/sets/INTER' @ TB @ B @ C ) ) )
| ( ( 'const/sets/IN' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) )
!= ( 'const/sets/IN' @ TB @ D @ C ) ) ),
inference(paramod_ordered,[status(thm)],[14,17]) ).
thf(125,plain,
! [TA: $tType,TB: $tType,D: TB,C: TB > $o,B: TB > $o,A: TA] :
( ( ( 'const/sets/IN' @ TB @ D @ B )
= ( 'const/sets/IN' @ TB @ D @ ( 'const/sets/INTER' @ TB @ B @ C ) ) )
| ( ( 'const/sets/IN' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) )
!= ( 'const/sets/IN' @ TB @ D @ C ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(126,plain,
! [TB: $tType,B: TB > $o,A: TB] :
( ( 'const/sets/IN' @ TB @ A @ B )
= ( 'const/sets/IN' @ TB @ A @ ( 'const/sets/INTER' @ TB @ B @ ( 'const/sets/UNIV' @ TB ) ) ) ),
inference(pattern_uni,[status(thm)],[125:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( 'const/sets/UNIV' @ TB )),bind(D,$thf( A )),bind_type(TA,$thf( TB ))]]) ).
thf(177,plain,
! [TA: $tType,B: TA > $o,A: TA] :
( ( 'const/sets/IN' @ TA @ A @ B )
= ( 'const/sets/IN' @ TA @ A @ ( 'const/sets/INTER' @ TA @ B @ ( 'const/sets/UNIV' @ TA ) ) ) ),
inference(simp,[status(thm)],[126]) ).
thf(31,plain,
! [TA: $tType,TB: $tType,C: TB,B: TB > $o,A: TA] :
( ( B @ C )
| ( ( 'const/sets/IN' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) )
!= ( 'const/sets/IN' @ TB @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[14,12]) ).
thf(32,plain,
! [TB: $tType,A: TB] : ( 'const/sets/UNIV' @ TB @ A ),
inference(pattern_uni,[status(thm)],[31:[bind(A,$thf( A )),bind(B,$thf( 'const/sets/UNIV' @ TB )),bind(C,$thf( A )),bind_type(TA,$thf( TB ))]]) ).
thf(38,plain,
! [TA: $tType,A: TA] : ( 'const/sets/UNIV' @ TA @ A ),
inference(simp,[status(thm)],[32]) ).
thf(13576,plain,
! [TA: $tType,B: TA > $o,A: TA] :
( ( 'const/sets/IN' @ TA @ A @ B )
= ( 'const/sets/IN' @ TA @ A
@ ( 'const/sets/INTER' @ TA @ B
@ ^ [C: TA] : $true ) ) ),
inference(rewrite,[status(thm)],[177,38]) ).
thf(137,plain,
! [TA: $tType,TB: $tType,E: TB,D: TB > $o,C: TA,B: TA > $o,A: TA > $o] :
( ( ( ( 'const/sets/IN' @ TA @ C @ A )
& ( 'const/sets/IN' @ TA @ C @ B ) )
= ( 'const/sets/IN' @ TB @ E @ D ) )
| ( ( 'const/sets/IN' @ TA @ C @ ( 'const/sets/INTER' @ TA @ A @ B ) )
!= ( D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[17,12]) ).
thf(153,plain,
! [TA: $tType,TB: $tType,F: TB > TA > TA > $o,E: TB > TA > TA > $o,D: TB > TA,C: TB,B: TA > $o,A: TA > $o] :
( ( ( ( 'const/sets/IN' @ TA @ ( D @ C ) @ A )
& ( 'const/sets/IN' @ TA @ ( D @ C ) @ B ) )
= ( 'const/sets/IN' @ TB @ C
@ ^ [G: TB] :
( 'const/sets/IN' @ TA @ ( D @ G )
@ ^ [H: TA] : ( 'const/sets/INTER' @ TA @ ( E @ G @ H ) @ ( F @ G @ H ) @ H ) ) ) )
| ( ( ^ [G: TA] : A )
!= ( E @ C ) )
| ( ( ^ [G: TA] : B )
!= ( F @ C ) ) ),
inference(pre_uni,[status(thm)],[137:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( F @ E )),bind(D,$thf( ^ [I: TB] : ( 'const/sets/IN' @ TA @ ( F @ I ) @ ^ [J: TA] : ( 'const/sets/INTER' @ TA @ ( H @ I @ J ) @ ( I @ I @ J ) @ J ) ) )),bind(E,$thf( E ))]]) ).
thf(154,plain,
! [TA: $tType,TB: $tType,F: TB > TA > TA > $o,E: TB > TA > TA > $o,D: TB > TA,C: TB,B: TA > $o,A: TA > $o] :
( ( ( ( 'const/sets/IN' @ TA @ ( D @ C ) @ A )
& ( 'const/sets/IN' @ TA @ ( D @ C ) @ B ) )
= ( 'const/sets/IN' @ TB @ C
@ ^ [G: TB] :
( 'const/sets/IN' @ TA @ ( D @ G )
@ ^ [H: TA] : ( 'const/sets/INTER' @ TA @ ( E @ G @ H ) @ ( F @ G @ H ) @ H ) ) ) )
| ( ( ^ [G: TA] : A )
!= ( E @ C ) )
| ( ( ^ [G: TA] : B )
!= ( F @ C ) ) ),
inference(pre_uni,[status(thm)],[153:[]]) ).
thf(174,plain,
! [TA: $tType,TB: $tType,F: TB > TA > TA > $o,E: TB > TA > TA > $o,D: TB > TA,C: TB,B: TA > $o,A: TA > $o] :
( ( ( ( 'const/sets/IN' @ TA @ ( D @ C ) @ A )
& ( 'const/sets/IN' @ TA @ ( D @ C ) @ B ) )
= ( 'const/sets/IN' @ TB @ C
@ ^ [G: TB] :
( 'const/sets/IN' @ TA @ ( D @ G )
@ ^ [H: TA] : ( 'const/sets/INTER' @ TA @ ( E @ G @ H ) @ ( F @ G @ H ) @ H ) ) ) )
| ( ( ^ [G: TA] : A )
!= ( E @ C ) )
| ( ( ^ [G: TA] : B )
!= ( F @ C ) ) ),
inference(simp,[status(thm)],[154]) ).
thf(135,plain,
! [TA: $tType,TB: $tType,E: TB,D: TB > $o,C: TA,B: TA > $o,A: TA > $o] :
( ( ( ( 'const/sets/IN' @ TA @ C @ A )
& ( 'const/sets/IN' @ TA @ C @ B ) )
= ( D @ E ) )
| ( ( 'const/sets/IN' @ TA @ C @ ( 'const/sets/INTER' @ TA @ A @ B ) )
!= ( 'const/sets/IN' @ TB @ E @ D ) ) ),
inference(paramod_ordered,[status(thm)],[17,12]) ).
thf(136,plain,
! [TB: $tType,C: TB,B: TB > $o,A: TB > $o] :
( ( ( 'const/sets/IN' @ TB @ C @ A )
& ( 'const/sets/IN' @ TB @ C @ B ) )
= ( 'const/sets/INTER' @ TB @ A @ B @ C ) ),
inference(pattern_uni,[status(thm)],[135:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( 'const/sets/INTER' @ TB @ A @ B )),bind(E,$thf( C )),bind_type(TA,$thf( TB ))]]) ).
thf(165,plain,
! [TA: $tType,C: TA,B: TA > $o,A: TA > $o] :
( ( ( 'const/sets/IN' @ TA @ C @ A )
& ( 'const/sets/IN' @ TA @ C @ B ) )
= ( 'const/sets/INTER' @ TA @ A @ B @ C ) ),
inference(simp,[status(thm)],[136]) ).
thf(10322,plain,
! [TA: $tType,TB: $tType,F: TB > TA > TA > $o,E: TB > TA > TA > $o,D: TB > TA,C: TB,B: TA > $o,A: TA > $o] :
( ( ( 'const/sets/INTER' @ TA @ A @ B @ ( D @ C ) )
= ( 'const/sets/IN' @ TB @ C
@ ^ [G: TB] :
( 'const/sets/IN' @ TA @ ( D @ G )
@ ^ [H: TA] : ( 'const/sets/INTER' @ TA @ ( E @ G @ H ) @ ( F @ G @ H ) @ H ) ) ) )
| ( ( ^ [G: TA] : A )
!= ( E @ C ) )
| ( ( ^ [G: TA] : B )
!= ( F @ C ) ) ),
inference(rewrite,[status(thm)],[174,165]) ).
thf(1,conjecture,
! [TA: $tType,A: TA > $o] :
( ( 'const/sets/INTER' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/INTER_UNIV_1') ).
thf(2,negated_conjecture,
~ ! [TA: $tType,A: TA > $o] :
( ( 'const/sets/INTER' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) )
= A ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(7,plain,
~ ! [TA: $tType,A: TA > $o] :
( ( 'const/sets/INTER' @ TA @ A @ ( 'const/sets/UNIV' @ TA ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(8,plain,
( ( 'const/sets/INTER' @ skt1 @ sk1 @ ( 'const/sets/UNIV' @ skt1 ) )
!= sk1 ),
inference(cnf,[status(esa)],[7]) ).
thf(9,plain,
( ( 'const/sets/INTER' @ skt1 @ sk1 @ ( 'const/sets/UNIV' @ skt1 ) )
!= sk1 ),
inference(lifteq,[status(thm)],[8]) ).
thf(181,plain,
( ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true )
!= sk1 ),
inference(rewrite,[status(thm)],[9,38]) ).
thf(192,plain,
( ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true
@ sk3 )
!= ( sk1 @ sk3 ) ),
inference(func_ext,[status(esa)],[181]) ).
thf(269,plain,
( ~ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true
@ sk3 )
| ~ ( sk1 @ sk3 ) ),
inference(bool_ext,[status(thm)],[192]) ).
thf(270,plain,
( ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true
@ sk3 )
| ( sk1 @ sk3 ) ),
inference(bool_ext,[status(thm)],[192]) ).
thf(10417,plain,
! [TA: $tType,TB: $tType,F: TB > TA > TA > $o,E: TB > TA > TA > $o,D: TB > TA,C: TB,B: TA > $o,A: TA > $o] :
( ( ( ^ [G: TA] : A )
!= ( E @ C ) )
| ( ( ^ [G: TA] : B )
!= ( F @ C ) )
| ( 'const/sets/IN' @ TB @ C
@ ^ [G: TB] :
( 'const/sets/IN' @ TA @ ( D @ G )
@ ^ [H: TA] : ( 'const/sets/INTER' @ TA @ ( E @ G @ H ) @ ( F @ G @ H ) @ H ) ) )
| ( sk1 @ sk3 )
| ( ( 'const/sets/INTER' @ TA @ A @ B @ ( D @ C ) )
!= ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [G: skt1] : $true
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[10322,270]) ).
thf(10662,plain,
! [TB: $tType,C: TB > skt1 > skt1 > $o,B: TB > skt1 > skt1 > $o,A: TB] :
( ( ( ^ [D: skt1] : sk1 )
!= ( B @ A ) )
| ( ( ^ [D: skt1,E: skt1] : $true )
!= ( C @ A ) )
| ( 'const/sets/IN' @ TB @ A
@ ^ [D: TB] :
( 'const/sets/IN' @ skt1 @ sk3
@ ^ [E: skt1] : ( 'const/sets/INTER' @ skt1 @ ( B @ D @ E ) @ ( C @ D @ E ) @ E ) ) )
| ( sk1 @ sk3 ) ),
inference(pre_uni,[status(thm)],[10417:[bind(A,$thf( sk1 )),bind(B,$thf( ^ [G: skt1] : $true )),bind(C,$thf( C )),bind(D,$thf( ^ [G: TB] : sk3 )),bind_type(TA,$thf( skt1 ))]]) ).
thf(10663,plain,
! [TB: $tType,A: TB] :
( ( sk1 @ sk3 )
| ( 'const/sets/IN' @ TB @ A
@ ^ [B: TB] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [C: skt1] : $true ) ) ) ),
inference(pre_uni,[status(thm)],[10662:[bind(A,$thf( (@) )),bind(B,$thf( ^ [D: TB] : ^ [E: skt1] : sk1 )),bind(C,$thf( ^ [D: TB] : ^ [E: skt1] : ^ [F: skt1] : $true ))]]) ).
thf(10822,plain,
! [TA: $tType,A: TA] :
( ( sk1 @ sk3 )
| ( 'const/sets/IN' @ TA @ A
@ ^ [B: TA] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [C: skt1] : $true ) ) ) ),
inference(simp,[status(thm)],[10663]) ).
thf(24,plain,
! [TA: $tType,B: TA,A: TA > $o] :
( ~ ( 'const/sets/IN' @ TA @ B @ A )
| ( A @ B ) ),
inference(bool_ext,[status(thm)],[12]) ).
thf(13317,plain,
! [TA: $tType,TB: $tType,C: TB,B: TB > $o,A: TA] :
( ( sk1 @ sk3 )
| ~ $true
| ( B @ C )
| ( ( 'const/sets/IN' @ TA @ A
@ ^ [D: TA] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [E: skt1] : $true ) ) )
!= ( 'const/sets/IN' @ TB @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[10822,24]) ).
thf(13318,plain,
! [TA: $tType,TB: $tType,C: TB,B: TB > $o,A: TA] :
( ( sk1 @ sk3 )
| ( B @ C )
| ( ( 'const/sets/IN' @ TA @ A
@ ^ [D: TA] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [E: skt1] : $true ) ) )
!= ( 'const/sets/IN' @ TB @ C @ B ) ) ),
inference(simp,[status(thm)],[13317]) ).
thf(13319,plain,
( ( sk1 @ sk3 )
| ( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true ) ) ),
inference(pattern_uni,[status(thm)],[13318:[bind(A,$thf( A )),bind(B,$thf( ^ [D: TB] : ( 'const/sets/IN' @ skt1 @ sk3 @ ( 'const/sets/INTER' @ skt1 @ sk1 @ ^ [E: skt1] : $true ) ) )),bind(C,$thf( A )),bind_type(TA,$thf( TB ))]]) ).
thf(143,plain,
! [TA: $tType,TB: $tType,E: TB,D: TB > $o,C: TB > $o,B: TA,A: TA > $o] :
( ( ( ( A @ B )
& ( 'const/sets/IN' @ TB @ E @ D ) )
= ( 'const/sets/IN' @ TB @ E @ ( 'const/sets/INTER' @ TB @ C @ D ) ) )
| ( ( 'const/sets/IN' @ TA @ B @ A )
!= ( 'const/sets/IN' @ TB @ E @ C ) ) ),
inference(paramod_ordered,[status(thm)],[12,17]) ).
thf(144,plain,
! [TB: $tType,C: TB > $o,B: TB,A: TB > $o] :
( ( ( A @ B )
& ( 'const/sets/IN' @ TB @ B @ C ) )
= ( 'const/sets/IN' @ TB @ B @ ( 'const/sets/INTER' @ TB @ A @ C ) ) ),
inference(pattern_uni,[status(thm)],[143:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( D )),bind(E,$thf( B )),bind_type(TA,$thf( TB ))]]) ).
thf(168,plain,
! [TA: $tType,C: TA > $o,B: TA,A: TA > $o] :
( ( ( A @ B )
& ( 'const/sets/IN' @ TA @ B @ C ) )
= ( 'const/sets/IN' @ TA @ B @ ( 'const/sets/INTER' @ TA @ A @ C ) ) ),
inference(simp,[status(thm)],[144]) ).
thf(14333,plain,
! [TA: $tType,C: TA > $o,B: TA,A: TA > $o] :
( ( sk1 @ sk3 )
| ( ( A @ B )
& ( 'const/sets/IN' @ TA @ B @ C ) )
| ( ( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [D: skt1] : $true ) )
!= ( 'const/sets/IN' @ TA @ B @ ( 'const/sets/INTER' @ TA @ A @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[13319,168]) ).
thf(14334,plain,
( ( sk1 @ sk3 )
| ( ( sk1 @ sk3 )
& ( 'const/sets/IN' @ skt1 @ sk3
@ ^ [A: skt1] : $true ) ) ),
inference(pattern_uni,[status(thm)],[14333:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 )),bind(C,$thf( ^ [D: skt1] : $true )),bind_type(TA,$thf( skt1 ))]]) ).
thf(14455,plain,
( ( ( sk1 @ sk3 )
| ( sk1 @ sk3 ) )
& ( ( sk1 @ sk3 )
| ( 'const/sets/IN' @ skt1 @ sk3
@ ^ [A: skt1] : $true ) ) ),
inference(cnf,[status(esa)],[14334]) ).
thf(14456,plain,
( ( sk1 @ sk3 )
| ( sk1 @ sk3 ) ),
inference(cnfConj,[status(thm)],[14455]) ).
thf(14458,plain,
sk1 @ sk3,
inference(simp,[status(thm)],[14456]) ).
thf(14463,plain,
( ~ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true
@ sk3 )
| ~ $true ),
inference(rewrite,[status(thm)],[269,14458]) ).
thf(14464,plain,
~ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true
@ sk3 ),
inference(simp,[status(thm)],[14463]) ).
thf(15424,plain,
! [TA: $tType,TB: $tType,F: TB > TA > TA > $o,E: TB > TA > TA > $o,D: TB > TA,C: TB,B: TA > $o,A: TA > $o] :
( ( ( ^ [G: TA] : A )
!= ( E @ C ) )
| ( ( ^ [G: TA] : B )
!= ( F @ C ) )
| ~ ( 'const/sets/IN' @ TB @ C
@ ^ [G: TB] :
( 'const/sets/IN' @ TA @ ( D @ G )
@ ^ [H: TA] : ( 'const/sets/INTER' @ TA @ ( E @ G @ H ) @ ( F @ G @ H ) @ H ) ) )
| ( ( 'const/sets/INTER' @ TA @ A @ B @ ( D @ C ) )
!= ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [G: skt1] : $true
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[10322,14464]) ).
thf(15442,plain,
! [TB: $tType,C: TB > skt1 > skt1 > $o,B: TB > skt1 > skt1 > $o,A: TB] :
( ( ( ^ [D: skt1] : sk1 )
!= ( B @ A ) )
| ( ( ^ [D: skt1,E: skt1] : $true )
!= ( C @ A ) )
| ~ ( 'const/sets/IN' @ TB @ A
@ ^ [D: TB] :
( 'const/sets/IN' @ skt1 @ sk3
@ ^ [E: skt1] : ( 'const/sets/INTER' @ skt1 @ ( B @ D @ E ) @ ( C @ D @ E ) @ E ) ) ) ),
inference(pre_uni,[status(thm)],[15424:[bind(A,$thf( sk1 )),bind(B,$thf( ^ [G: skt1] : $true )),bind(C,$thf( C )),bind(D,$thf( ^ [G: TB] : sk3 )),bind_type(TA,$thf( skt1 ))]]) ).
thf(15443,plain,
! [TB: $tType,A: TB] :
~ ( 'const/sets/IN' @ TB @ A
@ ^ [B: TB] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [C: skt1] : $true ) ) ),
inference(pre_uni,[status(thm)],[15442:[bind(A,$thf( (@) )),bind(B,$thf( ^ [D: TB] : ^ [E: skt1] : sk1 )),bind(C,$thf( ^ [D: TB] : ^ [E: skt1] : ^ [F: skt1] : $true ))]]) ).
thf(15452,plain,
! [TA: $tType,A: TA] :
~ ( 'const/sets/IN' @ TA @ A
@ ^ [B: TA] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [C: skt1] : $true ) ) ),
inference(simp,[status(thm)],[15443]) ).
thf(15794,plain,
! [TA: $tType,TB: $tType,C: TB,B: TA,A: TA > $o] :
( ~ ( A @ B )
| ~ $true
| ( ( 'const/sets/IN' @ TA @ B @ A )
!= ( 'const/sets/IN' @ TB @ C
@ ^ [D: TB] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [E: skt1] : $true ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15452]) ).
thf(15795,plain,
! [TA: $tType,TB: $tType,C: TB,B: TA,A: TA > $o] :
( ~ ( A @ B )
| ( ( 'const/sets/IN' @ TA @ B @ A )
!= ( 'const/sets/IN' @ TB @ C
@ ^ [D: TB] :
( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [E: skt1] : $true ) ) ) ) ),
inference(simp,[status(thm)],[15794]) ).
thf(15796,plain,
~ ( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [A: skt1] : $true ) ),
inference(pattern_uni,[status(thm)],[15795:[bind(A,$thf( ^ [D: TB] : ( 'const/sets/IN' @ skt1 @ sk3 @ ( 'const/sets/INTER' @ skt1 @ sk1 @ ^ [E: skt1] : $true ) ) )),bind(B,$thf( B )),bind(C,$thf( B )),bind_type(TA,$thf( TB ))]]) ).
thf(15866,plain,
! [TA: $tType,B: TA > $o,A: TA] :
( ~ ( 'const/sets/IN' @ TA @ A @ B )
| ( ( 'const/sets/IN' @ TA @ A
@ ( 'const/sets/INTER' @ TA @ B
@ ^ [C: TA] : $true ) )
!= ( 'const/sets/IN' @ skt1 @ sk3
@ ( 'const/sets/INTER' @ skt1 @ sk1
@ ^ [C: skt1] : $true ) ) ) ),
inference(paramod_ordered,[status(thm)],[13576,15796]) ).
thf(15867,plain,
~ ( 'const/sets/IN' @ skt1 @ sk3 @ sk1 ),
inference(pattern_uni,[status(thm)],[15866:[bind(A,$thf( sk3 )),bind(B,$thf( sk1 )),bind_type(TA,$thf( skt1 ))]]) ).
thf(15933,plain,
! [TA: $tType,B: TA,A: TA > $o] :
( ~ ( A @ B )
| ~ $true
| ( ( 'const/sets/IN' @ TA @ B @ A )
!= ( 'const/sets/IN' @ skt1 @ sk3 @ sk1 ) ) ),
inference(paramod_ordered,[status(thm)],[25,15867]) ).
thf(15934,plain,
! [TA: $tType,B: TA,A: TA > $o] :
( ~ ( A @ B )
| ( ( 'const/sets/IN' @ TA @ B @ A )
!= ( 'const/sets/IN' @ skt1 @ sk3 @ sk1 ) ) ),
inference(simp,[status(thm)],[15933]) ).
thf(15935,plain,
~ ( sk1 @ sk3 ),
inference(pattern_uni,[status(thm)],[15934:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 )),bind_type(TA,$thf( skt1 ))]]) ).
thf(15962,plain,
~ $true,
inference(rewrite,[status(thm)],[15935,14458]) ).
thf(15963,plain,
$false,
inference(simp,[status(thm)],[15962]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV453^1 : TPTP v9.3.1. Released v7.0.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.10/0.22 % Computer : n004.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 15:48:22 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 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
% 1.00/0.80 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.16/1.00 % [INFO] Parsing done (198ms).
% 1.16/1.02 % [INFO] Running in sequential loop mode.
% 1.94/1.42 % [INFO] eprover registered as external prover.
% 1.94/1.43 % [INFO] Scanning for conjecture ...
% 2.12/1.52 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.12/1.56 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 2.12/1.57 % [INFO] Problem is higher-order (TPTP THF).
% 2.12/1.58 % [INFO] Type checking passed.
% 2.12/1.58 % [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 ...
% 93.00/41.08 % [INFO] Killing All external provers ...
% 93.00/41.09 % Time passed: 40713ms (effective reasoning time: 40060ms)
% 93.00/41.09 % 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)>
% 93.00/41.09 % Axioms used in derivation (3): thm/sets/IN_, thm/sets/IN_UNIV_, thm/sets/IN_INTER_
% 93.00/41.09 % No. of inferences in proof: 69
% 93.00/41.09 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 40713 ms resp. 40060 ms w/o parsing
% 93.19/41.17 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 93.19/41.17 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------