%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : NUM637^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n002.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:17:51 AM UTC 2026
% Result : Theorem 34.48s 8.44s
% Output : Refutation 29.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 7
% Syntax : Number of formulae : 152 ( 50 unt; 0 typ; 1 def)
% Number of atoms : 453 ( 126 equ; 19 cnn)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1578 ( 289 ~; 205 |; 1 &;1071 @)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 8 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 135 ( 135 >; 0 *; 0 +; 0 <<)
% Number of symbols : 11 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 449 ( 156 ^; 291 !; 1 ?; 449 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% Comments :
%------------------------------------------------------------------------------
thf(nat_type,type,
nat: $tType ).
thf(set_type,type,
set: $tType ).
thf(x_decl,type,
x: nat ).
thf(n_1_decl,type,
n_1: nat ).
thf(suc_decl,type,
suc: nat > nat ).
thf(esti_decl,type,
esti: nat > set > $o ).
thf(setof_decl,type,
setof: ( nat > $o ) > set ).
thf(sk1_decl,type,
sk1: set > nat ).
thf(sk3_decl,type,
sk3: ( nat > $o ) > nat ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: set] :
@+[B: nat] :
~ ( ( esti @ B @ A )
=> ( esti @ ( suc @ B ) @ A ) ) ) ) ).
thf(6,axiom,
! [A: nat > $o,B: nat] :
( ( A @ B )
=> ( esti @ B @ ( setof @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',estii) ).
thf(22,plain,
! [A: nat > $o,B: nat] :
( ( A @ B )
=> ( esti @ B @ ( setof @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(23,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ B )
| ( esti @ B @ ( setof @ A ) ) ),
inference(cnf,[status(esa)],[22]) ).
thf(100,plain,
! [B: nat > $o,A: nat] :
( ~ ~ ( B @ A )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(prim_subst,[status(thm)],[23:[bind(A,$thf( ^ [D: nat] : ~ ( C @ D ) ))]]) ).
thf(117,plain,
! [B: nat > $o,A: nat] :
( ( B @ A )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(cnf,[status(esa)],[100]) ).
thf(118,plain,
! [B: nat > $o,A: nat] :
( ( B @ A )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(simp,[status(thm)],[117]) ).
thf(5,axiom,
! [A: set] :
( ( esti @ n_1 @ A )
=> ( ! [B: nat] :
( ( esti @ B @ A )
=> ( esti @ ( suc @ B ) @ A ) )
=> ! [B: nat] : ( esti @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
thf(18,plain,
! [A: set] :
( ( esti @ n_1 @ A )
=> ( ! [B: nat] :
( ( esti @ B @ A )
=> ( esti @ ( suc @ B ) @ A ) )
=> ! [B: nat] : ( esti @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(19,plain,
! [B: nat,A: set] :
( ( ~ ( esti @ n_1 @ A )
| ( esti @ ( sk1 @ A ) @ A )
| ( esti @ B @ A ) )
& ( ~ ( esti @ n_1 @ A )
| ~ ( esti @ ( suc @ ( sk1 @ A ) ) @ A )
| ( esti @ B @ A ) ) ),
inference(cnf,[status(esa)],[18]) ).
thf(20,plain,
! [B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ ( sk1 @ A ) @ A )
| ( esti @ B @ A ) ),
inference(cnfConj,[status(thm)],[19]) ).
thf(69,plain,
! [B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ ( sk1 @ A ) @ A )
| ( ( esti @ B @ A )
!= ( esti @ ( sk1 @ A ) @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[20]) ).
thf(70,plain,
! [A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ ( sk1 @ A ) @ A ) ),
inference(pattern_uni,[status(thm)],[69:[bind(A,$thf( C )),bind(B,$thf( sk1 @ C ))]]) ).
thf(75,plain,
! [A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ ( sk1 @ A ) @ A ) ),
inference(simp,[status(thm)],[70]) ).
thf(484,plain,
! [C: set,B: nat > $o,A: nat] :
( ( B @ A )
| ~ $true
| ( esti @ ( sk1 @ C ) @ C )
| ( ( esti @ A
@ ( setof
@ ^ [D: nat] :
~ ( B @ D ) ) )
!= ( esti @ n_1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[118,75]) ).
thf(485,plain,
! [C: set,B: nat > $o,A: nat] :
( ( B @ A )
| ( esti @ ( sk1 @ C ) @ C )
| ( ( esti @ A
@ ( setof
@ ^ [D: nat] :
~ ( B @ D ) ) )
!= ( esti @ n_1 @ C ) ) ),
inference(simp,[status(thm)],[484]) ).
thf(486,plain,
! [A: nat > $o] :
( ( A @ n_1 )
| ( esti
@ ( sk1
@ ( setof
@ ^ [B: nat] :
~ ( A @ B ) ) )
@ ( setof
@ ^ [B: nat] :
~ ( A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[485:[bind(A,$thf( n_1 )),bind(B,$thf( E )),bind(C,$thf( setof @ ^ [E: nat] : ~ ( E @ E ) ))]]) ).
thf(580,plain,
! [A: nat > $o] :
( ( A @ n_1 )
| ( esti
@ ( sk1
@ ( setof
@ ^ [B: nat] :
~ ( A @ B ) ) )
@ ( setof
@ ^ [B: nat] :
~ ( A @ B ) ) ) ),
inference(simp,[status(thm)],[486]) ).
thf(4,axiom,
! [A: nat > $o,B: nat] :
( ( esti @ B @ ( setof @ A ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',estie) ).
thf(16,plain,
! [A: nat > $o,B: nat] :
( ( esti @ B @ ( setof @ A ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(17,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( A @ B ) ),
inference(cnf,[status(esa)],[16]) ).
thf(32,plain,
! [A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [B: nat] : $false ) )
| $false ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [C: nat] : $false ))]]) ).
thf(35,plain,
! [A: nat] :
~ ( esti @ A
@ ( setof
@ ^ [B: nat] : $false ) ),
inference(simp,[status(thm)],[32]) ).
thf(1046,plain,
! [B: nat,A: nat > $o] :
( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
| ~ $true
| ( ( A @ n_1 )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[580,35]) ).
thf(1047,plain,
! [B: nat,A: nat > $o] :
( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
| ( ( A @ n_1 )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(simp,[status(thm)],[1046]) ).
thf(1120,plain,
! [A: nat > nat] :
( esti
@ ( sk1
@ ( setof
@ ^ [B: nat] :
~ ( esti @ ( A @ B )
@ ( setof
@ ^ [C: nat] : $false ) ) ) )
@ ( setof
@ ^ [B: nat] :
~ ( esti @ ( A @ B )
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(pre_uni,[status(thm)],[1047:[bind(A,$thf( ^ [D: nat] : ( esti @ ( C @ D ) @ ( setof @ ^ [E: nat] : $false ) ) )),bind(B,$thf( C @ n_1 ))]]) ).
thf(1168,plain,
! [A: nat > nat] :
( esti
@ ( sk1
@ ( setof
@ ^ [B: nat] :
~ ( esti @ ( A @ B )
@ ( setof
@ ^ [C: nat] : $false ) ) ) )
@ ( setof
@ ^ [B: nat] :
~ ( esti @ ( A @ B )
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(simp,[status(thm)],[1120]) ).
thf(1369,plain,
( esti
@ ( sk1
@ ( setof
@ ^ [A: nat] : ~ $false ) )
@ ( setof
@ ^ [A: nat] : ~ $false ) ),
inference(rewrite,[status(thm)],[1168,35]) ).
thf(1370,plain,
( esti
@ ( sk1
@ ( setof
@ ^ [A: nat] : $true ) )
@ ( setof
@ ^ [A: nat] : $true ) ),
inference(simp,[status(thm)],[1369]) ).
thf(29,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ~ ( B @ A ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [D: nat] : ~ ( C @ D ) ))]]) ).
thf(38,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ~ ( B @ A ) ),
inference(cnf,[status(esa)],[29]) ).
thf(39,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ~ ( B @ A ) ),
inference(simp,[status(thm)],[38]) ).
thf(1390,plain,
! [B: nat > $o,A: nat] :
( ~ $true
| ~ ( B @ A )
| ( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] : $true ) )
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1370,39]) ).
thf(1391,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ A )
| ( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] : $true ) )
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ) ),
inference(simp,[status(thm)],[1390]) ).
thf(1431,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ A )
| ( ( sk1
@ ( setof
@ ^ [C: nat] : $true ) )
!= A )
| ( ( setof
@ ^ [C: nat] :
~ ( B @ C ) )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[1391]) ).
thf(1458,plain,
! [A: nat > $o] :
( ~ ( A
@ ( sk1
@ ( setof
@ ^ [B: nat] : $true ) ) )
| ( ( setof
@ ^ [B: nat] :
~ ( A @ B ) )
!= ( setof
@ ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[1431]) ).
thf(3116,plain,
! [A: nat > $o] :
( ~ ( A
@ ( sk1
@ ( setof
@ ^ [B: nat] : $true ) ) )
| ( ( ^ [B: nat] :
~ ( A @ B ) )
!= ( ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[1458]) ).
thf(1049,plain,
! [B: nat,A: nat > $o] :
( ( A @ n_1 )
| ~ $true
| ( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[580,35]) ).
thf(1050,plain,
! [B: nat,A: nat > $o] :
( ( A @ n_1 )
| ( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(simp,[status(thm)],[1049]) ).
thf(1125,plain,
! [B: nat,A: nat > $o] :
( ( A @ n_1 )
| ( ( sk1
@ ( setof
@ ^ [C: nat] :
~ ( A @ C ) ) )
!= B )
| ( ( setof
@ ^ [C: nat] :
~ ( A @ C ) )
!= ( setof
@ ^ [C: nat] : $false ) ) ),
inference(simp,[status(thm)],[1050]) ).
thf(1173,plain,
! [A: nat > $o] :
( ( A @ n_1 )
| ( ( setof
@ ^ [B: nat] :
~ ( A @ B ) )
!= ( setof
@ ^ [B: nat] : $false ) ) ),
inference(simp,[status(thm)],[1125]) ).
thf(1582,plain,
! [A: nat > $o] :
( ( A @ n_1 )
| ( ( ^ [B: nat] :
~ ( A @ B ) )
!= ( ^ [B: nat] : $false ) ) ),
inference(simp,[status(thm)],[1173]) ).
thf(1691,plain,
! [A: nat > $o] :
( ~ ( A @ ( sk3 @ A ) )
| ( A @ n_1 ) ),
inference(func_ext,[status(esa)],[1582]) ).
thf(1787,plain,
! [A: nat > $o] :
( ~ ( A @ ( sk3 @ A ) )
| ( A @ n_1 ) ),
inference(cnf,[status(esa)],[1691]) ).
thf(2192,plain,
! [A: nat > $o] :
( ~ ~ ( A
@ ( sk3
@ ^ [B: nat] :
~ ( A @ B ) ) )
| ~ ( A @ n_1 ) ),
inference(prim_subst,[status(thm)],[1787:[bind(A,$thf( ^ [C: nat] : ~ ( B @ C ) ))]]) ).
thf(2236,plain,
! [A: nat > $o] :
( ( A
@ ( sk3
@ ^ [B: nat] :
~ ( A @ B ) ) )
| ~ ( A @ n_1 ) ),
inference(cnf,[status(esa)],[2192]) ).
thf(2237,plain,
! [A: nat > $o] :
( ( A
@ ( sk3
@ ^ [B: nat] :
~ ( A @ B ) ) )
| ~ ( A @ n_1 ) ),
inference(simp,[status(thm)],[2236]) ).
thf(86,plain,
! [D: nat,C: nat > $o,B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ B @ A )
| ~ $true
| ( esti @ D @ ( setof @ C ) )
| ( ( esti @ ( sk1 @ A ) @ A )
!= ( C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[20,23]) ).
thf(87,plain,
! [D: nat,C: nat > $o,B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ B @ A )
| ( esti @ D @ ( setof @ C ) )
| ( ( esti @ ( sk1 @ A ) @ A )
!= ( C @ D ) ) ),
inference(simp,[status(thm)],[86]) ).
thf(112,plain,
! [C: set,B: nat > set,A: nat] :
( ~ ( esti @ n_1 @ ( B @ ( sk1 @ C ) ) )
| ( esti @ A @ ( B @ ( sk1 @ C ) ) )
| ( esti @ ( sk1 @ C )
@ ( setof
@ ^ [D: nat] : ( esti @ D @ ( B @ D ) ) ) )
| ( ( B @ ( sk1 @ C ) )
!= C ) ),
inference(pre_uni,[status(thm)],[87:[bind(A,$thf( F @ ( sk1 @ H ) )),bind(B,$thf( B )),bind(C,$thf( ^ [F: nat] : ( esti @ F @ ( F @ F ) ) )),bind(D,$thf( sk1 @ H ))]]) ).
thf(114,plain,
! [C: set,B: nat > set,A: nat] :
( ( esti @ ( sk1 @ C )
@ ( setof
@ ^ [D: nat] : ( esti @ D @ ( B @ D ) ) ) )
| ( esti @ A @ ( B @ ( sk1 @ C ) ) )
| ~ ( esti @ n_1 @ ( B @ ( sk1 @ C ) ) )
| ( ( B @ ( sk1 @ C ) )
!= C ) ),
inference(pre_uni,[status(thm)],[112:[]]) ).
thf(116,plain,
! [C: set,B: nat > set,A: nat] :
( ( esti @ ( sk1 @ C )
@ ( setof
@ ^ [D: nat] : ( esti @ D @ ( B @ D ) ) ) )
| ( esti @ A @ ( B @ ( sk1 @ C ) ) )
| ~ ( esti @ n_1 @ ( B @ ( sk1 @ C ) ) )
| ( ( B @ ( sk1 @ C ) )
!= C ) ),
inference(simp,[status(thm)],[114]) ).
thf(55,plain,
! [D: nat,C: nat > $o,B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ B @ A )
| ~ $true
| ( C @ D )
| ( ( esti @ ( sk1 @ A ) @ A )
!= ( esti @ D @ ( setof @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,17]) ).
thf(56,plain,
! [D: nat,C: nat > $o,B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ B @ A )
| ( C @ D )
| ( ( esti @ ( sk1 @ A ) @ A )
!= ( esti @ D @ ( setof @ C ) ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(57,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ n_1 @ ( setof @ B ) )
| ( esti @ A @ ( setof @ B ) )
| ( B @ ( sk1 @ ( setof @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[56:[bind(A,$thf( setof @ F )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( sk1 @ ( setof @ F ) ))]]) ).
thf(78,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ n_1 @ ( setof @ B ) )
| ( esti @ A @ ( setof @ B ) )
| ( B @ ( sk1 @ ( setof @ B ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(2300,plain,
! [D: nat > $o,C: nat,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ $true
| ( esti @ C @ ( setof @ D ) )
| ( D @ ( sk1 @ ( setof @ D ) ) )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ n_1 @ ( setof @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,78]) ).
thf(2301,plain,
! [D: nat > $o,C: nat,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ( esti @ C @ ( setof @ D ) )
| ( D @ ( sk1 @ ( setof @ D ) ) )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ n_1 @ ( setof @ D ) ) ) ),
inference(simp,[status(thm)],[2300]) ).
thf(2302,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ n_1 )
| ( esti @ B @ ( setof @ A ) )
| ( A @ ( sk1 @ ( setof @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[2301:[bind(A,$thf( A )),bind(B,$thf( n_1 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(2398,plain,
! [A: nat] :
( ( n_1 != n_1 )
| ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( n_1
= ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(replace_leibeq,[status(thm)],[2302:[bind(A,$thf( (=) @ nat @ n_1 ))]]) ).
thf(2399,plain,
! [A: nat] :
( ( n_1 != n_1 )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 )
| ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ),
inference(lifteq,[status(thm)],[2398]) ).
thf(2457,plain,
! [A: nat] :
( ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 ) ),
inference(pattern_uni,[status(thm)],[2399:[]]) ).
thf(2489,plain,
! [A: nat] :
( ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 ) ),
inference(simp,[status(thm)],[2457]) ).
thf(4183,plain,
! [C: nat,B: nat > $o,A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 )
| ~ $true
| ( B @ C )
| ( ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= ( esti @ C @ ( setof @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[2489,17]) ).
thf(4184,plain,
! [C: nat,B: nat > $o,A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 )
| ( B @ C )
| ( ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= ( esti @ C @ ( setof @ B ) ) ) ),
inference(simp,[status(thm)],[4183]) ).
thf(4185,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 )
| ( n_1 = A ) ),
inference(pattern_uni,[status(thm)],[4184:[bind(A,$thf( A )),bind(B,$thf( (=) @ nat @ n_1 )),bind(C,$thf( A ))]]) ).
thf(4247,plain,
! [A: nat] :
( ( n_1 = A )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 ) ),
inference(lifteq,[status(thm)],[4185]) ).
thf(4457,plain,
! [A: nat] :
( ( n_1 = A )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= A )
| ( n_1 != n_1 ) ),
inference(eqfactor_ordered,[status(thm)],[4247]) ).
thf(4476,plain,
( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
= n_1 ),
inference(pattern_uni,[status(thm)],[4457:[bind(A,$thf( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) ))]]) ).
thf(25,plain,
! [D: nat,C: nat > $o,B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ~ $true
| ( C @ D )
| ( ( A @ B )
!= ( esti @ D @ ( setof @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,17]) ).
thf(26,plain,
! [D: nat,C: nat > $o,B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( C @ D )
| ( ( A @ B )
!= ( esti @ D @ ( setof @ C ) ) ) ),
inference(simp,[status(thm)],[25]) ).
thf(34,plain,
! [C: nat > nat > $o,B: nat > nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ ( B @ D ) @ ( setof @ ( C @ D ) ) ) ) )
| ( C @ A @ ( B @ A ) ) ),
inference(pre_uni,[status(thm)],[26:[bind(A,$thf( ^ [G: nat] : ( esti @ ( E @ G ) @ ( setof @ ( G @ G ) ) ) )),bind(B,$thf( B )),bind(C,$thf( G @ B )),bind(D,$thf( E @ B ))]]) ).
thf(36,plain,
! [C: nat > nat > $o,B: nat > nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ ( B @ D ) @ ( setof @ ( C @ D ) ) ) ) )
| ( C @ A @ ( B @ A ) ) ),
inference(simp,[status(thm)],[34]) ).
thf(1632,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( ( setof
@ ^ [B: nat] :
~ ~ ( A @ B ) )
!= ( setof
@ ^ [B: nat] : $false ) ) ),
inference(prim_subst,[status(thm)],[1173:[bind(A,$thf( ^ [C: nat] : ~ ( B @ C ) ))]]) ).
thf(1664,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( ( setof
@ ^ [B: nat] :
~ ~ ( A @ B ) )
!= ( setof
@ ^ [B: nat] : $false ) ) ),
inference(cnf,[status(esa)],[1632]) ).
thf(1665,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( ( setof @ A )
!= ( setof
@ ^ [B: nat] : $false ) ) ),
inference(simp,[status(thm)],[1664]) ).
thf(643,plain,
! [D: nat,C: nat > nat > $o,B: nat > nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [E: nat] : ( esti @ ( B @ E ) @ ( setof @ ( C @ E ) ) ) ) )
| ~ $true
| ( ( C @ A @ ( B @ A ) )
!= ( esti @ D
@ ( setof
@ ^ [E: nat] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,35]) ).
thf(644,plain,
! [D: nat,C: nat > nat > $o,B: nat > nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [E: nat] : ( esti @ ( B @ E ) @ ( setof @ ( C @ E ) ) ) ) )
| ( ( C @ A @ ( B @ A ) )
!= ( esti @ D
@ ( setof
@ ^ [E: nat] : $false ) ) ) ),
inference(simp,[status(thm)],[643]) ).
thf(693,plain,
! [C: nat > nat > nat,B: nat > nat,A: nat] :
~ ( esti @ A
@ ( setof
@ ^ [D: nat] :
( esti @ ( B @ D )
@ ( setof
@ ^ [E: nat] :
( esti @ ( C @ D @ E )
@ ( setof
@ ^ [F: nat] : $false ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[644:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( ^ [F: nat] : ^ [G: nat] : ( esti @ ( E @ F @ G ) @ ( setof @ ^ [H: nat] : $false ) ) )),bind(D,$thf( E @ A @ ( B @ A ) ))]]) ).
thf(750,plain,
! [C: nat > nat > nat,B: nat > nat,A: nat] :
~ ( esti @ A
@ ( setof
@ ^ [D: nat] :
( esti @ ( B @ D )
@ ( setof
@ ^ [E: nat] :
( esti @ ( C @ D @ E )
@ ( setof
@ ^ [F: nat] : $false ) ) ) ) ) ),
inference(simp,[status(thm)],[693]) ).
thf(760,plain,
! [B: nat > nat,A: nat] :
~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
( esti @ ( B @ C )
@ ( setof
@ ^ [D: nat] : $false ) ) ) ),
inference(rewrite,[status(thm)],[750,35]) ).
thf(111,plain,
! [D: nat > set,C: nat > set,B: nat,A: nat] :
( ~ ( esti @ n_1 @ ( C @ B ) )
| ( esti @ A @ ( C @ B ) )
| ( esti @ B
@ ( setof
@ ^ [E: nat] : ( esti @ ( sk1 @ ( D @ E ) ) @ ( C @ E ) ) ) )
| ( ( C @ B )
!= ( D @ B ) ) ),
inference(pre_uni,[status(thm)],[87:[bind(A,$thf( F @ D )),bind(B,$thf( B )),bind(C,$thf( ^ [G: nat] : ( esti @ ( sk1 @ ( G @ G ) ) @ ( F @ G ) ) )),bind(D,$thf( D ))]]) ).
thf(113,plain,
! [D: nat > set,C: nat > set,B: nat,A: nat] :
( ( esti @ B
@ ( setof
@ ^ [E: nat] : ( esti @ ( sk1 @ ( D @ E ) ) @ ( C @ E ) ) ) )
| ( esti @ A @ ( C @ B ) )
| ~ ( esti @ n_1 @ ( C @ B ) )
| ( ( C @ B )
!= ( D @ B ) ) ),
inference(pre_uni,[status(thm)],[111:[]]) ).
thf(115,plain,
! [D: nat > set,C: nat > set,B: nat,A: nat] :
( ( esti @ B
@ ( setof
@ ^ [E: nat] : ( esti @ ( sk1 @ ( D @ E ) ) @ ( C @ E ) ) ) )
| ( esti @ A @ ( C @ B ) )
| ~ ( esti @ n_1 @ ( C @ B ) )
| ( ( C @ B )
!= ( D @ B ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(104,plain,
! [A: nat] :
( ~ $true
| ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) ) ),
inference(prim_subst,[status(thm)],[23:[bind(A,$thf( ^ [C: nat] : $true ))]]) ).
thf(126,plain,
! [A: nat] :
( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) ),
inference(simp,[status(thm)],[104]) ).
thf(249,plain,
! [C: nat > $o,B: nat,A: nat] :
( ~ $true
| ~ ( C @ B )
| ( ( esti @ A
@ ( setof
@ ^ [D: nat] : $true ) )
!= ( esti @ B
@ ( setof
@ ^ [D: nat] :
~ ( C @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[126,39]) ).
thf(250,plain,
! [C: nat > $o,B: nat,A: nat] :
( ~ ( C @ B )
| ( ( esti @ A
@ ( setof
@ ^ [D: nat] : $true ) )
!= ( esti @ B
@ ( setof
@ ^ [D: nat] :
~ ( C @ D ) ) ) ) ),
inference(simp,[status(thm)],[249]) ).
thf(265,plain,
! [C: nat > $o,B: nat,A: nat] :
( ~ ( C @ B )
| ( A != B )
| ( ( setof
@ ^ [D: nat] :
~ ( C @ D ) )
!= ( setof
@ ^ [D: nat] : $true ) ) ),
inference(simp,[status(thm)],[250]) ).
thf(285,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ A )
| ( ( setof
@ ^ [C: nat] :
~ ( B @ C ) )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[265]) ).
thf(429,plain,
! [B: nat > $o,A: nat] :
( ~ ~ ( B @ A )
| ( ( setof
@ ^ [C: nat] :
~ ~ ( B @ C ) )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(prim_subst,[status(thm)],[285:[bind(A,$thf( A )),bind(B,$thf( ^ [D: nat] : ~ ( C @ D ) ))]]) ).
thf(448,plain,
! [B: nat > $o,A: nat] :
( ( B @ A )
| ( ( setof
@ ^ [C: nat] :
~ ~ ( B @ C ) )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(cnf,[status(esa)],[429]) ).
thf(449,plain,
! [B: nat > $o,A: nat] :
( ( B @ A )
| ( ( setof @ B )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[448]) ).
thf(101,plain,
! [C: nat > set,B: nat > nat,A: nat] :
( ~ ( esti @ ( B @ A ) @ ( C @ A ) )
| ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ ( B @ D ) @ ( C @ D ) ) ) ) ),
inference(prim_subst,[status(thm)],[23:[bind(A,$thf( ^ [E: nat] : ( esti @ ( C @ E ) @ ( D @ E ) ) ))]]) ).
thf(120,plain,
! [C: nat > set,B: nat > nat,A: nat] :
( ~ ( esti @ ( B @ A ) @ ( C @ A ) )
| ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ ( B @ D ) @ ( C @ D ) ) ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(7,axiom,
! [A: $o] :
( ~ ~ A
=> A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',et) ).
thf(24,plain,
$true,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(28,plain,
! [C: nat > set,B: nat > nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ ( B @ D ) @ ( C @ D ) ) ) )
| ( esti @ ( B @ A ) @ ( C @ A ) ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [E: nat] : ( esti @ ( C @ E ) @ ( D @ E ) ) ))]]) ).
thf(37,plain,
! [C: nat > set,B: nat > nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ ( B @ D ) @ ( C @ D ) ) ) )
| ( esti @ ( B @ A ) @ ( C @ A ) ) ),
inference(simp,[status(thm)],[28]) ).
thf(4971,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( ( ^ [B: nat] :
~ ( A @ B ) )
!= ( ^ [B: nat] : $true ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= ( sk1
@ ( setof
@ ^ [B: nat] : $true ) ) ) ),
inference(paramod_ordered,[status(thm)],[4476,3116]) ).
thf(4998,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( ( ^ [B: nat] :
~ ( A @ B ) )
!= ( ^ [B: nat] : $true ) )
| ( ( setof @ ( (=) @ nat @ n_1 ) )
!= ( setof
@ ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[4971]) ).
thf(5020,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( ( ^ [B: nat] :
~ ( A @ B ) )
!= ( ^ [B: nat] : $true ) )
| ( ( (=) @ nat @ n_1 )
!= ( ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[4998]) ).
thf(27,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( ( A @ B )
!= ( ~ ( esti @ B @ ( setof @ A ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[17]) ).
thf(33,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( ( A @ B )
!= ( ~ ( esti @ B @ ( setof @ A ) ) ) ) ),
inference(simp,[status(thm)],[27]) ).
thf(21,plain,
! [B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ~ ( esti @ ( suc @ ( sk1 @ A ) ) @ A )
| ( esti @ B @ A ) ),
inference(cnfConj,[status(thm)],[19]) ).
thf(93,plain,
! [D: nat,C: nat > $o,B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ~ $true
| ( esti @ D @ ( setof @ C ) )
| ( ( A @ B )
!= ( C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[17,23]) ).
thf(94,plain,
! [D: nat,C: nat > $o,B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( esti @ D @ ( setof @ C ) )
| ( ( A @ B )
!= ( C @ D ) ) ),
inference(simp,[status(thm)],[93]) ).
thf(108,plain,
! [D: nat,C: nat > $o,B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( esti @ D @ ( setof @ C ) )
| ( ( A @ B )
!= ( C @ D ) ) ),
inference(pre_uni,[status(thm)],[94:[]]) ).
thf(109,plain,
! [D: nat,C: nat > $o,B: nat,A: nat > $o] :
( ( esti @ D @ ( setof @ C ) )
| ~ ( esti @ B @ ( setof @ A ) )
| ( ( A @ B )
!= ( C @ D ) ) ),
inference(pre_uni,[status(thm)],[108:[]]) ).
thf(61,plain,
! [D: nat,C: set,B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ~ $true
| ( esti @ ( sk1 @ C ) @ C )
| ( esti @ D @ C )
| ( ( A @ B )
!= ( esti @ n_1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[17,20]) ).
thf(62,plain,
! [D: nat,C: set,B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( esti @ ( sk1 @ C ) @ C )
| ( esti @ D @ C )
| ( ( A @ B )
!= ( esti @ n_1 @ C ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(72,plain,
! [C: nat > set,B: nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ n_1 @ ( C @ D ) ) ) )
| ( esti @ ( sk1 @ ( C @ A ) ) @ ( C @ A ) )
| ( esti @ B @ ( C @ A ) ) ),
inference(pre_uni,[status(thm)],[62:[bind(A,$thf( ^ [F: nat] : ( esti @ n_1 @ ( F @ F ) ) )),bind(B,$thf( B )),bind(C,$thf( F @ B )),bind(D,$thf( D ))]]) ).
thf(77,plain,
! [C: nat > set,B: nat,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] : ( esti @ n_1 @ ( C @ D ) ) ) )
| ( esti @ ( sk1 @ ( C @ A ) ) @ ( C @ A ) )
| ( esti @ B @ ( C @ A ) ) ),
inference(simp,[status(thm)],[72]) ).
thf(3,axiom,
x != n_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',n) ).
thf(13,plain,
x != n_1,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(31,plain,
! [C: nat > $o,B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] :
( ( B @ D )
| ( C @ D ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [E: nat] : ( ( C @ E ) | ( D @ E ) ) ))]]) ).
thf(40,plain,
! [C: nat > $o,B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] :
( ( B @ D )
| ( C @ D ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(cnf,[status(esa)],[31]) ).
thf(41,plain,
! [C: nat > $o,B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [D: nat] :
( ( B @ D )
| ( C @ D ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(simp,[status(thm)],[40]) ).
thf(1,conjecture,
~ ! [A: nat] :
( x
!= ( suc @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz3) ).
thf(2,negated_conjecture,
~ ~ ! [A: nat] :
( x
!= ( suc @ A ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(8,plain,
~ ~ ! [A: nat] :
( x
!= ( suc @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(9,plain,
! [A: nat] :
( x
!= ( suc @ A ) ),
inference(polarity_switch,[status(thm)],[8]) ).
thf(10,plain,
~ ? [A: nat] :
( x
= ( suc @ A ) ),
inference(miniscope,[status(thm)],[9]) ).
thf(11,plain,
! [A: nat] :
( x
!= ( suc @ A ) ),
inference(cnf,[status(esa)],[10]) ).
thf(12,plain,
! [A: nat] :
( ( suc @ A )
!= x ),
inference(lifteq,[status(thm)],[11]) ).
thf(202,plain,
! [B: nat,A: nat] :
( ~ $true
| ( ( esti @ A
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[126,35]) ).
thf(203,plain,
! [B: nat,A: nat] :
( ( esti @ A
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(208,plain,
! [B: nat,A: nat] :
( ( A != B )
| ( ( setof
@ ^ [C: nat] : $false )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[203]) ).
thf(209,plain,
( ( setof
@ ^ [A: nat] : $false )
!= ( setof
@ ^ [A: nat] : $true ) ),
inference(simp,[status(thm)],[208]) ).
thf(2886,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( ( setof
@ ^ [B: nat] : $true )
!= ( setof
@ ^ [B: nat] : $true ) )
| ( A
@ ( sk3
@ ^ [B: nat] :
~ ( A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[2237,209]) ).
thf(2887,plain,
! [A: nat > $o] :
( ~ ( A @ n_1 )
| ( A
@ ( sk3
@ ^ [B: nat] :
~ ( A @ B ) ) ) ),
inference(simp,[status(thm)],[2886]) ).
thf(2963,plain,
( ( n_1 != n_1 )
| ( n_1
= ( sk3
@ ^ [A: nat] : ( n_1 != A ) ) ) ),
inference(replace_leibeq,[status(thm)],[2887:[bind(A,$thf( (=) @ nat @ n_1 ))]]) ).
thf(2965,plain,
( ( n_1 != n_1 )
| ( ( sk3
@ ^ [A: nat] : ( n_1 != A ) )
= n_1 ) ),
inference(lifteq,[status(thm)],[2963]) ).
thf(3002,plain,
( ( sk3
@ ^ [A: nat] : ( n_1 != A ) )
= n_1 ),
inference(pattern_uni,[status(thm)],[2965:[]]) ).
thf(1392,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ~ $true
| ( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] : $true ) )
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1370,39]) ).
thf(1393,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ( ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] : $true ) )
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[1392]) ).
thf(1437,plain,
~ ( esti
@ ( sk1
@ ( setof
@ ^ [A: nat] : $true ) )
@ ( setof
@ ^ [A: nat] :
~ ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) ) ) ),
inference(pre_uni,[status(thm)],[1393:[bind(A,$thf( sk1 @ ( setof @ ^ [C: nat] : $true ) )),bind(B,$thf( ^ [C: nat] : ( esti @ C @ ( setof @ ^ [D: nat] : $true ) ) ))]]) ).
thf(1476,plain,
~ ( esti
@ ( sk1
@ ( setof
@ ^ [A: nat] : $true ) )
@ ( setof
@ ^ [A: nat] : ~ $true ) ),
inference(rewrite,[status(thm)],[1437,126]) ).
thf(1477,plain,
~ ( esti
@ ( sk1
@ ( setof
@ ^ [A: nat] : $true ) )
@ ( setof
@ ^ [A: nat] : $false ) ),
inference(simp,[status(thm)],[1476]) ).
thf(2955,plain,
! [A: nat > $o] :
( ~ ( A
@ ( sk3
@ ^ [B: nat] :
~ ~ ( A @ B ) ) )
| ~ ~ ( A @ n_1 ) ),
inference(prim_subst,[status(thm)],[2237:[bind(A,$thf( ^ [C: nat] : ~ ( B @ C ) ))]]) ).
thf(3047,plain,
! [A: nat > $o] :
( ~ ( A
@ ( sk3
@ ^ [B: nat] :
~ ~ ( A @ B ) ) )
| ( A @ n_1 ) ),
inference(cnf,[status(esa)],[2955]) ).
thf(3048,plain,
! [A: nat > $o] :
( ~ ( A @ ( sk3 @ A ) )
| ( A @ n_1 ) ),
inference(simp,[status(thm)],[3047]) ).
thf(83,plain,
! [D: nat,C: set,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ $true
| ( esti @ ( sk1 @ C ) @ C )
| ( esti @ D @ C )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ n_1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[23,20]) ).
thf(84,plain,
! [D: nat,C: set,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ( esti @ ( sk1 @ C ) @ C )
| ( esti @ D @ C )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ n_1 @ C ) ) ),
inference(simp,[status(thm)],[83]) ).
thf(85,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ n_1 )
| ( esti @ ( sk1 @ ( setof @ B ) ) @ ( setof @ B ) )
| ( esti @ A @ ( setof @ B ) ) ),
inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( E )),bind(B,$thf( n_1 )),bind(C,$thf( setof @ E ))]]) ).
thf(119,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ n_1 )
| ( esti @ ( sk1 @ ( setof @ B ) ) @ ( setof @ B ) )
| ( esti @ A @ ( setof @ B ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(73,plain,
! [B: nat > set,A: nat] :
( ~ ( esti @ n_1
@ ( setof
@ ^ [C: nat] : ( esti @ C @ ( B @ C ) ) ) )
| ( esti @ ( sk1 @ ( B @ n_1 ) ) @ ( B @ n_1 ) )
| ( esti @ A @ ( B @ n_1 ) ) ),
inference(pre_uni,[status(thm)],[62:[bind(A,$thf( ^ [F: nat] : ( esti @ F @ ( F @ F ) ) )),bind(B,$thf( n_1 )),bind(C,$thf( F @ n_1 )),bind(D,$thf( D ))]]) ).
thf(79,plain,
! [B: nat > set,A: nat] :
( ~ ( esti @ n_1
@ ( setof
@ ^ [C: nat] : ( esti @ C @ ( B @ C ) ) ) )
| ( esti @ ( sk1 @ ( B @ n_1 ) ) @ ( B @ n_1 ) )
| ( esti @ A @ ( B @ n_1 ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(415,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ A )
| ( ( ^ [C: nat] :
~ ( B @ C ) )
!= ( ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[285]) ).
thf(14,plain,
x != n_1,
inference(polarity_switch,[status(thm)],[13]) ).
thf(15,plain,
n_1 != x,
inference(lifteq,[status(thm)],[14]) ).
thf(7069,plain,
$false,
inference(e,[status(thm)],[1458,3116,2237,116,4476,17,39,16,23,36,1665,760,115,449,120,1173,24,37,5020,78,33,21,1370,1787,285,109,77,13,41,4998,22,118,12,3002,1477,35,209,3048,580,18,8,75,119,126,79,415,1582,15]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM637^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n002.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % 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 12:33:52 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.01/0.84 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.43/1.05 % [INFO] Parsing done (207ms).
% 1.43/1.06 % [INFO] Running in sequential loop mode.
% 1.97/1.47 % [INFO] eprover registered as external prover.
% 1.97/1.48 % [INFO] Scanning for conjecture ...
% 2.18/1.57 % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ...
% 2.35/1.61 % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms).
% 2.35/1.62 % [INFO] Problem is higher-order (TPTP THF).
% 2.35/1.63 % [INFO] Type checking passed.
% 2.35/1.63 % [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 ...
% 34.48/8.44 % External prover 'e' found a proof!
% 34.48/8.44 % [INFO] Killing All external provers ...
% 34.48/8.44 % Time passed: 8076ms (effective reasoning time: 7371ms)
% 34.48/8.44 % 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)>
% 34.48/8.44 % Axioms used in derivation (5): n, estii, et, estie, ax5
% 34.48/8.44 % No. of inferences in proof: 151
% 34.48/8.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 8076 ms resp. 7371 ms w/o parsing
% 29.74/8.56 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 29.74/8.57 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------