%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : NUM636^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 : n008.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:50 AM UTC 2026
% Result : Theorem 25.04s 6.81s
% Output : Refutation 22.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 8
% Syntax : Number of formulae : 135 ( 35 unt; 0 typ; 2 def)
% Number of atoms : 544 ( 306 equ; 108 cnn)
% Maximal formula atoms : 6 ( 4 avg)
% Number of connectives : 1500 ( 299 ~; 206 |; 1 &; 981 @)
% ( 0 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 47 ( 47 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 260 ( 74 ^; 182 !; 2 ?; 260 :)
% ( 0 !>; 0 ?*; 0 @-; 2 @+)
% Comments :
%------------------------------------------------------------------------------
thf(nat_type,type,
nat: $tType ).
thf(set_type,type,
set: $tType ).
thf(x_decl,type,
x: 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(n_1_decl,type,
n_1: nat ).
thf(sk1_decl,type,
sk1: set > nat ).
thf(sk2_decl,type,
sk2: nat > nat ).
thf(sk3_decl,type,
sk3: nat ).
thf(sk5_decl,type,
sk5: nat ).
thf(sk6_decl,type,
sk6: nat ).
thf(sk7_decl,type,
sk7: nat ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: set] :
@+[B: nat] :
~ ( ( esti @ B @ A )
=> ( esti @ ( suc @ B ) @ A ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: nat > nat] :
! [B: nat] :
( ( A @ ( suc @ B ) )
= B ) ) ) ).
thf(3,axiom,
! [A: nat > $o,B: nat] :
( ( esti @ B @ ( setof @ A ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',estie) ).
thf(11,plain,
! [A: nat > $o,B: nat] :
( ( esti @ B @ ( setof @ A ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(12,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( A @ B ) ),
inference(cnf,[status(esa)],[11]) ).
thf(88,plain,
! [A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [B: nat] : $false ) )
| $false ),
inference(prim_subst,[status(thm)],[12:[bind(A,$thf( ^ [C: nat] : $false ))]]) ).
thf(115,plain,
! [A: nat] :
~ ( esti @ A
@ ( setof
@ ^ [B: nat] : $false ) ),
inference(simp,[status(thm)],[88]) ).
thf(1,conjecture,
( ( suc @ x )
!= x ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz2) ).
thf(2,negated_conjecture,
~ ( ( ( suc @ x )
!= x ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(8,plain,
~ ( ( ( suc @ x )
!= x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(9,plain,
( ( suc @ x )
= x ),
inference(polarity_switch,[status(thm)],[8]) ).
thf(10,plain,
( ( suc @ x )
= x ),
inference(lifteq,[status(thm)],[9]) ).
thf(4,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(13,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)],[4]) ).
thf(14,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)],[13]) ).
thf(16,plain,
! [B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ~ ( esti @ ( suc @ ( sk1 @ A ) ) @ A )
| ( esti @ B @ A ) ),
inference(cnfConj,[status(thm)],[14]) ).
thf(33,plain,
! [B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ~ ( esti @ x @ A )
| ( esti @ B @ A )
| ( ( suc @ ( sk1 @ A ) )
!= ( suc @ x ) ) ),
inference(paramod_ordered,[status(thm)],[10,16]) ).
thf(39,plain,
! [B: nat,A: set] :
( ( esti @ B @ A )
| ~ ( esti @ n_1 @ A )
| ~ ( esti @ x @ A )
| ( ( sk1 @ A )
!= x ) ),
inference(simp,[status(thm)],[33]) ).
thf(74,plain,
! [D: nat,C: nat > $o,B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ~ ( esti @ x @ A )
| ( ( sk1 @ A )
!= x )
| ~ $true
| ( C @ D )
| ( ( esti @ B @ A )
!= ( esti @ D @ ( setof @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[39,12]) ).
thf(75,plain,
! [D: nat,C: nat > $o,B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ~ ( esti @ x @ A )
| ( ( sk1 @ A )
!= x )
| ( C @ D )
| ( ( esti @ B @ A )
!= ( esti @ D @ ( setof @ C ) ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(76,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ n_1 @ ( setof @ B ) )
| ~ ( esti @ x @ ( setof @ B ) )
| ( ( sk1 @ ( setof @ B ) )
!= x )
| ( B @ A ) ),
inference(pattern_uni,[status(thm)],[75:[bind(A,$thf( setof @ E )),bind(B,$thf( B )),bind(C,$thf( E )),bind(D,$thf( B ))]]) ).
thf(110,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ n_1 @ ( setof @ B ) )
| ~ ( esti @ x @ ( setof @ B ) )
| ( ( sk1 @ ( setof @ B ) )
!= x )
| ( B @ A ) ),
inference(simp,[status(thm)],[76]) ).
thf(5,axiom,
! [A: nat > $o,B: nat] :
( ( A @ B )
=> ( esti @ B @ ( setof @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',estii) ).
thf(17,plain,
! [A: nat > $o,B: nat] :
( ( A @ B )
=> ( esti @ B @ ( setof @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(18,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ B )
| ( esti @ B @ ( setof @ A ) ) ),
inference(cnf,[status(esa)],[17]) ).
thf(380,plain,
! [D: nat > $o,C: nat,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ ( esti @ n_1 @ ( setof @ D ) )
| ~ $true
| ( ( sk1 @ ( setof @ D ) )
!= x )
| ( D @ C )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ x @ ( setof @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,110]) ).
thf(381,plain,
! [D: nat > $o,C: nat,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ ( esti @ n_1 @ ( setof @ D ) )
| ( ( sk1 @ ( setof @ D ) )
!= x )
| ( D @ C )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ x @ ( setof @ D ) ) ) ),
inference(simp,[status(thm)],[380]) ).
thf(382,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ x )
| ~ ( esti @ n_1 @ ( setof @ A ) )
| ( ( sk1 @ ( setof @ A ) )
!= x )
| ( A @ B ) ),
inference(pattern_uni,[status(thm)],[381:[bind(A,$thf( A )),bind(B,$thf( x )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(425,plain,
! [A: nat] :
( ( x != x )
| ~ ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( x = A ) ),
inference(replace_leibeq,[status(thm)],[382:[bind(A,$thf( (=) @ nat @ x ))]]) ).
thf(428,plain,
! [A: nat] :
( ( x != x )
| ( x = A )
| ~ ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x ) ),
inference(lifteq,[status(thm)],[425]) ).
thf(454,plain,
! [A: nat] :
( ( x = A )
| ~ ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x ) ),
inference(simp,[status(thm)],[428]) ).
thf(420,plain,
! [A: nat] :
( ~ $true
| ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) ) ),
inference(prim_subst,[status(thm)],[18:[bind(A,$thf( ^ [C: nat] : $true ))]]) ).
thf(445,plain,
! [A: nat] :
( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) ),
inference(simp,[status(thm)],[420]) ).
thf(377,plain,
! [D: nat > $o,C: nat,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ $true
| ~ ( esti @ x @ ( setof @ D ) )
| ( ( sk1 @ ( setof @ D ) )
!= x )
| ( D @ C )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ n_1 @ ( setof @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,110]) ).
thf(378,plain,
! [D: nat > $o,C: nat,B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ ( esti @ x @ ( setof @ D ) )
| ( ( sk1 @ ( setof @ D ) )
!= x )
| ( D @ C )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ n_1 @ ( setof @ D ) ) ) ),
inference(simp,[status(thm)],[377]) ).
thf(379,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ n_1 )
| ~ ( esti @ x @ ( setof @ A ) )
| ( ( sk1 @ ( setof @ A ) )
!= x )
| ( A @ B ) ),
inference(pattern_uni,[status(thm)],[378:[bind(A,$thf( A )),bind(B,$thf( n_1 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(426,plain,
! [A: nat] :
( ( n_1 != n_1 )
| ~ ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( n_1 = A ) ),
inference(replace_leibeq,[status(thm)],[379:[bind(A,$thf( (=) @ nat @ n_1 ))]]) ).
thf(429,plain,
! [A: nat] :
( ( n_1 != n_1 )
| ( n_1 = A )
| ~ ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(lifteq,[status(thm)],[426]) ).
thf(456,plain,
! [A: nat] :
( ( n_1 = A )
| ~ ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(simp,[status(thm)],[429]) ).
thf(6,axiom,
! [A: nat] :
( ( suc @ A )
!= n_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
thf(19,plain,
! [A: nat] :
( ( suc @ A )
!= n_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(20,plain,
~ ? [A: nat] :
( ( suc @ A )
= n_1 ),
inference(miniscope,[status(thm)],[19]) ).
thf(21,plain,
! [A: nat] :
( ( suc @ A )
!= n_1 ),
inference(cnf,[status(esa)],[20]) ).
thf(22,plain,
! [A: nat] :
( ( suc @ A )
!= n_1 ),
inference(lifteq,[status(thm)],[21]) ).
thf(905,plain,
! [B: nat,A: nat] :
( ~ ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( n_1 != n_1 )
| ( A
!= ( suc @ B ) ) ),
inference(paramod_ordered,[status(thm)],[456,22]) ).
thf(906,plain,
! [B: nat,A: nat] :
( ~ ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( A
!= ( suc @ B ) ) ),
inference(simp,[status(thm)],[905]) ).
thf(907,plain,
( ~ ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(pattern_uni,[status(thm)],[906:[bind(A,$thf( suc @ C )),bind(B,$thf( C ))]]) ).
thf(1027,plain,
! [A: nat] :
( ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,907]) ).
thf(1028,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(simp,[status(thm)],[1027]) ).
thf(1040,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( A != x )
| ( ( setof @ ( (=) @ nat @ n_1 ) )
!= ( setof
@ ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[1028]) ).
thf(1052,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( setof @ ( (=) @ nat @ n_1 ) )
!= ( setof
@ ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[1040]) ).
thf(1222,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( (=) @ nat @ n_1 )
!= ( ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[1052]) ).
thf(1229,plain,
( ( n_1 != sk3 )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(func_ext,[status(esa)],[1222]) ).
thf(1236,plain,
( ( sk3 != n_1 )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(lifteq,[status(thm)],[1229]) ).
thf(1240,plain,
! [A: nat] :
( ~ ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( sk3 != n_1 )
| ( x != x )
| ( A
!= ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[454,1236]) ).
thf(1241,plain,
! [A: nat] :
( ~ ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( sk3 != n_1 )
| ( A
!= ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(simp,[status(thm)],[1240]) ).
thf(1242,plain,
( ~ ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( sk3 != n_1 ) ),
inference(pattern_uni,[status(thm)],[1241:[bind(A,$thf( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) ))]]) ).
thf(89,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ~ ( B @ A ) ),
inference(prim_subst,[status(thm)],[12:[bind(A,$thf( ^ [D: nat] : ~ ( C @ D ) ))]]) ).
thf(116,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ~ ( B @ A ) ),
inference(cnf,[status(esa)],[89]) ).
thf(117,plain,
! [B: nat > $o,A: nat] :
( ~ ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ~ ( B @ A ) ),
inference(simp,[status(thm)],[116]) ).
thf(1025,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( A @ B )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,907]) ).
thf(1026,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( A @ B )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(simp,[status(thm)],[1025]) ).
thf(1045,plain,
( ~ ( esti @ x
@ ( setof
@ ^ [A: nat] : ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(pre_uni,[status(thm)],[1026:[bind(A,$thf( ^ [C: nat] : ( esti @ C @ ( setof @ ( (=) @ nat @ n_1 ) ) ) )),bind(B,$thf( x ))]]) ).
thf(1324,plain,
! [A: nat] :
( ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ x
@ ( setof
@ ^ [B: nat] : ( esti @ B @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,1045]) ).
thf(1325,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ x
@ ( setof
@ ^ [B: nat] : ( esti @ B @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ) ) ),
inference(simp,[status(thm)],[1324]) ).
thf(1340,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( A != x )
| ( ( setof
@ ^ [B: nat] : ( esti @ B @ ( setof @ ( (=) @ nat @ n_1 ) ) ) )
!= ( setof
@ ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[1325]) ).
thf(1343,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( setof
@ ^ [A: nat] : ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) ) )
!= ( setof
@ ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[1340]) ).
thf(84,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( ( A @ B )
!= ( ~ ( esti @ B @ ( setof @ A ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[12]) ).
thf(92,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( ( A @ B )
!= ( ~ ( esti @ B @ ( setof @ A ) ) ) ) ),
inference(simp,[status(thm)],[84]) ).
thf(479,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)],[445,117]) ).
thf(480,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)],[479]) ).
thf(508,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)],[480]) ).
thf(518,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ A )
| ( ( setof
@ ^ [C: nat] :
~ ( B @ C ) )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[508]) ).
thf(662,plain,
! [B: nat > $o,A: nat] :
( ~ ( B @ A )
| ( ( ^ [C: nat] :
~ ( B @ C ) )
!= ( ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[518]) ).
thf(1407,plain,
! [A: nat] :
( ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( sk3 != n_1 )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,1242]) ).
thf(1408,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( sk3 != n_1 )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ n_1 @ ( setof @ ( (=) @ nat @ x ) ) ) ) ),
inference(simp,[status(thm)],[1407]) ).
thf(1427,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( sk3 != n_1 )
| ( A != n_1 )
| ( ( setof @ ( (=) @ nat @ x ) )
!= ( setof
@ ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[1408]) ).
thf(1436,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ x ) ) )
!= x )
| ( sk3 != n_1 )
| ( ( setof @ ( (=) @ nat @ x ) )
!= ( setof
@ ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[1427]) ).
thf(1046,plain,
( ~ ( esti @ n_1
@ ( setof
@ ^ [A: nat] : ( esti @ x @ ( setof @ ( (=) @ nat @ A ) ) ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(pre_uni,[status(thm)],[1026:[bind(A,$thf( ^ [C: nat] : ( esti @ x @ ( setof @ ( (=) @ nat @ C ) ) ) )),bind(B,$thf( n_1 ))]]) ).
thf(1362,plain,
! [A: nat] :
( ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ n_1
@ ( setof
@ ^ [B: nat] : ( esti @ x @ ( setof @ ( (=) @ nat @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,1046]) ).
thf(1363,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ n_1
@ ( setof
@ ^ [B: nat] : ( esti @ x @ ( setof @ ( (=) @ nat @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[1362]) ).
thf(1379,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( A != n_1 )
| ( ( setof
@ ^ [B: nat] : ( esti @ x @ ( setof @ ( (=) @ nat @ B ) ) ) )
!= ( setof
@ ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[1363]) ).
thf(1382,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( setof
@ ^ [A: nat] : ( esti @ x @ ( setof @ ( (=) @ nat @ A ) ) ) )
!= ( setof
@ ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[1379]) ).
thf(2009,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( ^ [A: nat] : ( esti @ x @ ( setof @ ( (=) @ nat @ A ) ) ) )
!= ( ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[1382]) ).
thf(2018,plain,
( ~ ( esti @ x @ ( setof @ ( (=) @ nat @ sk6 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(func_ext,[status(esa)],[2009]) ).
thf(2045,plain,
! [A: nat] :
( ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ sk6 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,2018]) ).
thf(2046,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ A
@ ( setof
@ ^ [B: nat] : $true ) )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ sk6 ) ) ) ) ),
inference(simp,[status(thm)],[2045]) ).
thf(2071,plain,
! [A: nat] :
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( A != x )
| ( ( setof @ ( (=) @ nat @ sk6 ) )
!= ( setof
@ ^ [B: nat] : $true ) ) ),
inference(simp,[status(thm)],[2046]) ).
thf(2086,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( setof @ ( (=) @ nat @ sk6 ) )
!= ( setof
@ ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[2071]) ).
thf(2266,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( (=) @ nat @ sk6 )
!= ( ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[2086]) ).
thf(2273,plain,
( ( sk6 != sk7 )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(func_ext,[status(esa)],[2266]) ).
thf(2280,plain,
( ( sk7 != sk6 )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(lifteq,[status(thm)],[2273]) ).
thf(7,axiom,
! [A: nat,B: nat] :
( ( A != B )
=> ( ( suc @ A )
!= ( suc @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',satz1) ).
thf(23,plain,
! [A: nat,B: nat] :
( ( A != B )
=> ( ( suc @ A )
!= ( suc @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(24,plain,
! [B: nat,A: nat] :
( ( A = B )
| ( ( suc @ A )
!= ( suc @ B ) ) ),
inference(cnf,[status(esa)],[23]) ).
thf(25,plain,
! [B: nat,A: nat] :
( ( A = B )
| ( ( suc @ A )
!= ( suc @ B ) ) ),
inference(lifteq,[status(thm)],[24]) ).
thf(56,plain,
! [B: nat,A: set] :
( ( esti @ B @ A )
| ~ ( esti @ x @ A )
| ( ( sk1 @ A )
!= x )
| ( ( esti @ n_1 @ A )
!= ( esti @ x @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[39]) ).
thf(57,plain,
! [B: nat,A: set] :
( ( esti @ B @ A )
| ~ ( esti @ x @ A )
| ( ( sk1 @ A )
!= x )
| ( ( esti @ n_1 @ A )
!= ( esti @ x @ A ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(28,plain,
! [A: nat] :
( ( n_1 != x )
| ( ( suc @ x )
!= ( suc @ A ) ) ),
inference(paramod_ordered,[status(thm)],[10,22]) ).
thf(29,plain,
n_1 != x,
inference(pattern_uni,[status(thm)],[28:[bind(A,$thf( x ))]]) ).
thf(470,plain,
! [B: nat,A: nat] :
( ~ $true
| ( ( esti @ A
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[445,115]) ).
thf(471,plain,
! [B: nat,A: nat] :
( ( esti @ A
@ ( setof
@ ^ [C: nat] : $true ) )
!= ( esti @ B
@ ( setof
@ ^ [C: nat] : $false ) ) ),
inference(simp,[status(thm)],[470]) ).
thf(509,plain,
! [B: nat,A: nat] :
( ( A != B )
| ( ( setof
@ ^ [C: nat] : $false )
!= ( setof
@ ^ [C: nat] : $true ) ) ),
inference(simp,[status(thm)],[471]) ).
thf(519,plain,
( ( setof
@ ^ [A: nat] : $false )
!= ( setof
@ ^ [A: nat] : $true ) ),
inference(simp,[status(thm)],[509]) ).
thf(421,plain,
! [B: nat > $o,A: nat] :
( ~ ~ ( B @ A )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(prim_subst,[status(thm)],[18:[bind(A,$thf( ^ [D: nat] : ~ ( C @ D ) ))]]) ).
thf(446,plain,
! [B: nat > $o,A: nat] :
( ( B @ A )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(cnf,[status(esa)],[421]) ).
thf(447,plain,
! [B: nat > $o,A: nat] :
( ( B @ A )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(simp,[status(thm)],[446]) ).
thf(15,plain,
! [B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ ( sk1 @ A ) @ A )
| ( esti @ B @ A ) ),
inference(cnfConj,[status(thm)],[14]) ).
thf(761,plain,
! [D: nat,C: set,B: nat > $o,A: nat] :
( ( B @ A )
| ~ $true
| ( esti @ ( sk1 @ C ) @ C )
| ( esti @ D @ C )
| ( ( esti @ A
@ ( setof
@ ^ [E: nat] :
~ ( B @ E ) ) )
!= ( esti @ n_1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[447,15]) ).
thf(762,plain,
! [D: nat,C: set,B: nat > $o,A: nat] :
( ( B @ A )
| ( esti @ ( sk1 @ C ) @ C )
| ( esti @ D @ C )
| ( ( esti @ A
@ ( setof
@ ^ [E: nat] :
~ ( B @ E ) ) )
!= ( esti @ n_1 @ C ) ) ),
inference(simp,[status(thm)],[761]) ).
thf(763,plain,
! [B: nat > $o,A: nat] :
( ( B @ n_1 )
| ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(pattern_uni,[status(thm)],[762:[bind(A,$thf( n_1 )),bind(B,$thf( F )),bind(C,$thf( setof @ ^ [F: nat] : ~ ( F @ F ) )),bind(D,$thf( D ))]]) ).
thf(869,plain,
! [B: nat > $o,A: nat] :
( ( B @ n_1 )
| ( esti
@ ( sk1
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) )
| ( esti @ A
@ ( setof
@ ^ [C: nat] :
~ ( B @ C ) ) ) ),
inference(simp,[status(thm)],[763]) ).
thf(1925,plain,
( ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( ^ [A: nat] : ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) ) )
!= ( ^ [A: nat] : $true ) ) ),
inference(simp,[status(thm)],[1343]) ).
thf(1932,plain,
( ~ ( esti @ sk5 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(func_ext,[status(esa)],[1925]) ).
thf(1966,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ sk5 @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,1932]) ).
thf(1967,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ B )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ sk5 @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(simp,[status(thm)],[1966]) ).
thf(1968,plain,
( ( n_1 != sk5 )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(pattern_uni,[status(thm)],[1967:[bind(A,$thf( (=) @ nat @ n_1 )),bind(B,$thf( sk5 ))]]) ).
thf(1979,plain,
( ( sk5 != n_1 )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(lifteq,[status(thm)],[1968]) ).
thf(26,plain,
? [A: nat > nat] :
! [B: nat] :
( ( A @ ( suc @ B ) )
= B ),
inference(detectInverse,[status(thm)],[25]) ).
thf(27,plain,
! [A: nat] :
( ( sk2 @ ( suc @ A ) )
= A ),
inference(cnf,[status(esa)],[26]) ).
thf(30,plain,
! [A: nat] :
( ( sk2 @ ( suc @ A ) )
= A ),
inference(lifteq,[status(thm)],[27]) ).
thf(31,plain,
! [A: nat] :
( ( ( sk2 @ x )
= A )
| ( ( suc @ x )
!= ( suc @ A ) ) ),
inference(paramod_ordered,[status(thm)],[10,30]) ).
thf(32,plain,
( ( sk2 @ x )
= x ),
inference(pattern_uni,[status(thm)],[31:[bind(A,$thf( x ))]]) ).
thf(2047,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ B )
| ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ sk6 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,2018]) ).
thf(2048,plain,
! [B: nat,A: nat > $o] :
( ~ ( A @ B )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( esti @ B @ ( setof @ A ) )
!= ( esti @ x @ ( setof @ ( (=) @ nat @ sk6 ) ) ) ) ),
inference(simp,[status(thm)],[2047]) ).
thf(2049,plain,
( ( sk6 != x )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(pattern_uni,[status(thm)],[2048:[bind(A,$thf( (=) @ nat @ sk6 )),bind(B,$thf( x ))]]) ).
thf(2069,plain,
( ( sk6 != x )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(lifteq,[status(thm)],[2049]) ).
thf(61,plain,
! [A: nat] :
( ( x = A )
| ( ( sk2 @ ( suc @ A ) )
!= ( sk2 @ x ) ) ),
inference(paramod_ordered,[status(thm)],[32,30]) ).
thf(63,plain,
! [A: nat] :
( ( x = A )
| ( ( suc @ A )
!= x ) ),
inference(simp,[status(thm)],[61]) ).
thf(1962,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ~ $true
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( A @ B )
!= ( esti @ sk5 @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,1932]) ).
thf(1963,plain,
! [B: nat,A: nat > $o] :
( ~ ( esti @ B @ ( setof @ A ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x )
| ( ( A @ B )
!= ( esti @ sk5 @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) ),
inference(simp,[status(thm)],[1962]) ).
thf(1981,plain,
( ~ ( esti @ sk5
@ ( setof
@ ^ [A: nat] : ( esti @ A @ ( setof @ ( (=) @ nat @ n_1 ) ) ) ) )
| ( ( sk1 @ ( setof @ ( (=) @ nat @ n_1 ) ) )
!= x ) ),
inference(pre_uni,[status(thm)],[1963:[bind(A,$thf( ^ [C: nat] : ( esti @ C @ ( setof @ ( (=) @ nat @ n_1 ) ) ) )),bind(B,$thf( sk5 ))]]) ).
thf(38,plain,
! [B: nat,A: set] :
( ~ ( esti @ n_1 @ A )
| ( esti @ B @ A )
| ( ( esti @ ( suc @ ( sk1 @ A ) ) @ A )
!= ( esti @ n_1 @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(40,plain,
! [B: nat,A: set] :
( ( esti @ B @ A )
| ~ ( esti @ n_1 @ A )
| ( ( esti @ ( suc @ ( sk1 @ A ) ) @ A )
!= ( esti @ n_1 @ A ) ) ),
inference(simp,[status(thm)],[38]) ).
thf(2749,plain,
$false,
inference(e,[status(thm)],[115,110,1242,117,1343,92,662,22,39,1436,518,2280,10,1222,1046,25,57,29,519,869,1382,1932,13,1979,32,17,12,445,2086,2069,63,18,16,907,1981,1052,11,2266,40,23,1045,2009,8,447,30,19,1236,15,1925,2018,454]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM636^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.11 % 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.28/0.32 % Computer : n008.cluster.edu
% 0.28/0.32 % Model : x86_64 x86_64
% 0.28/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.28/0.32 % Memory : 8046.5625MB
% 0.28/0.32 % OS : Linux 6.8.0-71-generic
% 0.28/0.32 % CPULimit : 300
% 0.28/0.32 % WCLimit : 300
% 0.28/0.32 % DateTime : Tue Sep 29 12:02:24 UTC 2026
% 0.28/0.32 % CPUTime :
% 0.28/0.32 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.36/1.06 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.70/1.21 % [INFO] Parsing done (153ms).
% 1.70/1.22 % [INFO] Running in sequential loop mode.
% 2.49/1.77 % [INFO] eprover registered as external prover.
% 2.49/1.78 % [INFO] Scanning for conjecture ...
% 2.70/1.89 % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ...
% 2.89/1.93 % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms).
% 2.89/1.97 % [INFO] Problem is higher-order (TPTP THF).
% 2.89/1.98 % [INFO] Type checking passed.
% 2.89/1.98 % [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 ...
% 25.04/6.80 % External prover 'e' found a proof!
% 25.04/6.81 % [INFO] Killing All external provers ...
% 25.04/6.81 % Time passed: 6293ms (effective reasoning time: 5578ms)
% 25.04/6.81 % 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)>
% 25.04/6.81 % Axioms used in derivation (5): estii, satz1, estie, ax3, ax5
% 25.04/6.81 % No. of inferences in proof: 133
% 25.04/6.81 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 6293 ms resp. 5578 ms w/o parsing
% 22.55/6.98 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 22.55/6.99 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------